Theorems · Definition · category theory

CategoryTheory.Localization.compUniqFunctor

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst_1 : CategoryTheory.Category.{v_4, u_4} D₁] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D₂] →
            (L₁ : CategoryTheory.Functor C D₁) →
              (L₂ : CategoryTheory.Functor C D₂) →
                (W' : CategoryTheory.MorphismProperty C) →
                  [inst_3 : L₁.IsLocalization W'] →
                    [inst_4 : L₂.IsLocalization W'] → L₁.comp (CategoryTheory.Localization.uniq L₁ L₂ W').functor ≅ L₂

The functor of equivalence of localized categories given by Localization.uniq is compatible with the localization functors.

Defined in

Mathlib.CategoryTheory.Localization.Predicate

Cited by

16 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalization