Theorems · Definition · category theory

ComplexShape.strictUniversalPropertyFixedTargetQuotient

{ι : Type u_1} →
  (c : ComplexShape ι) →
    (∀ (j : ι), ∃ i, c.Rel i j) →
      (C : Type u_2) →
        [inst : CategoryTheory.Category.{v_1, u_2} C] →
          [inst_1 : CategoryTheory.Preadditive C] →
            [CategoryTheory.Limits.HasBinaryBiproducts C] →
              (E : Type u_3) →
                [inst_3 : CategoryTheory.Category.{v_2, u_3} E] →
                  CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c)
                    (HomologicalComplex.homotopyEquivalences C c) E

The homotopy category satisfies the universal property of the localized category with respect to homotopy equivalences.

Defined in

Mathlib.Algebra.Homology.Localization

Cited by

1 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Limits.HasBinaryBiproductsCategoryTheory.Category