VertexZeroTotal.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.VertexZeroTotal.vertexFunctor line 16
theorem OAI.LittleFinitistic.VertexZeroTotal.column_zero line 20
Source documentation
Actual column terms vanish at vertex zero when their supporting vertex is positive.
```
theorem column_zero (j : Fin 3) (hj : 0 < j) (D : RightComplex (QuadraticEncoding.B P)) (n : ℤ) :
    IsZero ((vertexFunctor P).obj
      (((columnComplex k B (ThreeVertexAlgebra.vertex (QuadraticEncoding.composition P) j)).obj D).X n)) := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.B, OAI.LittleFinitistic.VertexZeroTotal.vertexFunctor, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.QuadraticEncoding.composition
theorem OAI.LittleFinitistic.VertexZeroTotal.higher_zero line 30
Source documentation
Both higher columns of the constructed total vanish at the first vertex.
```
theorem higher_zero (n : ℤ) :
    IsZero ((vertexFunctor P).obj ((L1Prime s D₀ D₁ D₂ f g).X n)) ∧
    IsZero ((vertexFunctor P).obj ((L2Prime s D₀ D₁ D₂ f g).X n)) := by
…
```
Mentions: OAI.LittleFinitistic.VertexZeroTotal.vertexFunctor
theorem OAI.LittleFinitistic.VertexZeroTotal.inclusion_isIso line 52
Source documentation
At vertex zero, the original zero-column inclusion in the actual total is an isomorphism.
```
theorem inclusion_isIso (H : ∀ r, Homotopy (relationMap s D₀ D₁ D₂ f g r) 0) :
    IsIso (((vertexFunctor P).mapHomologicalComplex (.up ℤ)).map
      (InducedRectification.inclusion s D₀ D₁ D₂ f g H)) :=
…
```
Mentions: OAI.LittleFinitistic.VertexZeroTotal.vertexFunctor, OAI.LittleFinitistic.InducedRectification.inclusion