Predicate for localized categories

In this file, a predicate L.IsLocalization W is introduced for a functor L : C ⥤ D and W : MorphismProperty C: it expresses that L identifies D with the localized category of C with respect to W (up to equivalence).

We introduce a universal property StrictUniversalPropertyFixedTarget L W E which states that L inverts the morphisms in W and that all functors C ⥤ E inverting W uniquely factors as a composition of L ⋙ G with G : D ⥤ E. Such universal properties are inputs for the constructor IsLocalization.mk' for L.IsLocalization W.

When L : C ⥤ D is a localization functor for W : MorphismProperty (i.e. when [L.IsLocalization W] holds), for any category E, there is an equivalence FunctorEquivalence L W E : (D ⥤ E) ≌ (W.FunctorsInverting E) that is induced by the composition with the functor L. When two functors F : C ⥤ E and F' : D ⥤ E correspond via this equivalence, we shall say that F' lifts F, and the associated isomorphism L ⋙ F' ≅ F is the datum that is part of the class Lifting L W F F'. The functions liftNatTrans and liftNatIso can be used to lift natural transformations and natural isomorphisms between functors.

class CategoryTheory.Functor.IsLocalization {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) : Prop

• inverts : CategoryTheory.MorphismProperty.IsInvertedBy W L

  the functor inverts the given MorphismProperty

• nonempty_isEquivalence : Nonempty (CategoryTheory.IsEquivalence (CategoryTheory.Localization.Construction.lift L (_ : CategoryTheory.MorphismProperty.IsInvertedBy W L)))

  the induced functor from the constructed localized category is an equivalence

The predicate expressing that, up to equivalence, a functor L : C ⥤ D identifies the category D with the localized category of C with respect to W : MorphismProperty C.

instance CategoryTheory.Functor.q_isLocalization {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (W : CategoryTheory.MorphismProperty C) : CategoryTheory.Functor.IsLocalization (CategoryTheory.MorphismProperty.Q W) W

structure CategoryTheory.Localization.StrictUniversalPropertyFixedTarget {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_6, u_3} E] : Type (max (max (max (max (max u_1 u_2) u_3) u_4) u_5) u_6)

• inverts : CategoryTheory.MorphismProperty.IsInvertedBy W L

  the functor L inverts W

• lift : (F : CategoryTheory.Functor C E) → CategoryTheory.MorphismProperty.IsInvertedBy W F → CategoryTheory.Functor D E

  any functor C ⥤ E which inverts W can be lifted as a functor D ⥤ E

• fac : ∀ (F : CategoryTheory.Functor C E) (hF : CategoryTheory.MorphismProperty.IsInvertedBy W F), CategoryTheory.Functor.comp L (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.lift s F hF) = F

  there is a factorisation involving the lifted functor

• uniq : ∀ (F₁ F₂ : CategoryTheory.Functor D E), CategoryTheory.Functor.comp L F₁ = CategoryTheory.Functor.comp L F₂ → F₁ = F₂

  uniqueness of the lifted functor

This universal property states that a functor L : C ⥤ D inverts morphisms in W and the all functors D ⥤ E (for a fixed category E) uniquely factors through L.

@[simp]

theorem CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ_lift {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_5, u_3} E] (G : CategoryTheory.Functor C E) (hG : CategoryTheory.MorphismProperty.IsInvertedBy W G) : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.lift (CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ W E) G hG = CategoryTheory.Localization.Construction.lift G hG

def CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_5, u_3} E] : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (CategoryTheory.MorphismProperty.Q W) W E

The localized category W.Localization that was constructed satisfies the universal property of the localization.

instance CategoryTheory.Localization.instInhabitedStrictUniversalPropertyFixedTargetLocalizationInstCategoryLocalizationQ {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_5, u_3} E] : Inhabited (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (CategoryTheory.MorphismProperty.Q W) W E)

@[simp]

theorem CategoryTheory.Localization.strictUniversalPropertyFixedTargetId_lift {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_5, u_3} E] (hW : W ⊆ CategoryTheory.MorphismProperty.isomorphisms C) (F : CategoryTheory.Functor C E) : ∀ (x : CategoryTheory.MorphismProperty.IsInvertedBy W F), CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.lift (CategoryTheory.Localization.strictUniversalPropertyFixedTargetId W E hW) F x = F

def CategoryTheory.Localization.strictUniversalPropertyFixedTargetId {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_5, u_3} E] (hW : W ⊆ CategoryTheory.MorphismProperty.isomorphisms C) : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (CategoryTheory.Functor.id C) W E

