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.

structure CategoryTheory.Functor.IsLocalization {C : Type u_1} {D : Type u_2} [Category C] [Category 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

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

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

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.

• 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) : Eq (L.comp (self.lift F hF)) F

  there is a factorisation involving the lifted functor

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

  uniqueness of the lifted functor

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

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

Equations

• Eq (CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ W E) { inverts := ⋯, lift := CategoryTheory.Localization.Construction.lift, fac := ⋯, uniq := ⋯ }

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

def CategoryTheory.Localization.instInhabitedStrictUniversalPropertyFixedTargetLocalizationQ {C : Type u_1} [Category C] (W : MorphismProperty C) (E : Type u_3) [Category E] : Inhabited (StrictUniversalPropertyFixedTarget W.Q W E)

Equations

• Eq (CategoryTheory.Localization.instInhabitedStrictUniversalPropertyFixedTargetLocalizationQ W E) { default := CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ W E }

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

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

Equations

• Eq (CategoryTheory.Localization.strictUniversalPropertyFixedTargetId W E hW) { inverts := ⋯, lift := fun (F : CategoryTheory.Functor C E) (x : W.IsInvertedBy F) => F, fac := ⋯, uniq := ⋯ }

theorem CategoryTheory.Localization.strictUniversalPropertyFixedTargetId_lift {C : Type u_1} [Category C] (W : MorphismProperty C) (E : Type u_3) [Category E] (hW : LE.le W (MorphismProperty.isomorphisms C)) (F : Functor C E) (x✝ : W.IsInvertedBy F) : Eq ((strictUniversalPropertyFixedTargetId W E hW).lift F x✝) F

theorem CategoryTheory.Functor.IsLocalization.mk' {C : Type u_1} {D : Type u_2} [Category C] [Category 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 C] (W : MorphismProperty C) (hW : LE.le W (MorphismProperty.isomorphisms C)) : (Functor.id C).IsLocalization W

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

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

Equations

• Eq (CategoryTheory.Localization.isoOfHom L W f hf) (CategoryTheory.asIso (L.map f))

