Theorems · Definition · category theory

HomRel.FactorsThroughLocalization.strictUniversalPropertyFixedTarget

{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {homRel : HomRel C} →
          {W : CategoryTheory.MorphismProperty C} →
            homRel.FactorsThroughLocalization W →
              {W' : CategoryTheory.MorphismProperty (CategoryTheory.Quotient homRel)} →
                W = W'.inverseImage (CategoryTheory.Quotient.functor homRel) →
                  {E : Type u_3} →
                    [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                      (L' : CategoryTheory.Functor (CategoryTheory.Quotient homRel) D) →
                        CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L' W' E →
                          CategoryTheory.Localization.StrictUniversalPropertyFixedTarget
                            ((CategoryTheory.Quotient.functor homRel).comp L') W E

If L' : Quotient homRel ⥤ D satisfies the strict universal property of the localization, then Quotient.functor homRel ⋙ L' also satisfies it.

Defined in

Mathlib.CategoryTheory.Localization.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category