iso — Mathlib

English

There is an isomorphism between the image of a resolution in the homotopy quotient and the original cocomplex, given by the equivalence of the quotient with the chosen resolution.

Русский

Существует изоморфизм между образом резолюции и исходным кококомплексом в гомотопической категории.

LaTeX

$$iso {X} (I : InjectiveResolution X) : (injectiveResolutions C).obj X ≅ (HomotopyCategory.quotient _ _).obj I.cocomplex$$

Lean4

/-- If `I : InjectiveResolution X`, then the chosen `(injectiveResolutions C).obj X`
is isomorphic (in the homotopy category) to `I.cocomplex`. -/
def iso {X : C} (I : InjectiveResolution X) :
    (injectiveResolutions C).obj X ≅ (HomotopyCategory.quotient _ _).obj I.cocomplex :=
  HomotopyCategory.isoOfHomotopyEquiv (homotopyEquiv _ _)

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