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 factor 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) : Prop

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.

• inverts : W.IsInvertedBy L

  the functor inverts the given MorphismProperty

• isEquivalence : (Localization.Construction.lift L ⋯).IsEquivalence

  the induced functor from the constructed localized category is an equivalence

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

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

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

• inverts : W.IsInvertedBy L

  the functor L inverts W

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

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

• fac (F : Functor C E) (hF : W.IsInvertedBy F) : L.comp (self.lift F hF) = F

  there is a factorisation involving the lifted functor

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

  uniqueness of the lifted functor

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

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

@[simp]

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Localization.instInhabitedStrictUniversalPropertyFixedTargetLocalizationQ {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) (E : Type u_3) [Category.{v_3, u_3} E] : Inhabited (StrictUniversalPropertyFixedTarget W.Q W E)

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

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

@[simp]

theorem CategoryTheory.Localization.strictUniversalPropertyFixedTargetId_lift {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) (E : Type u_3) [Category.{v_3, u_3} E] (hW : W ≤ MorphismProperty.isomorphisms C) (F : Functor C E) (x✝ : W.IsInvertedBy F) : (strictUniversalPropertyFixedTargetId W E hW).lift F x✝ = F

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

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

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

noncomputable def CategoryTheory.Localization.isoOfHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W 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.

@[simp]

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

@[simp]

theorem CategoryTheory.Localization.isoOfHom_hom_inv_id {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f) : CategoryStruct.comp (L.map f) (isoOfHom L W f hf).inv = CategoryStruct.id (L.obj X)

@[simp]

theorem CategoryTheory.Localization.isoOfHom_hom_inv_id_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f) {Z : D} (h : L.obj X ⟶ Z) : CategoryStruct.comp (L.map f) (CategoryStruct.comp (isoOfHom L W f hf).inv h) = h

@[simp]

theorem CategoryTheory.Localization.isoOfHom_inv_hom_id {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f) : CategoryStruct.comp (isoOfHom L W f hf).inv (L.map f) = CategoryStruct.id (L.obj Y)

@[simp]

theorem CategoryTheory.Localization.isoOfHom_inv_hom_id_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f) {Z : D} (h : L.obj Y ⟶ Z) : CategoryStruct.comp (isoOfHom L W f hf).inv (CategoryStruct.comp (L.map f) h) = h

@[simp]

theorem CategoryTheory.Localization.isoOfHom_id_inv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (X : C) (hX : W (CategoryStruct.id X)) : (isoOfHom L W (CategoryStruct.id X) hX).inv = CategoryStruct.id (L.obj X)

theorem CategoryTheory.Localization.Construction.wIso_eq_isoOfHom {C : Type u_1} [Category.{v_1, u_1} C] {W : MorphismProperty C} {X Y : C} (f : X ⟶ Y) (hf : W f) : wIso f hf = isoOfHom W.Q W f hf

theorem CategoryTheory.Localization.Construction.wInv_eq_isoOfHom_inv {C : Type u_1} [Category.{v_1, u_1} C] {W : MorphismProperty C} {X Y : C} (f : X ⟶ Y) (hf : W f) : wInv f hf = (isoOfHom W.Q W f hf).inv

instance CategoryTheory.Localization.instIsEquivalenceLocalizationLift {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) {W : MorphismProperty C} [L.IsLocalization W] : (Construction.lift L ⋯).IsEquivalence

noncomputable def CategoryTheory.Localization.equivalenceFromModel {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] : W.Localization ≌ 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.

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

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

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

Via the equivalence of categories equivalenceFromModel 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] : L.EssSurj

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

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

instance CategoryTheory.Localization.instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) (E : Type u_3) [Category.{v_3, u_3} E] [L.IsLocalization W] : (whiskeringLeftFunctor L W E).IsEquivalence

noncomputable def CategoryTheory.Localization.functorEquivalence {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) (E : Type u_3) [Category.{v_3, u_3} E] [L.IsLocalization W] : Functor D E ≌ W.FunctorsInverting 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (E : Type u_4) [Category.{v_4, u_4} E] : Functor (Functor D E) (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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) (E : Type u_3) [Category.{v_3, u_3} E] [L.IsLocalization W] : whiskeringLeftFunctor' L W E = (whiskeringLeftFunctor L W E).comp (inducedFunctor ObjectProperty.FullSubcategory.obj)