When W consists of isomorphisms, the identity satisfies the universal property of the localization.

theorem CategoryTheory.Functor.IsLocalization.mk' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) (h₁ : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W D) (h₂ : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W (CategoryTheory.MorphismProperty.Localization W)) : CategoryTheory.Functor.IsLocalization L W

theorem CategoryTheory.Functor.IsLocalization.for_id {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (W : CategoryTheory.MorphismProperty C) (hW : W ⊆ CategoryTheory.MorphismProperty.isomorphisms C) : CategoryTheory.Functor.IsLocalization (CategoryTheory.Functor.id C) W

theorem CategoryTheory.Localization.inverts {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.MorphismProperty.IsInvertedBy W L

@[simp]

theorem CategoryTheory.Localization.isoOfHom_inv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] {X : C} {Y : C} (f : X ⟶ Y) (hf : W X Y f) : (CategoryTheory.Localization.isoOfHom L W f hf).inv = CategoryTheory.inv (L.map f)

@[simp]

theorem CategoryTheory.Localization.isoOfHom_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] {X : C} {Y : C} (f : X ⟶ Y) (hf : W X Y f) : (CategoryTheory.Localization.isoOfHom L W f hf).hom = L.map f

def CategoryTheory.Localization.isoOfHom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] {X : C} {Y : C} (f : X ⟶ Y) (hf : W X Y f) : L.obj X ≅ L.obj Y

The isomorphism L.obj X ≅ L.obj Y that is deduced from a morphism f : X ⟶ Y which belongs to W, when L.IsLocalization W.

instance CategoryTheory.Localization.instIsEquivalenceLocalizationInstCategoryLocalizationLiftInverts {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.IsEquivalence (CategoryTheory.Localization.Construction.lift L (_ : CategoryTheory.MorphismProperty.IsInvertedBy W L))

def CategoryTheory.Localization.equivalenceFromModel {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.MorphismProperty.Localization W ≌ D

A chosen equivalence of categories W.Localization ≅ D for a functor L : C ⥤ D which satisfies L.IsLocalization W. This shall be used in order to deduce properties of L from properties of W.Q.

def CategoryTheory.Localization.qCompEquivalenceFromModelFunctorIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W) (CategoryTheory.Localization.equivalenceFromModel L W).functor ≅ L

Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D, one may identify the functors W.Q and L.

def CategoryTheory.Localization.compEquivalenceFromModelInverseIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Functor.comp L (CategoryTheory.Localization.equivalenceFromModel L W).inverse ≅ CategoryTheory.MorphismProperty.Q W

Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D, one may identify the functors L and W.Q.

theorem CategoryTheory.Localization.essSurj {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.EssSurj L

def CategoryTheory.Localization.whiskeringLeftFunctor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Functor (CategoryTheory.Functor D E) (CategoryTheory.MorphismProperty.FunctorsInverting W E)

The functor (D ⥤ E) ⥤ W.functors_inverting E induced by the composition with a localization functor L : C ⥤ D with respect to W : morphism_property C.

instance CategoryTheory.Localization.instIsEquivalenceFunctorCategoryFunctorsInvertingInstCategoryFunctorsInvertingWhiskeringLeftFunctor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.IsEquivalence (CategoryTheory.Localization.whiskeringLeftFunctor L W E)

def CategoryTheory.Localization.functorEquivalence {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Functor D E ≌ CategoryTheory.MorphismProperty.FunctorsInverting W E

The equivalence of categories (D ⥤ E) ≌ (W.FunctorsInverting E) induced by the composition with a localization functor L : C ⥤ D with respect to W : MorphismProperty C.

def CategoryTheory.Localization.whiskeringLeftFunctor' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (L : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty C → (E : Type u_4) → [inst : CategoryTheory.Category.{u_7, u_4} E] → CategoryTheory.Functor (CategoryTheory.Functor D E) (CategoryTheory.Functor C E)

The functor (D ⥤ E) ⥤ (C ⥤ E) given by the composition with a localization functor L : C ⥤ D with respect to W : MorphismProperty C.

theorem CategoryTheory.Localization.whiskeringLeftFunctor'_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Localization.whiskeringLeftFunctor' L W E = CategoryTheory.Functor.comp (CategoryTheory.Localization.whiskeringLeftFunctor L W E) (CategoryTheory.inducedFunctor CategoryTheory.FullSubcategory.obj)

@[simp]

theorem CategoryTheory.Localization.whiskeringLeftFunctor'_obj {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] (F : CategoryTheory.Functor D E) : (CategoryTheory.Localization.whiskeringLeftFunctor' L W E).obj F = CategoryTheory.Functor.comp L F

instance CategoryTheory.Localization.instFullFunctorCategoryFunctorCategoryWhiskeringLeftFunctor' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Full (CategoryTheory.Localization.whiskeringLeftFunctor' L W E)

instance CategoryTheory.Localization.instFaithfulFunctorCategoryFunctorCategoryWhiskeringLeftFunctor' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Faithful (CategoryTheory.Localization.whiskeringLeftFunctor' L W E)

