quotient_isLocalization — Mathlib

English

The quotient by homotopy relations is a localization with respect to homotopy equivalences.

Русский

Квартит по отношению к гомотопическим эквивалентностям является локализацией.

LaTeX

$$$ (HomotopyCategory.quotient\ C\ c).IsLocalization(HomologicalComplex.homotopyEquivalences\ C\ c). $$$

Lean4

theorem quotient_isLocalization :
    (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences _ _) :=
  by
  apply Functor.IsLocalization.mk'
  all_goals apply c.strictUniversalPropertyFixedTargetQuotient hc

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