Theorems · Definition · category theory

CategoryTheory.Localization.Lifting.ofIsos

{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] →
                {F₁ F₂ : CategoryTheory.Functor C E} →
                  {F₁' F₂' : CategoryTheory.Functor D E} →
                    (F₁ ≅ F₂) →
                      (F₁' ≅ F₂') →
                        [CategoryTheory.Localization.Lifting L W F₁ F₁'] →
                          CategoryTheory.Localization.Lifting L W F₂ F₂'

Given a localization functor L : C ⥤ D for W : MorphismProperty C, if F₁' : D ⥤ E lifts a functor F₁ : C ⥤ D, then a functor F₂' which is isomorphic to F₁' also lifts a functor F₂ that is isomorphic to F₁.

Defined in

Mathlib.CategoryTheory.Localization.Predicate

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Localization.Lifting