Theorems · Definition · category theory

CategoryTheory.Localization.liftNatIso

{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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            {E : Type u_3} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                [L.IsLocalization W] →
                  (F₁ F₂ : CategoryTheory.Functor C E) →
                    (F₁' F₂' : CategoryTheory.Functor D E) →
                      [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] →
                        [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'] → (F₁ ≅ F₂) → (F₁' ≅ F₂')

Given a localization functor L : C ⥤ D for W : MorphismProperty C, if (F₁' F₂' : D ⥤ E) are functors which lift functors (F₁ F₂ : C ⥤ E), a natural isomorphism τ : F₁ ⟶ F₂ lifts to a natural isomorphism F₁' ⟶ F₂'.

Defined in

Mathlib.CategoryTheory.Localization.Predicate

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Localization.LiftingCategoryTheory.Localization.Lifting