@[simp]

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

instance CategoryTheory.Localization.instFullFunctorWhiskeringLeftFunctor' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) (E : Type u_3) [Category.{v_3, u_3} E] [L.IsLocalization W] : (whiskeringLeftFunctor' L W E).Full

instance CategoryTheory.Localization.instFaithfulFunctorWhiskeringLeftFunctor' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) (E : Type u_3) [Category.{v_3, u_3} E] [L.IsLocalization W] : (whiskeringLeftFunctor' L W E).Faithful

theorem CategoryTheory.Localization.full_whiskeringLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (E : Type u_4) [Category.{v_4, u_4} E] : ((Functor.whiskeringLeft C D E).obj L).Full

theorem CategoryTheory.Localization.faithful_whiskeringLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (E : Type u_4) [Category.{v_4, u_4} E] : ((Functor.whiskeringLeft C D E).obj L).Faithful

noncomputable def CategoryTheory.Localization.fullyFaithfulWhiskeringLeft {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (E : Type u_4) [Category.{v_4, u_4} E] : ((Functor.whiskeringLeft C D E).obj L).FullyFaithful

The precomposition with a localization functor gives fully faithful functors between functor categories.

theorem CategoryTheory.Localization.natTrans_ext {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {F₁ F₂ : Functor D E} {τ τ' : 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (L : Functor C D) (W : MorphismProperty C) (F : Functor C E) (F' : Functor D E) : Type (max u_1 v_3)

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.

• iso : L.comp F' ≅ F

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

noncomputable def CategoryTheory.Localization.lift {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {W : MorphismProperty C} {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C E) (hF : W.IsInvertedBy F) (L : Functor C D) [L.IsLocalization W] : 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.

@[implicit_reducible]

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

noncomputable def CategoryTheory.Localization.fac {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {W : MorphismProperty C} {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C E) (hF : W.IsInvertedBy F) (L : Functor C D) [L.IsLocalization W] : L.comp (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.

@[implicit_reducible]

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

noncomputable def CategoryTheory.Localization.liftNatTrans {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category.{v_3, u_3} E] [L.IsLocalization W] (F₁ F₂ : Functor C E) (F₁' F₂' : Functor D E) [Lifting L W F₁ F₁'] [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 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category.{v_3, u_3} E] [L.IsLocalization W] (F₁ F₂ : Functor C E) (F₁' F₂' : Functor D E) [Lifting L W F₁ F₁'] [Lifting L W F₂ F₂'] (τ : F₁ ⟶ F₂) (X : C) : (liftNatTrans L W F₁ F₂ F₁' F₂' τ).app (L.obj X) = CategoryStruct.comp ((Lifting.iso L W F₁ F₁').hom.app X) (CategoryStruct.comp (τ.app X) ((Lifting.iso L W F₂ F₂').inv.app X))

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Localization.liftNatIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category.{v_3, u_3} E] [L.IsLocalization W] (F₁ F₂ : Functor C E) (F₁' F₂' : Functor D E) [h₁ : Lifting L W F₁ F₁'] [h₂ : 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 lift functors (F₁ F₂ : C ⥤ E), a natural isomorphism τ : F₁ ⟶ F₂ lifts to a natural isomorphism F₁' ⟶ F₂'.

@[simp]

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

@[simp]

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

@[implicit_reducible]

instance CategoryTheory.Localization.Lifting.compRight {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category.{v_3, u_3} E] {E' : Type u_4} [Category.{v_4, u_4} E'] (F : Functor C E) (F' : Functor D E) [Lifting L W F F'] (G : Functor E E') : Lifting L W (F.comp G) (F'.comp G)

@[simp]

theorem CategoryTheory.Localization.Lifting.compRight_iso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category.{v_3, u_3} E] {E' : Type u_4} [Category.{v_4, u_4} E'] (F : Functor C E) (F' : Functor D E) [Lifting L W F F'] (G : Functor E E') : iso L W (F.comp G) (F'.comp G) = Functor.isoWhiskerRight (iso L W F F') G

@[implicit_reducible]

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

@[simp]

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

@[implicit_reducible]

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

@[simp]

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

@[implicit_reducible]

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

@[simp]

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

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

theorem CategoryTheory.Functor.IsLocalization.of_equivalence_target {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_4} [Category.{v_4, u_4} E] (L' : Functor C E) (eq : D ≌ E) [L.IsLocalization W] (e : L.comp eq.functor ≅ L') : L'.IsLocalization 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.

instance CategoryTheory.Functor.IsLocalization.instCompOfIsEquivalence {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) (E : Type u_3) [Category.{v_3, u_3} E] (F : Functor D E) [F.IsEquivalence] [L.IsLocalization W] : (L.comp F).IsLocalization W

theorem CategoryTheory.Functor.IsLocalization.of_isEquivalence {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) (hW : W ≤ MorphismProperty.isomorphisms C) [L.IsEquivalence] : L.IsLocalization W

noncomputable def CategoryTheory.Localization.uniq {C : Type u_1} [Category.{v_1, u_1} C] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (L₁ : Functor C D₁) (L₂ : Functor C D₂) (W' : MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization 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} [Category.{v_1, u_1} C] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (L₁ : Functor C D₁) (L₂ : Functor C D₂) (W' : MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W'] : (uniq L₁ L₂ W').symm = uniq L₂ L₁ W'

noncomputable def CategoryTheory.Localization.compUniqFunctor {C : Type u_1} [Category.{v_1, u_1} C] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (L₁ : Functor C D₁) (L₂ : Functor C D₂) (W' : MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W'] : L₁.comp (uniq L₁ L₂ W').functor ≅ L₂

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

noncomputable def CategoryTheory.Localization.isoUniqFunctor {C : Type u_1} [Category.{v_1, u_1} C] {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (L₁ : Functor C D₁) (L₂ : Functor C D₂) (W' : MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W'] (F : Functor D₁ D₂) (e : L₁.comp F ≅ L₂) : F ≅ (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.

theorem CategoryTheory.Localization.morphismProperty_eq_top {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (P : MorphismProperty D) [P.RespectsIso] [P.IsMultiplicative] (h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)) (h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv) : P = ⊤

theorem CategoryTheory.Localization.isGroupoid {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [L.IsLocalization ⊤] : IsGroupoid D

instance CategoryTheory.Localization.instIsGroupoidLocalizationTopMorphismProperty {C : Type u_1} [Category.{v_1, u_1} C] : IsGroupoid ⊤.Localization

@[implicit_reducible]

noncomputable def CategoryTheory.Localization.groupoid {C : Type u_1} [Category.{v_1, u_1} C] : Groupoid ⊤.Localization

Localization of a category with respect to all morphisms results in a groupoid.

def CategoryTheory.AreEqualizedByLocalization {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) {X Y : C} (f g : X ⟶ Y) : Prop

The property that two morphisms become equal in the localized category.

theorem CategoryTheory.areEqualizedByLocalization_iff {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) (W : MorphismProperty C) {X Y : C} (f g : X ⟶ Y) [L.IsLocalization W] : AreEqualizedByLocalization W f g ↔ L.map f = L.map g

theorem CategoryTheory.AreEqualizedByLocalization.mk {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (W : MorphismProperty C) {X Y : C} (f g : X ⟶ Y) (L : Functor C D) [L.IsLocalization W] (h : L.map f = L.map g) : AreEqualizedByLocalization W f g

theorem CategoryTheory.AreEqualizedByLocalization.map_eq {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {W : MorphismProperty C} {X Y : C} {f g : X ⟶ Y} (h : AreEqualizedByLocalization W f g) (L : Functor C D) [L.IsLocalization W] : L.map f = L.map g

theorem CategoryTheory.AreEqualizedByLocalization.map_eq_of_isInvertedBy {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {W : MorphismProperty C} {X Y : C} {f g : X ⟶ Y} (h : AreEqualizedByLocalization W f g) (F : Functor C D) (hF : W.IsInvertedBy F) : F.map f = F.map g