Q_inverts_homotopyEquivalences — Mathlib

English

All homotopy equivalences in the homological complex setting are inverted by the functor Q.

Русский

Все гомотопические эквивалентности в контексте гомологических комплексов обращаются локализацией Q.

LaTeX

$$$ \forall h \in \mathrm{HomotopyEquivalences}(C,c),\quad \operatorname{IsIso}\bigl(Q(h)\bigr). $$$

Lean4

theorem Q_inverts_homotopyEquivalences [(HomologicalComplex.quasiIso C c).HasLocalization] :
    (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy HomologicalComplexUpToQuasiIso.Q :=
  MorphismProperty.IsInvertedBy.of_le _ _ _ (Localization.inverts Q (HomologicalComplex.quasiIso C c))
    (homotopyEquivalences_le_quasiIso C c)

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