VertexColumnComplex.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.VertexColumnComplex.vertexColumn line 15
def OAI.LittleFinitistic.VertexColumnComplex.diagonalNatIso line 20
Source documentation
The diagonal insertion is natural in the original right module.
```
def diagonalNatIso (i : Fin 3) : 𝟭 (ModuleCat.{u} Tᵐᵒᵖ) ≅ vertexColumn μ i i :=
…
```
Mentions: OAI.LittleFinitistic.VertexColumnComplex.vertexColumn
def OAI.LittleFinitistic.VertexColumnComplex.diagonalComplexIso line 34
Source documentation
On actual complexes, the diagonal vertex is the original complex via its specified insertion.
```
def diagonalComplexIso (i : Fin 3) (D : CochainComplex (ModuleCat.{u} Tᵐᵒᵖ) ℤ) :
    D ≅ ((vertexColumn μ i i).mapHomologicalComplex (.up ℤ)).obj D :=
…
```
Mentions: OAI.LittleFinitistic.VertexColumnComplex.vertexColumn
theorem OAI.LittleFinitistic.VertexColumnComplex.reverse_isZero line 40
Source documentation
Every term of a reverse vertex column is zero, hence the actual complex is zero.
```
theorem reverse_isZero (i j : Fin 3) (hij : i < j)
    (D : CochainComplex (ModuleCat.{u} Tᵐᵒᵖ) ℤ) :
    IsZero (((vertexColumn μ i j).mapHomologicalComplex (.up ℤ)).obj D) := by
…
```
Mentions: OAI.LittleFinitistic.VertexColumnComplex.vertexColumn