theorem CategoryTheory.Localization.natTrans_ext {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] [CategoryTheory.Functor.IsLocalization L W] {F₁ : CategoryTheory.Functor D E} {F₂ : CategoryTheory.Functor D E} (τ : F₁ ⟶ F₂) (τ' : F₁ ⟶ F₂) (h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)) : τ = τ'

class CategoryTheory.Localization.Lifting {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E) : Type (max u_1 u_6)

• iso' : CategoryTheory.Functor.comp L F' ≅ F

  the isomorphism relating the localization functor and the two other given functors

When L : C ⥤ D is a localization functor for W : MorphismProperty C and F : C ⥤ E is a functor, we shall say that F' : D ⥤ E lifts F if the obvious diagram is commutative up to an isomorphism.

def CategoryTheory.Localization.Lifting.iso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E) [CategoryTheory.Localization.Lifting L W F F'] : CategoryTheory.Functor.comp L F' ≅ F

The distinguished isomorphism L ⋙ F' ≅ F given by [Lifting L W F F'].

def CategoryTheory.Localization.lift {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (F : CategoryTheory.Functor C E) (hF : CategoryTheory.MorphismProperty.IsInvertedBy W F) (L : CategoryTheory.Functor C D) [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Functor D E

Given a localization functor L : C ⥤ D for W : MorphismProperty C and a functor F : C ⥤ E which inverts W, this is a choice of functor D ⥤ E which lifts F.

instance CategoryTheory.Localization.liftingLift {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (F : CategoryTheory.Functor C E) (hF : CategoryTheory.MorphismProperty.IsInvertedBy W F) (L : CategoryTheory.Functor C D) [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Localization.Lifting L W F (CategoryTheory.Localization.lift F hF L)

def CategoryTheory.Localization.fac {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (F : CategoryTheory.Functor C E) (hF : CategoryTheory.MorphismProperty.IsInvertedBy W F) (L : CategoryTheory.Functor C D) [CategoryTheory.Functor.IsLocalization L W] : CategoryTheory.Functor.comp L (CategoryTheory.Localization.lift F hF L) ≅ F

The canonical isomorphism L ⋙ lift F hF L ≅ F for any functor F : C ⥤ E which inverts W, when L : C ⥤ D is a localization functor for W.

instance CategoryTheory.Localization.liftingConstructionLift {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {W : CategoryTheory.MorphismProperty C} (F : CategoryTheory.Functor C D) (hF : CategoryTheory.MorphismProperty.IsInvertedBy W F) : CategoryTheory.Localization.Lifting (CategoryTheory.MorphismProperty.Q W) W F (CategoryTheory.Localization.Construction.lift F hF)

def CategoryTheory.Localization.liftNatTrans {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] (F₁ : CategoryTheory.Functor C E) (F₂ : CategoryTheory.Functor C E) (F₁' : CategoryTheory.Functor D E) (F₂' : CategoryTheory.Functor D E) [CategoryTheory.Localization.Lifting L W F₁ F₁'] [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 lifts functors (F₁ F₂ : C ⥤ E), a natural transformation τ : F₁ ⟶ F₂ uniquely lifts to a natural transformation F₁' ⟶ F₂'.

@[simp]

theorem CategoryTheory.Localization.liftNatTrans_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] [CategoryTheory.Functor.IsLocalization L W] (F₁ : CategoryTheory.Functor C E) (F₂ : CategoryTheory.Functor C E) (F₁' : CategoryTheory.Functor D E) (F₂' : CategoryTheory.Functor D E) [CategoryTheory.Localization.Lifting L W F₁ F₁'] [CategoryTheory.Localization.Lifting L W F₂ F₂'] (τ : F₁ ⟶ F₂) (X : C) : (CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ).app (L.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.Lifting.iso L W F₁ F₁').hom.app X) (CategoryTheory.CategoryStruct.comp (τ.app X) ((CategoryTheory.Localization.Lifting.iso L W F₂ F₂').inv.app X))

@[simp]

theorem CategoryTheory.Localization.comp_liftNatTrans_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] [CategoryTheory.Functor.IsLocalization L W] (F₁ : CategoryTheory.Functor C E) (F₂ : CategoryTheory.Functor C E) (F₃ : CategoryTheory.Functor C E) (F₁' : CategoryTheory.Functor D E) (F₂' : CategoryTheory.Functor D E) (F₃' : CategoryTheory.Functor D E) [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'] [h₃ : CategoryTheory.Localization.Lifting L W F₃ F₃'] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) {Z : CategoryTheory.Functor D E} (h : F₃' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₂ F₃ F₂' F₃' τ') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₁ F₃ F₁' F₃' (CategoryTheory.CategoryStruct.comp τ τ')) h

@[simp]

theorem CategoryTheory.Localization.comp_liftNatTrans {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] [CategoryTheory.Functor.IsLocalization L W] (F₁ : CategoryTheory.Functor C E) (F₂ : CategoryTheory.Functor C E) (F₃ : CategoryTheory.Functor C E) (F₁' : CategoryTheory.Functor D E) (F₂' : CategoryTheory.Functor D E) (F₃' : CategoryTheory.Functor D E) [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'] [h₃ : CategoryTheory.Localization.Lifting L W F₃ F₃'] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ) (CategoryTheory.Localization.liftNatTrans L W F₂ F₃ F₂' F₃' τ') = CategoryTheory.Localization.liftNatTrans L W F₁ F₃ F₁' F₃' (CategoryTheory.CategoryStruct.comp τ τ')

@[simp]

theorem CategoryTheory.Localization.liftNatTrans_id {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] [CategoryTheory.Functor.IsLocalization L W] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E) [h : CategoryTheory.Localization.Lifting L W F F'] : CategoryTheory.Localization.liftNatTrans L W F F F' F' (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F'

@[simp]

theorem CategoryTheory.Localization.liftNatIso_inv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] (F₁ : CategoryTheory.Functor C E) (F₂ : CategoryTheory.Functor C E) (F₁' : CategoryTheory.Functor D E) (F₂' : CategoryTheory.Functor D E) [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'] (e : F₁ ≅ F₂) : (CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e).inv = CategoryTheory.Localization.liftNatTrans L W F₂ F₁ F₂' F₁' e.inv

@[simp]

theorem CategoryTheory.Localization.liftNatIso_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] (F₁ : CategoryTheory.Functor C E) (F₂ : CategoryTheory.Functor C E) (F₁' : CategoryTheory.Functor D E) (F₂' : CategoryTheory.Functor D E) [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'] (e : F₁ ≅ F₂) : (CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e).hom = CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' e.hom

def CategoryTheory.Localization.liftNatIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Functor.IsLocalization L W] (F₁ : CategoryTheory.Functor C E) (F₂ : CategoryTheory.Functor C E) (F₁' : CategoryTheory.Functor D E) (F₂' : CategoryTheory.Functor D E) [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'] (e : F₁ ≅ F₂) : F₁' ≅ F₂'

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

@[simp]

theorem CategoryTheory.Localization.Lifting.compRight_iso' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_7, u_3} E] {E' : Type u_4} [CategoryTheory.Category.{u_8, u_4} E'] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E) [CategoryTheory.Localization.Lifting L W F F'] (G : CategoryTheory.Functor E E') : CategoryTheory.Localization.Lifting.iso' W = CategoryTheory.isoWhiskerRight (CategoryTheory.Localization.Lifting.iso L W F F') G

instance CategoryTheory.Localization.Lifting.compRight {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_7, u_3} E] {E' : Type u_4} [CategoryTheory.Category.{u_8, u_4} E'] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E) [CategoryTheory.Localization.Lifting L W F F'] (G : CategoryTheory.Functor E E') : CategoryTheory.Localization.Lifting L W (CategoryTheory.Functor.comp F G) (CategoryTheory.Functor.comp F' G)

@[simp]

theorem CategoryTheory.Localization.Lifting.id_iso' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) : CategoryTheory.Localization.Lifting.iso' W = CategoryTheory.Functor.rightUnitor L

instance CategoryTheory.Localization.Lifting.id {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) : CategoryTheory.Localization.Lifting L W L (CategoryTheory.Functor.id D)

@[simp]

theorem CategoryTheory.Localization.Lifting.compLeft_iso' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (F : CategoryTheory.Functor D E) : CategoryTheory.Localization.Lifting.iso' W = CategoryTheory.Iso.refl (CategoryTheory.Functor.comp L F)

instance CategoryTheory.Localization.Lifting.compLeft {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (F : CategoryTheory.Functor D E) : CategoryTheory.Localization.Lifting L W (CategoryTheory.Functor.comp L F) F

@[simp]

theorem CategoryTheory.Localization.Lifting.ofIsos_iso' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] {F₁ : CategoryTheory.Functor C E} {F₂ : CategoryTheory.Functor C E} {F₁' : CategoryTheory.Functor D E} {F₂' : CategoryTheory.Functor D E} (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂') [CategoryTheory.Localization.Lifting L W F₁ F₁'] : CategoryTheory.Localization.Lifting.iso' W = CategoryTheory.isoWhiskerLeft L e'.symm ≪≫ CategoryTheory.Localization.Lifting.iso L W F₁ F₁' ≪≫ e

def CategoryTheory.Localization.Lifting.ofIsos {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] {F₁ : CategoryTheory.Functor C E} {F₂ : CategoryTheory.Functor C E} {F₁' : CategoryTheory.Functor D E} {F₂' : CategoryTheory.Functor D E} (e : F₁ ≅ F₂) (e' : 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₁.

theorem CategoryTheory.Functor.IsLocalization.of_iso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (W : CategoryTheory.MorphismProperty C) {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} (e : L₁ ≅ L₂) [CategoryTheory.Functor.IsLocalization L₁ W] : CategoryTheory.Functor.IsLocalization L₂ W

theorem CategoryTheory.Functor.IsLocalization.of_equivalence_target {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_4} [CategoryTheory.Category.{u_5, u_4} E] (L' : CategoryTheory.Functor C E) (eq : D ≌ E) [CategoryTheory.Functor.IsLocalization L W] (e : CategoryTheory.Functor.comp L eq.functor ≅ L') : CategoryTheory.Functor.IsLocalization L' W

If L : C ⥤ D is a localization for W : MorphismProperty C, then it is also the case of a functor obtained by post-composing L with an equivalence of categories.

def CategoryTheory.Localization.uniq {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L₁ W'] [CategoryTheory.Functor.IsLocalization L₂ W'] : D₁ ≌ D₂

If L₁ : C ⥤ D₁ and L₂ : C ⥤ D₂ are two localization functors for the same MorphismProperty C, this is an equivalence of categories D₁ ≌ D₂.

theorem CategoryTheory.Localization.uniq_symm {C : Type u_1} [CategoryTheory.Category.{u_8, u_1} C] {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{u_6, u_4} D₁] [CategoryTheory.Category.{u_7, u_5} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L₁ W'] [CategoryTheory.Functor.IsLocalization L₂ W'] : (CategoryTheory.Localization.uniq L₁ L₂ W').symm = CategoryTheory.Localization.uniq L₂ L₁ W'

def CategoryTheory.Localization.compUniqFunctor {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L₁ W'] [CategoryTheory.Functor.IsLocalization L₂ W'] : CategoryTheory.Functor.comp L₁ (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.

def CategoryTheory.Localization.compUniqInverse {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L₁ W'] [CategoryTheory.Functor.IsLocalization L₂ W'] : CategoryTheory.Functor.comp L₂ (CategoryTheory.Localization.uniq L₁ L₂ W').inverse ≅ L₁

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

instance CategoryTheory.Localization.instLiftingFunctorUniq {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L₁ W'] [CategoryTheory.Functor.IsLocalization L₂ W'] : CategoryTheory.Localization.Lifting L₁ W' L₂ (CategoryTheory.Localization.uniq L₁ L₂ W').functor

instance CategoryTheory.Localization.instLiftingInverseUniq {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L₁ W'] [CategoryTheory.Functor.IsLocalization L₂ W'] : CategoryTheory.Localization.Lifting L₂ W' L₁ (CategoryTheory.Localization.uniq L₁ L₂ W').inverse

def CategoryTheory.Localization.isoUniqFunctor {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L₁ W'] [CategoryTheory.Functor.IsLocalization L₂ W'] (F : CategoryTheory.Functor D₁ D₂) (e : CategoryTheory.Functor.comp L₁ F ≅ L₂) : F ≅ (CategoryTheory.Localization.uniq L₁ L₂ W').functor

If L₁ : C ⥤ D₁ and L₂ : C ⥤ D₂ are two localization functors for the same MorphismProperty C, any functor F : D₁ ⥤ D₂ equipped with an isomorphism L₁ ⋙ F ≅ L₂ is isomorphic to the functor of the equivalence given by uniq.