strictUniversalPropertyFixedTargetQuotient

Lean4

/-- The homotopy category satisfies the universal property of the localized category
with respect to homotopy equivalences. -/
def strictUniversalPropertyFixedTargetQuotient (E : Type*) [Category E] :
    Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c)
      (HomologicalComplex.homotopyEquivalences C c) E
    where
  inverts := HomotopyCategory.quotient_inverts_homotopyEquivalences C c
  lift F
    hF :=
    CategoryTheory.Quotient.lift _ F
      (by
        intro K L f g ⟨h⟩
        have : DecidableRel c.Rel := by classical infer_instance
        exact h.map_eq_of_inverts_homotopyEquivalences hc F hF)
  fac _ _ := rfl
  uniq _ _ h := Quotient.lift_unique' _ _ _ h

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