English
Equivalently restated: data in the Sigma type with a homotopy is determined by its first coordinate and all the homotopy components agree componentwise.
Русский
Эквивалентно: данные в сигма-типе с гомотопией задаются по первой координате и по всем компонентам гомотопии согласованы по компонентам.
LaTeX
$$$ {\\text{eq}_{\\text{sim}}} \\;(x,y) \\Leftrightarrow \\dots $$$
Lean4
/-- Morphisms `homotopyCofiber φ ⟶ K` are uniquely determined by
a morphism `α : G ⟶ K` and a homotopy from `φ ≫ α` to `0`. -/
noncomputable def descEquiv (K : HomologicalComplex C c) (hc : ∀ j, ∃ i, c.Rel i j) :
(Σ (α : G ⟶ K), Homotopy (φ ≫ α) 0) ≃ (homotopyCofiber φ ⟶ K)
where
toFun := fun ⟨α, hα⟩ => desc φ α hα
invFun
f :=
⟨inr φ ≫ f,
Homotopy.trans (Homotopy.ofEq (by simp)) (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq (by simp)))⟩
right_inv f := (eq_desc φ f hc).symm
left_inv := fun ⟨α, hα⟩ => by
rw [descSigma_ext_iff]
cat_disch