theorem CategoryTheory.Localization.isoOfHom_hom {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {X Y : C} (f : Quiver.Hom X Y) (hf : W f) : Eq (isoOfHom L W f hf).hom (L.map f)

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

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

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

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

theorem CategoryTheory.Localization.isoOfHom_id_inv {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (X : C) (hX : W (CategoryStruct.id X)) : Eq (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 C] {W : MorphismProperty C} {X Y : C} (f : Quiver.Hom X Y) (hf : W f) : Eq (wIso f hf) (isoOfHom W.Q W f hf)

theorem CategoryTheory.Localization.Construction.wInv_eq_isoOfHom_inv {C : Type u_1} [Category C] {W : MorphismProperty C} {X Y : C} (f : Quiver.Hom X Y) (hf : W f) : Eq (wInv f hf) (isoOfHom W.Q W f hf).inv

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

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

Equations

• Eq (CategoryTheory.Localization.equivalenceFromModel L W) (CategoryTheory.Localization.Construction.lift L ⋯).asEquivalence

def CategoryTheory.Localization.qCompEquivalenceFromModelFunctorIso {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] : Iso (W.Q.comp (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.

Equations

• Eq (CategoryTheory.Localization.qCompEquivalenceFromModelFunctorIso L W) (CategoryTheory.eqToIso ⋯)

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Localization.essSurj {C : Type u_1} {D : Type u_2} [Category C] [Category 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 C] [Category D] (L : Functor C D) (W : MorphismProperty C) (E : Type u_3) [Category 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 : morphism_property C.

Equations

• One or more equations did not get rendered due to their size.

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

def CategoryTheory.Localization.functorEquivalence {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) (E : Type u_3) [Category E] [L.IsLocalization W] : Equivalence (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.

Equations

• Eq (CategoryTheory.Localization.functorEquivalence L W E) (CategoryTheory.Localization.whiskeringLeftFunctor L W E).asEquivalence

def CategoryTheory.Localization.whiskeringLeftFunctor' {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (E : Type u_4) [Category 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.

Equations

• Eq (CategoryTheory.Localization.whiskeringLeftFunctor' L W E) ((CategoryTheory.whiskeringLeft C D E).obj L)

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

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

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

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

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

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

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

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

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' : Iso (L.comp F') F

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

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

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

Equations

• Eq (CategoryTheory.Localization.Lifting.iso L W F F') (CategoryTheory.Localization.Lifting.iso' W)

def CategoryTheory.Localization.lift {C : Type u_1} {D : Type u_2} [Category C] [Category D] {W : MorphismProperty C} {E : Type u_3} [Category 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.

Equations

• Eq (CategoryTheory.Localization.lift F hF L) ((CategoryTheory.Localization.functorEquivalence L W E).inverse.obj { obj := F, property := hF })

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Eq (CategoryTheory.Localization.fac F hF L) (CategoryTheory.Localization.Lifting.iso L W F (CategoryTheory.Localization.lift F hF L))

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

Equations

• Eq (CategoryTheory.Localization.liftingConstructionLift F hF) { iso' := CategoryTheory.eqToIso ⋯ }

def CategoryTheory.Localization.liftNatTrans {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category E] [L.IsLocalization W] (F₁ F₂ : Functor C E) (F₁' F₂' : Functor D E) [Lifting L W F₁ F₁'] [Lifting L W F₂ F₂'] (τ : Quiver.Hom F₁ F₂) : Quiver.Hom 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₂'.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Localization.liftNatTrans_app {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category E] [L.IsLocalization W] (F₁ F₂ : Functor C E) (F₁' F₂' : Functor D E) [Lifting L W F₁ F₁'] [Lifting L W F₂ F₂'] (τ : Quiver.Hom F₁ F₂) (X : C) : Eq ((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)))

theorem CategoryTheory.Localization.comp_liftNatTrans {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category 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₃'] (τ : Quiver.Hom F₁ F₂) (τ' : Quiver.Hom F₂ F₃) : Eq (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 τ τ'))

theorem CategoryTheory.Localization.comp_liftNatTrans_assoc {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category 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₃'] (τ : Quiver.Hom F₁ F₂) (τ' : Quiver.Hom F₂ F₃) {Z : Functor D E} (h : Quiver.Hom F₃' Z) : Eq (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)

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

def CategoryTheory.Localization.liftNatIso {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category 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 : Iso F₁ F₂) : Iso 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₂'.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Localization.liftNatIso_inv {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category 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 : Iso F₁ F₂) : Eq (liftNatIso L W F₁ F₂ F₁' F₂' e).inv (liftNatTrans L W F₂ F₁ F₂' F₁' e.inv)

theorem CategoryTheory.Localization.liftNatIso_hom {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category 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 : Iso F₁ F₂) : Eq (liftNatIso L W F₁ F₂ F₁' F₂' e).hom (liftNatTrans L W F₁ F₂ F₁' F₂' e.hom)

def CategoryTheory.Localization.Lifting.compRight {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category E] {E' : Type u_4} [Category 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)

Equations

• Eq (CategoryTheory.Localization.Lifting.compRight L W F F' G) { iso' := CategoryTheory.isoWhiskerRight (CategoryTheory.Localization.Lifting.iso L W F F') G }

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

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

Equations

• Eq (CategoryTheory.Localization.Lifting.id L W) { iso' := L.rightUnitor }

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

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

Equations

• Eq (CategoryTheory.Localization.Lifting.compLeft L W F) { iso' := CategoryTheory.Iso.refl (L.comp F) }

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

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

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

Equations

• Eq (CategoryTheory.Localization.Lifting.ofIsos L W e e') { iso' := (CategoryTheory.isoWhiskerLeft L e'.symm).trans ((CategoryTheory.Localization.Lifting.iso L W F₁ F₁').trans e) }

theorem CategoryTheory.Localization.Lifting.ofIsos_iso' {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_3} [Category E] {F₁ F₂ : Functor C E} {F₁' F₂' : Functor D E} (e : Iso F₁ F₂) (e' : Iso F₁' F₂') [Lifting L W F₁ F₁'] : Eq (iso' W) ((isoWhiskerLeft L e'.symm).trans ((iso L W F₁ F₁').trans e))

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

theorem CategoryTheory.Functor.IsLocalization.of_equivalence_target {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {E : Type u_4} [Category E] (L' : Functor C E) (eq : Equivalence D E) [L.IsLocalization W] (e : Iso (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.

theorem CategoryTheory.Functor.IsLocalization.instCompOfIsEquivalence {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) (E : Type u_3) [Category 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 C] [Category D] (L : Functor C D) (W : MorphismProperty C) (hW : LE.le W (MorphismProperty.isomorphisms C)) [L.IsEquivalence] : L.IsLocalization W

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

Equations

• Eq (CategoryTheory.Localization.uniq L₁ L₂ W') ((CategoryTheory.Localization.equivalenceFromModel L₁ W').symm.trans (CategoryTheory.Localization.equivalenceFromModel L₂ W'))

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Eq (CategoryTheory.Localization.compUniqInverse L₁ L₂ W') (CategoryTheory.Localization.compUniqFunctor L₂ L₁ W')

def CategoryTheory.Localization.instLiftingFunctorUniq {C : Type u_1} [Category C] {D₁ : Type u_5} {D₂ : Type u_6} [Category D₁] [Category 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

Equations

• Eq (CategoryTheory.Localization.instLiftingFunctorUniq L₁ L₂ W') { iso' := CategoryTheory.Localization.compUniqFunctor L₁ L₂ W' }

def CategoryTheory.Localization.instLiftingInverseUniq {C : Type u_1} [Category C] {D₁ : Type u_5} {D₂ : Type u_6} [Category D₁] [Category 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

Equations

• Eq (CategoryTheory.Localization.instLiftingInverseUniq L₁ L₂ W') { iso' := CategoryTheory.Localization.compUniqInverse L₁ L₂ W' }

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Eq (CategoryTheory.AreEqualizedByLocalization W f g) (Eq (W.Q.map f) (W.Q.map g))

theorem CategoryTheory.areEqualizedByLocalization_iff {C : Type u_1} {D : Type u_2} [Category C] [Category D] (L : Functor C D) (W : MorphismProperty C) {X Y : C} (f g : Quiver.Hom X Y) [L.IsLocalization W] : Iff (AreEqualizedByLocalization W f g) (Eq (L.map f) (L.map g))

theorem CategoryTheory.AreEqualizedByLocalization.mk {C : Type u_1} {D : Type u_2} [Category C] [Category D] (W : MorphismProperty C) {X Y : C} (f g : Quiver.Hom X Y) (L : Functor C D) [L.IsLocalization W] (h : Eq (L.map f) (L.map g)) : AreEqualizedByLocalization W f g

theorem CategoryTheory.AreEqualizedByLocalization.map_eq {C : Type u_1} {D : Type u_2} [Category C] [Category D] {W : MorphismProperty C} {X Y : C} {f g : Quiver.Hom X Y} (h : AreEqualizedByLocalization W f g) (L : Functor C D) [L.IsLocalization W] : Eq (L.map f) (L.map g)