English
A technical identity relating the left component of the cylinder with the null-homotopic map via a long, structured expression; it is used to prove how nullHomotopicMap behaves on X components in presence of a homotopy cofibre.
Русский
Техническое тождество, связывающее левый компонент цилиндра с нулевой гомотопией через сложное выражение; используется для анализа поведения nullHomotopicMap на компонентах X в условиях кофибра.
LaTeX
$$$\text{(complex identity)}$$$
Lean4
/-- If a functor inverts homotopy equivalences, it sends homotopic maps to the same map. -/
theorem _root_.Homotopy.map_eq_of_inverts_homotopyEquivalences {φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁)
(hc : ∀ j, ∃ i, c.Rel i j) [∀ i, HasBinaryBiproduct (F.X i) (F.X i)] [HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))]
{D : Type*} [Category D] (H : HomologicalComplex C c ⥤ D) (hH : (homotopyEquivalences C c).IsInvertedBy H) :
H.map φ₀ = H.map φ₁ := by
simp only [← cylinder.ι₀_desc _ _ h, ← cylinder.ι₁_desc _ _ h, H.map_comp, cylinder.map_ι₀_eq_map_ι₁ _ hc _ hH]
