English
Naturality of the inverse side of the homotopy equivalence: I.iso.inv composed with the functorial map equals the isomorphism on the quotient side composed with J.iso.inv.
Русский
Естественность для обратной стороны гомотопийного эквивалента: I.iso.inv ∘ (injectiveResolutions C).map f = (HomotopyCategory.quotient _ _).map φ ∘ J.iso.inv.
LaTeX
$$I.iso.inv ≫ (injectiveResolutions C).map f = (HomotopyCategory.quotient _ _).map φ ≫ J.iso.inv$$
Lean4
@[reassoc]
theorem iso_inv_naturality {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y)
(φ : I.cocomplex ⟶ J.cocomplex) (comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0) :
I.iso.inv ≫ (injectiveResolutions C).map f = (HomotopyCategory.quotient _ _).map φ ≫ J.iso.inv := by
rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm, Iso.inv_hom_id_assoc, Category.assoc,
Iso.inv_hom_id, Category.comp_id]
