ChainRepresentatives.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.ChainRepresentatives.quadratic_chain_representatives line 16

Source documentation

Choosing chain representatives of a finite quadratic diagram supplies actual, specified null-homotopies for all its relations.

theorem quadratic_chain_representatives (na nb nr : ℕ)
    (D₀ D₁ D₂ : HomologicalComplex V s)
    (a : Fin na → ((HomotopyCategory.quotient V s).obj D₀ ⟶
      (HomotopyCategory.quotient V s).obj D₁))
    (b : Fin nb → ((HomotopyCategory.quotient V s).obj D₁ ⟶
      (HomotopyCategory.quotient V s).obj D₂))
    (c : Fin nr → Fin na → Fin nb → k)
    (hc : ∀ t, ∑ i, ∑ j, c t i j • (a i ≫ b j) = 0) :
    ∃ (f : Fin na → (D₀ ⟶ D₁)) (g : Fin nb → (D₁ ⟶ D₂)),
      (∀ i, (HomotopyCategory.quotient V s).map (f i) = a i) ∧
      (∀ j, (HomotopyCategory.quotient V s).map (g j) = b j) ∧
      Nonempty (∀ t, Homotopy (∑ i, ∑ j, c t i j • (f i ≫ g j)) 0) := by
…

theorem OAI.LittleFinitistic.ChainRepresentatives.cochain_null_homotopy_equation line 41
Source documentation
In cochain conventions the chosen homotopy has degree minus one, with the exact differential equation used in the tensor construction.
```
theorem cochain_null_homotopy_equation {D E : CochainComplex V ℤ}
    (f : D ⟶ E) (h : Homotopy f 0) (i : ℤ) :
    f.f i = D.d i (i+1) ≫ h.hom (i+1) i + h.hom i (i-1) ≫ E.d (i-1) i := by
…
```