homotopyEquiv — Mathlib

English

Any two injective resolutions of X are connected by a homotopy equivalence, given by desc (𝟙 X) J I and its inverse, with associated homotopies.

Русский

Любые две инъективные резолюции X связаны гомотопийным эквивалентом, задаваемым desc (𝟙 X) J I и его обратной стороной с соответствующими гомотопиями.

LaTeX

$$homotopyEquiv X I J = { hom := desc (id X) J I, inv := desc (id X) I J, ... }$$

Lean4

/-- Any two injective resolutions are homotopy equivalent. -/
def homotopyEquiv {X : C} (I J : InjectiveResolution X) : HomotopyEquiv I.cocomplex J.cocomplex
    where
  hom := desc (𝟙 X) J I
  inv := desc (𝟙 X) I J
  homotopyHomInvId := (descCompHomotopy (𝟙 X) (𝟙 X) I J I).symm.trans <| by simpa [id_comp] using descIdHomotopy _ _
  homotopyInvHomId := (descCompHomotopy (𝟙 X) (𝟙 X) J I J).symm.trans <| by simpa [id_comp] using descIdHomotopy _ _

Похожие утверждения