VertexHomotopyEquivalence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.VertexHomotopyEquivalence.source line 15
abbrev OAI.LittleFinitistic.VertexHomotopyEquivalence.target line 17
def OAI.LittleFinitistic.VertexHomotopyEquivalence.iota line 21
theorem OAI.LittleFinitistic.VertexHomotopyEquivalence.iota_quasiIso line 30
Source documentation
All three original vertex insertions are quasi-isomorphisms.
```
theorem iota_quasiIso (v : Fin 3) : QuasiIso (iota P D₀ D₁ D₂ f g H v) := by
…
```
Mentions: OAI.LittleFinitistic.VertexHomotopyEquivalence.iota

theorem OAI.LittleFinitistic.VertexHomotopyEquivalence.homotopy_inverse line 40

Source documentation

The actual vertex insertions have chain-map inverses and both homotopies. Only the boundedness and projectivity of the chosen chain representatives are inputs.

theorem homotopy_inverse (v : Fin 3) (lo hi : ℤ)
    (b₀ : ∀ n, n < lo ∨ hi < n → IsZero (D₀.X n))
    (b₁ : ∀ n, n < lo ∨ hi < n → IsZero (D₁.X n))
    (b₂ : ∀ n, n < lo ∨ hi < n → IsZero (D₂.X n))
    (p₀ : ∀ n, Module.Projective (QuadraticEncoding.B P)ᵐᵒᵖ (D₀.X n))
    (p₁ : ∀ n, Module.Projective (QuadraticEncoding.B P)ᵐᵒᵖ (D₁.X n))
    (p₂ : ∀ n, Module.Projective (QuadraticEncoding.B P)ᵐᵒᵖ (D₂.X n)) :
    ∃ j : target P D₀ D₁ D₂ f g H v ⟶ source P D₀ D₁ D₂ v,
      Nonempty (Homotopy (iota P D₀ D₁ D₂ f g H v ≫ j) (𝟙 _)) ∧
      Nonempty (Homotopy (j ≫ iota P D₀ D₁ D₂ f g H v) (𝟙 _)) := by
…

Mentions: OAI.LittleFinitistic.QuadraticEncoding.B, OAI.LittleFinitistic.VertexHomotopyEquivalence.target, OAI.LittleFinitistic.VertexHomotopyEquivalence.source, OAI.LittleFinitistic.VertexHomotopyEquivalence.iota