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)
:
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 : (CategoryTheory.Localization.Construction.lift L ⋯).IsEquivalence
the induced functor from the constructed localized category is an equivalence
Instances
theorem
CategoryTheory.Functor.IsLocalization.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}
[self : L.IsLocalization W]
:
W.IsInvertedBy L
the functor inverts the given MorphismProperty
theorem
CategoryTheory.Functor.IsLocalization.isEquivalence
{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}
[self : L.IsLocalization W]
:
(CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} C]
(W : CategoryTheory.MorphismProperty C)
:
W.Q.IsLocalization W
Equations
- ⋯ = ⋯
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)
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
LinvertsW - lift : (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → CategoryTheory.Functor D E
any functor
C ⥤ Ewhich invertsWcan be lifted as a functorD ⥤ E - fac : ∀ (F : CategoryTheory.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₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂ → F₁ = F₂
uniqueness of the lifted functor
Instances For
theorem
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.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}
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
(self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E)
:
W.IsInvertedBy L
the functor L inverts W
theorem
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac
{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]
(self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E)
(F : CategoryTheory.Functor C E)
(hF : W.IsInvertedBy F)
:
L.comp (self.lift F hF) = F
there is a factorisation involving the lifted functor
theorem
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.uniq
{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]
(self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E)
(F₁ : CategoryTheory.Functor D E)
(F₂ : CategoryTheory.Functor D E)
:
uniqueness of the lifted functor
@[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 : W.IsInvertedBy G)
:
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]
:
The localized category W.Localization that was constructed satisfies
the universal property of the localization.
Equations
- CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ W E = { inverts := ⋯, lift := CategoryTheory.Localization.Construction.lift, fac := ⋯, uniq := ⋯ }
Instances For
instance
CategoryTheory.Localization.instInhabitedStrictUniversalPropertyFixedTargetLocalizationQ
{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]
:
@[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 : W.IsInvertedBy F), (CategoryTheory.Localization.strictUniversalPropertyFixedTargetId W E hW).lift 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)
:
When W consists of isomorphisms, the identity satisfies the universal property
of the localization.
Equations
- CategoryTheory.Localization.strictUniversalPropertyFixedTargetId W E hW = { inverts := ⋯, lift := fun (F : CategoryTheory.Functor C E) (x : W.IsInvertedBy F) => F, fac := ⋯, uniq := ⋯ }
Instances For
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 W.Localization)
:
L.IsLocalization 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.id C).IsLocalization 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)
[L.IsLocalization W]
:
W.IsInvertedBy L
@[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)
[L.IsLocalization W]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W 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)
[L.IsLocalization W]
{X : C}
{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.
Equations
- CategoryTheory.Localization.isoOfHom L W f hf = CategoryTheory.asIso (L.map f)
Instances For
@[simp]
theorem
CategoryTheory.Localization.isoOfHom_hom_inv_id_assoc
{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)
[L.IsLocalization W]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W f)
{Z : D}
(h : L.obj X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (L.map f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W f hf).inv h) = h
@[simp]
theorem
CategoryTheory.Localization.isoOfHom_hom_inv_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)
[L.IsLocalization W]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W f)
:
CategoryTheory.CategoryStruct.comp (L.map f) (CategoryTheory.Localization.isoOfHom L W f hf).inv = CategoryTheory.CategoryStruct.id (L.obj X)
@[simp]
theorem
CategoryTheory.Localization.isoOfHom_inv_hom_id_assoc
{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)
[L.IsLocalization W]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W f)
{Z : D}
(h : L.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W f hf).inv
(CategoryTheory.CategoryStruct.comp (L.map f) h) = h
@[simp]
theorem
CategoryTheory.Localization.isoOfHom_inv_hom_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)
[L.IsLocalization W]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W f)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W f hf).inv (L.map f) = CategoryTheory.CategoryStruct.id (L.obj Y)
@[simp]
theorem
CategoryTheory.Localization.isoOfHom_id_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)
[L.IsLocalization W]
(X : C)
(hX : W (CategoryTheory.CategoryStruct.id X))
:
(CategoryTheory.Localization.isoOfHom L W (CategoryTheory.CategoryStruct.id X) hX).inv = CategoryTheory.CategoryStruct.id (L.obj X)
theorem
CategoryTheory.Localization.Construction.wIso_eq_isoOfHom
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W f)
:
theorem
CategoryTheory.Localization.Construction.wInv_eq_isoOfHom_inv
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W f)
:
CategoryTheory.Localization.Construction.wInv f hf = (CategoryTheory.Localization.isoOfHom W.Q W f hf).inv
instance
CategoryTheory.Localization.instIsEquivalenceLocalizationLift
{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}
[L.IsLocalization W]
:
(CategoryTheory.Localization.Construction.lift L ⋯).IsEquivalence
Equations
- ⋯ = ⋯
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)
[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.
Equations
- CategoryTheory.Localization.equivalenceFromModel L W = (CategoryTheory.Localization.Construction.lift L ⋯).asEquivalence
Instances For
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)
[L.IsLocalization W]
:
W.Q.comp (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.
Equations
Instances For
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)
[L.IsLocalization W]
:
L.comp (CategoryTheory.Localization.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.
Instances For
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)
[L.IsLocalization W]
:
L.EssSurj
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]
[L.IsLocalization W]
:
CategoryTheory.Functor (CategoryTheory.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.
Instances For
instance
CategoryTheory.Localization.instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, 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_4, u_3} E]
[L.IsLocalization W]
:
(CategoryTheory.Localization.whiskeringLeftFunctor L W E).IsEquivalence
Equations
- ⋯ = ⋯
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]
[L.IsLocalization W]
:
CategoryTheory.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
- CategoryTheory.Localization.functorEquivalence L W E = (CategoryTheory.Localization.whiskeringLeftFunctor L W E).asEquivalence
Instances For
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.
Equations
- CategoryTheory.Localization.whiskeringLeftFunctor' L x E = (CategoryTheory.whiskeringLeft C D E).obj L
Instances For
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]
[L.IsLocalization W]
:
CategoryTheory.Localization.whiskeringLeftFunctor' L W E = (CategoryTheory.Localization.whiskeringLeftFunctor L W E).comp
(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 = L.comp F
instance
CategoryTheory.Localization.instFullFunctorWhiskeringLeftFunctor'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, 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_4, u_3} E]
[L.IsLocalization W]
:
(CategoryTheory.Localization.whiskeringLeftFunctor' L W E).Full
Equations
- ⋯ = ⋯
instance
CategoryTheory.Localization.instFaithfulFunctorWhiskeringLeftFunctor'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, 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_4, u_3} E]
[L.IsLocalization W]
:
(CategoryTheory.Localization.whiskeringLeftFunctor' L W E).Faithful
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Localization.full_whiskeringLeft
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, 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_4, u_3} E]
[L.IsLocalization W]
:
((CategoryTheory.whiskeringLeft C D E).obj L).Full
theorem
CategoryTheory.Localization.faithful_whiskeringLeft
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, 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_4, u_3} E]
[L.IsLocalization W]
:
((CategoryTheory.whiskeringLeft C D E).obj L).Faithful
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]
[L.IsLocalization 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)
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
Instances
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']
:
L.comp F' ≅ F
The distinguished isomorphism L ⋙ F' ≅ F given by [Lifting L W F F'].
Equations
Instances For
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 : W.IsInvertedBy F)
(L : CategoryTheory.Functor C D)
[L.IsLocalization W]
:
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
- CategoryTheory.Localization.lift F hF L = (CategoryTheory.Localization.functorEquivalence L W E).inverse.obj { obj := F, property := hF }
Instances For
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 : W.IsInvertedBy F)
(L : CategoryTheory.Functor C D)
[L.IsLocalization W]
:
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}
[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 : W.IsInvertedBy F)
(L : CategoryTheory.Functor C D)
[L.IsLocalization W]
:
L.comp (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.
Equations
Instances For
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 : W.IsInvertedBy F)
:
Equations
- CategoryTheory.Localization.liftingConstructionLift F hF = { iso' := CategoryTheory.eqToIso ⋯ }
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]
[L.IsLocalization 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₂'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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]
[L.IsLocalization 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]
[L.IsLocalization 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]
[L.IsLocalization 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]
[L.IsLocalization W]
(F : CategoryTheory.Functor C E)
(F' : CategoryTheory.Functor D E)
[h : CategoryTheory.Localization.Lifting L W F F']
:
@[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]
[L.IsLocalization 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
@[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]
[L.IsLocalization 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
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]
[L.IsLocalization 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₂'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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')
:
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 (F.comp G) (F'.comp G)
Equations
- CategoryTheory.Localization.Lifting.compRight L W F F' G = { iso' := CategoryTheory.isoWhiskerRight (CategoryTheory.Localization.Lifting.iso L W F 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 = L.rightUnitor
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)
:
Equations
- CategoryTheory.Localization.Lifting.id L W = { iso' := L.rightUnitor }
@[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)
:
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 (L.comp F) F
Equations
- CategoryTheory.Localization.Lifting.compLeft L W F = { iso' := CategoryTheory.Iso.refl (L.comp F) }
@[simp]
theorem
CategoryTheory.Localization.Lifting.compLeft_iso
{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.Lifting.iso L W (L.comp F) F = CategoryTheory.Iso.refl (L.comp 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₁.
Equations
- CategoryTheory.Localization.Lifting.ofIsos L W e e' = { iso' := CategoryTheory.isoWhiskerLeft L e'.symm ≪≫ CategoryTheory.Localization.Lifting.iso L W F₁ F₁' ≪≫ e }
Instances For
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₂)
[L₁.IsLocalization W]
:
L₂.IsLocalization 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)
[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}
[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)
[F.IsEquivalence]
[L.IsLocalization W]
:
(L.comp F).IsLocalization W
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Functor.IsLocalization.of_isEquivalence
{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)
(hW : W ≤ CategoryTheory.MorphismProperty.isomorphisms C)
[L.IsEquivalence]
:
L.IsLocalization W
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)
[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₂.
Equations
- CategoryTheory.Localization.uniq L₁ L₂ W' = (CategoryTheory.Localization.equivalenceFromModel L₁ W').symm.trans (CategoryTheory.Localization.equivalenceFromModel L₂ W')
Instances For
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)
[L₁.IsLocalization W']
[L₂.IsLocalization 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)
[L₁.IsLocalization W']
[L₂.IsLocalization W']
:
L₁.comp (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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
[L₁.IsLocalization W']
[L₂.IsLocalization W']
:
L₂.comp (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.
Equations
Instances For
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)
[L₁.IsLocalization W']
[L₂.IsLocalization W']
:
CategoryTheory.Localization.Lifting L₁ W' L₂ (CategoryTheory.Localization.uniq L₁ L₂ W').functor
Equations
- CategoryTheory.Localization.instLiftingFunctorUniq L₁ L₂ W' = { iso' := CategoryTheory.Localization.compUniqFunctor L₁ L₂ W' }
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)
[L₁.IsLocalization W']
[L₂.IsLocalization W']
:
CategoryTheory.Localization.Lifting L₂ W' L₁ (CategoryTheory.Localization.uniq L₁ L₂ W').inverse
Equations
- CategoryTheory.Localization.instLiftingInverseUniq L₁ L₂ W' = { iso' := CategoryTheory.Localization.compUniqInverse L₁ L₂ W' }
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)
[L₁.IsLocalization W']
[L₂.IsLocalization W']
(F : CategoryTheory.Functor D₁ D₂)
(e : L₁.comp 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.
Equations
- CategoryTheory.Localization.isoUniqFunctor L₁ L₂ W' F e = CategoryTheory.Localization.liftNatIso L₁ W' L₂ L₂ F (CategoryTheory.Localization.uniq L₁ L₂ W').functor (CategoryTheory.Iso.refl L₂)
Instances For
def
CategoryTheory.AreEqualizedByLocalization
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
The property that two morphisms become equal in the localized category.
Equations
- CategoryTheory.AreEqualizedByLocalization W f g = (W.Q.map f = W.Q.map g)
Instances For
theorem
CategoryTheory.areEqualizedByLocalization_iff
{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)
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[L.IsLocalization W]
:
CategoryTheory.AreEqualizedByLocalization W f g ↔ L.map f = L.map g
theorem
CategoryTheory.AreEqualizedByLocalization.mk
{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)
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
(L : CategoryTheory.Functor C D)
[L.IsLocalization W]
(h : L.map f = L.map g)
:
theorem
CategoryTheory.AreEqualizedByLocalization.map_eq
{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}
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(h : CategoryTheory.AreEqualizedByLocalization W f g)
(L : CategoryTheory.Functor C D)
[L.IsLocalization W]
:
L.map f = L.map g