homotopyEquiv_inv_ι — Mathlib

English

The inverse of the homotopy equivalence between two injective resolutions is natural with respect to morphisms and the 0-th iota maps.

Русский

Обратный гомотопийный эквивалент двух резолюций естественен по отношению к морфизмам и нулевым картам iota.

LaTeX

$$I.iso.inv ≫ (injectiveResolutions C).map f = (HomotopyCategory.quotient _ _).map φ ≫ J.iso.inv$$

Lean4

@[reassoc (attr := simp)]
theorem homotopyEquiv_inv_ι {X : C} (I J : InjectiveResolution X) : J.ι ≫ (homotopyEquiv I J).inv = I.ι := by
  simp [homotopyEquiv]

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