OAI/Algebra/Finitistic/Rectification/
494 declarations, 0 contain sorry, 0 declared as axioms; 64 files
Files
- AdjacentArrowSum.lean 4 declarations
- ArrowCompatibility.lean 9 declarations
- ArrowVertex.lean 19 declarations
- BiprodEvaluationSquare.lean 2 declarations
- CanonicalArrowCompatibility.lean 7 declarations
- ColumnComplex.lean 16 declarations
- ColumnFinite.lean 10 declarations
- ColumnProperties.lean 16 declarations
- ConcreteAdjacentGraded.lean 6 declarations
- CornerArrowCoordinates.lean 3 declarations
- CornerColumnComplex.lean 3 declarations
- CornerColumnPaths.lean 2 declarations
- CornerPathTransport.lean 2 declarations
- CornerProjection.lean 8 declarations
- CornerSpaces.lean 6 declarations
- CornerTensor.lean 4 declarations
- DiagramAssembly.lean 11 declarations
- ExactProducts.lean 4 declarations
- ExternalTensor.lean 31 declarations
- FiltrationExactness.lean 12 declarations
- FinalGradedAcyclic.lean 1 declarations
- FirstVertex.lean 7 declarations
- FullTensorProperties.lean 3 declarations
- FullTensorRectification.lean 12 declarations
- GradedVertexAcyclic.lean 6 declarations
- InducedColumns.lean 17 declarations
- InducedDerivedFunctor.lean 3 declarations
- InducedDiagram.lean 22 declarations
- InducedRectification.lean 6 declarations
- LeftVertexHomology.lean 7 declarations
- RectificationAcyclic.lean 7 declarations
- RectificationLemma.lean 2 declarations
- RectificationTotal.lean 9 declarations
- SecondVertex.lean 9 declarations
- SourceFiltration.lean 24 declarations
- SourceFiltrationComplex.lean 8 declarations
- SourceFiltrationCone.lean 8 declarations
- SourceFiltrationExact.lean 10 declarations
- SourceFiltrationReal.lean 9 declarations
- TensorArrowComparison.lean 5 declarations
- TensorArrowSum.lean 4 declarations
- TensorComplex.lean 10 declarations
- TensorProjection.lean 7 declarations
- ThirdVertex.lean 5 declarations
- ThirdVertexFiltration.lean 2 declarations
- TotalExact.lean 4 declarations
- TotalFinite.lean 2 declarations
- TotalFunctorial.lean 19 declarations
- TotalInterchange.lean 12 declarations
- VertexCategoricalAssembly.lean 3 declarations
- VertexColumnComplex.lean 4 declarations
- VertexColumnModels.lean 3 declarations
- VertexDecomposition.lean 7 declarations
- VertexFunctor.lean 12 declarations
- VertexHomology.lean 3 declarations
- VertexHomotopyEquivalence.lean 5 declarations
- VertexModuleAssembly.lean 6 declarations
- VertexProjectives.lean 8 declarations
- VertexTensorEvaluation.lean 12 declarations
- VertexTensorLinear.lean 2 declarations
- VertexTotalProperties.lean 3 declarations
- VertexZeroTotal.lean 4 declarations
- ZeroColumnTotal.lean 5 declarations
- ZeroLastColumn.lean 2 declarations