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 : CategoryTheory.MorphismProperty.IsInvertedBy W L
the functor inverts the given
MorphismProperty - nonempty_isEquivalence : Nonempty (CategoryTheory.IsEquivalence (CategoryTheory.Localization.Construction.lift L (_ : CategoryTheory.MorphismProperty.IsInvertedBy W L)))
the induced functor from the constructed localized category is an equivalence
Instances
instance
CategoryTheory.Functor.q_isLocalization
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
(W : CategoryTheory.MorphismProperty C)
:
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 : CategoryTheory.MorphismProperty.IsInvertedBy W L
the functor
LinvertsW - lift : (F : CategoryTheory.Functor C E) → CategoryTheory.MorphismProperty.IsInvertedBy W F → CategoryTheory.Functor D E
any functor
C ⥤ Ewhich invertsWcan be lifted as a functorD ⥤ E - fac : ∀ (F : CategoryTheory.Functor C E) (hF : CategoryTheory.MorphismProperty.IsInvertedBy W F), CategoryTheory.Functor.comp L (self.lift F hF) = F
there is a factorisation involving the lifted functor
- uniq : ∀ (F₁ F₂ : CategoryTheory.Functor D E), CategoryTheory.Functor.comp L F₁ = CategoryTheory.Functor.comp L F₂ → F₁ = F₂
uniqueness of the lifted functor
Instances For
@[simp]
theorem
CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ_lift
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
(W : CategoryTheory.MorphismProperty C)
(E : Type u_3)
[CategoryTheory.Category.{u_5, u_3} E]
(G : CategoryTheory.Functor C E)
(hG : CategoryTheory.MorphismProperty.IsInvertedBy W G)
:
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
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Localization.instInhabitedStrictUniversalPropertyFixedTargetLocalizationInstCategoryLocalizationQ
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
(W : CategoryTheory.MorphismProperty C)
(E : Type u_3)
[CategoryTheory.Category.{u_5, u_3} E]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Localization.strictUniversalPropertyFixedTargetId_lift
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
(W : CategoryTheory.MorphismProperty C)
(E : Type u_3)
[CategoryTheory.Category.{u_5, u_3} E]
(hW : W ⊆ CategoryTheory.MorphismProperty.isomorphisms C)
(F : CategoryTheory.Functor C E)
:
∀ (x : CategoryTheory.MorphismProperty.IsInvertedBy W F),
(CategoryTheory.Localization.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
- One or more equations did not get rendered due to their size.
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 (CategoryTheory.MorphismProperty.Localization W))
:
theorem
CategoryTheory.Localization.inverts
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.Functor.IsLocalization L W]
:
@[simp]
theorem
CategoryTheory.Localization.isoOfHom_inv
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.Functor.IsLocalization L W]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W f)
:
(CategoryTheory.Localization.isoOfHom L W f hf).inv = CategoryTheory.inv (L.toPrefunctor.map f)
@[simp]
theorem
CategoryTheory.Localization.isoOfHom_hom
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.Functor.IsLocalization L W]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W f)
:
(CategoryTheory.Localization.isoOfHom L W f hf).hom = L.toPrefunctor.map f
def
CategoryTheory.Localization.isoOfHom
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.Functor.IsLocalization L W]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : W f)
:
L.toPrefunctor.obj X ≅ L.toPrefunctor.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.toPrefunctor.map f)
Instances For
instance
CategoryTheory.Localization.instIsEquivalenceLocalizationInstCategoryLocalizationLiftInverts
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.Functor.IsLocalization L W]
:
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Localization.equivalenceFromModel
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.Functor.IsLocalization L W]
:
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
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Functor.IsLocalization L W]
:
Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D,
one may identify the functors W.Q and L.
Equations
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Functor.IsLocalization L W]
:
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)
[CategoryTheory.Functor.IsLocalization L W]
:
def
CategoryTheory.Localization.whiskeringLeftFunctor
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
(E : Type u_3)
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
:
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.instIsEquivalenceFunctorCategoryFunctorsInvertingInstCategoryFunctorsInvertingWhiskeringLeftFunctor
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
(E : Type u_3)
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
:
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Localization.functorEquivalence
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
(E : Type u_3)
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
:
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
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).toPrefunctor.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]
[CategoryTheory.Functor.IsLocalization L W]
:
CategoryTheory.Localization.whiskeringLeftFunctor' L W E = CategoryTheory.Functor.comp (CategoryTheory.Localization.whiskeringLeftFunctor L W E)
(CategoryTheory.inducedFunctor CategoryTheory.FullSubcategory.obj)
@[simp]
theorem
CategoryTheory.Localization.whiskeringLeftFunctor'_obj
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
(F : CategoryTheory.Functor D E)
:
(CategoryTheory.Localization.whiskeringLeftFunctor' L W E).toPrefunctor.obj F = CategoryTheory.Functor.comp L F
instance
CategoryTheory.Localization.instFullFunctorCategoryFunctorCategoryWhiskeringLeftFunctor'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Localization.instFaithfulFunctorCategoryFunctorCategoryWhiskeringLeftFunctor'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
:
Equations
theorem
CategoryTheory.Localization.natTrans_ext
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
{F₁ : CategoryTheory.Functor D E}
{F₂ : CategoryTheory.Functor D E}
(τ : F₁ ⟶ F₂)
(τ' : F₁ ⟶ F₂)
(h : ∀ (X : C), τ.app (L.toPrefunctor.obj X) = τ'.app (L.toPrefunctor.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' : CategoryTheory.Functor.comp L 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']
:
CategoryTheory.Functor.comp L 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 : CategoryTheory.MorphismProperty.IsInvertedBy W F)
(L : CategoryTheory.Functor C D)
[CategoryTheory.Functor.IsLocalization L 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.toPrefunctor.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 : CategoryTheory.MorphismProperty.IsInvertedBy W F)
(L : CategoryTheory.Functor C D)
[CategoryTheory.Functor.IsLocalization L 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 : CategoryTheory.MorphismProperty.IsInvertedBy W F)
(L : CategoryTheory.Functor C D)
[CategoryTheory.Functor.IsLocalization L W]
:
CategoryTheory.Functor.comp L (CategoryTheory.Localization.lift F hF L) ≅ F
The canonical isomorphism L ⋙ lift F hF L ≅ F for any functor F : C ⥤ E
which inverts W, when L : C ⥤ D is a localization functor for W.
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 : CategoryTheory.MorphismProperty.IsInvertedBy W F)
:
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Localization.liftNatTrans
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
(F₁ : CategoryTheory.Functor C E)
(F₂ : CategoryTheory.Functor C E)
(F₁' : CategoryTheory.Functor D E)
(F₂' : CategoryTheory.Functor D E)
[CategoryTheory.Localization.Lifting L W F₁ F₁']
[CategoryTheory.Localization.Lifting L W F₂ F₂']
(τ : F₁ ⟶ F₂)
:
F₁' ⟶ F₂'
Given a localization functor L : C ⥤ D for W : MorphismProperty C,
if (F₁' F₂' : D ⥤ E) are functors which lifts functors (F₁ F₂ : C ⥤ E),
a natural transformation τ : F₁ ⟶ F₂ uniquely lifts to a natural transformation F₁' ⟶ F₂'.
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]
[CategoryTheory.Functor.IsLocalization L W]
(F₁ : CategoryTheory.Functor C E)
(F₂ : CategoryTheory.Functor C E)
(F₁' : CategoryTheory.Functor D E)
(F₂' : CategoryTheory.Functor D E)
[CategoryTheory.Localization.Lifting L W F₁ F₁']
[CategoryTheory.Localization.Lifting L W F₂ F₂']
(τ : F₁ ⟶ F₂)
(X : C)
:
(CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ).app (L.toPrefunctor.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.Lifting.iso L W F₁ F₁').hom.app X)
(CategoryTheory.CategoryStruct.comp (τ.app X) ((CategoryTheory.Localization.Lifting.iso L W F₂ F₂').inv.app X))
@[simp]
theorem
CategoryTheory.Localization.comp_liftNatTrans_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
(F₁ : CategoryTheory.Functor C E)
(F₂ : CategoryTheory.Functor C E)
(F₃ : CategoryTheory.Functor C E)
(F₁' : CategoryTheory.Functor D E)
(F₂' : CategoryTheory.Functor D E)
(F₃' : CategoryTheory.Functor D E)
[h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁']
[h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
[h₃ : CategoryTheory.Localization.Lifting L W F₃ F₃']
(τ : F₁ ⟶ F₂)
(τ' : F₂ ⟶ F₃)
{Z : CategoryTheory.Functor D E}
(h : F₃' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₂ F₃ F₂' F₃' τ') h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Localization.liftNatTrans L W F₁ F₃ F₁' F₃' (CategoryTheory.CategoryStruct.comp τ τ')) h
@[simp]
theorem
CategoryTheory.Localization.comp_liftNatTrans
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
(F₁ : CategoryTheory.Functor C E)
(F₂ : CategoryTheory.Functor C E)
(F₃ : CategoryTheory.Functor C E)
(F₁' : CategoryTheory.Functor D E)
(F₂' : CategoryTheory.Functor D E)
(F₃' : CategoryTheory.Functor D E)
[h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁']
[h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
[h₃ : CategoryTheory.Localization.Lifting L W F₃ F₃']
(τ : F₁ ⟶ F₂)
(τ' : F₂ ⟶ F₃)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ)
(CategoryTheory.Localization.liftNatTrans L W F₂ F₃ F₂' F₃' τ') = CategoryTheory.Localization.liftNatTrans L W F₁ F₃ F₁' F₃' (CategoryTheory.CategoryStruct.comp τ τ')
@[simp]
theorem
CategoryTheory.Localization.liftNatTrans_id
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
(F : CategoryTheory.Functor C E)
(F' : CategoryTheory.Functor D E)
[h : CategoryTheory.Localization.Lifting L W F F']
:
@[simp]
theorem
CategoryTheory.Localization.liftNatIso_hom
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
(F₁ : CategoryTheory.Functor C E)
(F₂ : CategoryTheory.Functor C E)
(F₁' : CategoryTheory.Functor D E)
(F₂' : CategoryTheory.Functor D E)
[h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁']
[h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
(e : F₁ ≅ F₂)
:
(CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e).hom = CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' e.hom
@[simp]
theorem
CategoryTheory.Localization.liftNatIso_inv
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
(F₁ : CategoryTheory.Functor C E)
(F₂ : CategoryTheory.Functor C E)
(F₁' : CategoryTheory.Functor D E)
(F₂' : CategoryTheory.Functor D E)
[h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁']
[h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
(e : F₁ ≅ F₂)
:
(CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e).inv = CategoryTheory.Localization.liftNatTrans L W F₂ F₁ F₂' F₁' e.inv
def
CategoryTheory.Localization.liftNatIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
[CategoryTheory.Functor.IsLocalization L W]
(F₁ : CategoryTheory.Functor C E)
(F₂ : CategoryTheory.Functor C E)
(F₁' : CategoryTheory.Functor D E)
(F₂' : CategoryTheory.Functor D E)
[h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁']
[h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
(e : F₁ ≅ F₂)
:
F₁' ≅ F₂'
Given a localization functor L : C ⥤ D for W : MorphismProperty C,
if (F₁' F₂' : D ⥤ E) are functors which lifts functors (F₁ F₂ : C ⥤ E),
a natural isomorphism τ : F₁ ⟶ F₂ lifts to a natural isomorphism F₁' ⟶ F₂'.
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')
:
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)
:
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' := CategoryTheory.Functor.rightUnitor L }
@[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)
:
Equations
- CategoryTheory.Localization.Lifting.compLeft L W F = { iso' := CategoryTheory.Iso.refl (CategoryTheory.Functor.comp L 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₂)
[CategoryTheory.Functor.IsLocalization L₁ W]
:
theorem
CategoryTheory.Functor.IsLocalization.of_equivalence_target
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
{E : Type u_4}
[CategoryTheory.Category.{u_5, u_4} E]
(L' : CategoryTheory.Functor C E)
(eq : D ≌ E)
[CategoryTheory.Functor.IsLocalization L W]
(e : CategoryTheory.Functor.comp L eq.functor ≅ L')
:
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.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)
[CategoryTheory.IsEquivalence L]
:
def
CategoryTheory.Localization.uniq
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_7, u_5} D₁]
[CategoryTheory.Category.{u_8, u_6} D₂]
(L₁ : CategoryTheory.Functor C D₁)
(L₂ : CategoryTheory.Functor C D₂)
(W' : CategoryTheory.MorphismProperty C)
[CategoryTheory.Functor.IsLocalization L₁ W']
[CategoryTheory.Functor.IsLocalization L₂ W']
:
D₁ ≌ D₂
If L₁ : C ⥤ D₁ and L₂ : C ⥤ D₂ are two localization functors for the
same MorphismProperty C, this is an equivalence of categories D₁ ≌ D₂.
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)
[CategoryTheory.Functor.IsLocalization L₁ W']
[CategoryTheory.Functor.IsLocalization L₂ W']
:
(CategoryTheory.Localization.uniq L₁ L₂ W').symm = CategoryTheory.Localization.uniq L₂ L₁ W'
def
CategoryTheory.Localization.compUniqFunctor
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_7, u_5} D₁]
[CategoryTheory.Category.{u_8, u_6} D₂]
(L₁ : CategoryTheory.Functor C D₁)
(L₂ : CategoryTheory.Functor C D₂)
(W' : CategoryTheory.MorphismProperty C)
[CategoryTheory.Functor.IsLocalization L₁ W']
[CategoryTheory.Functor.IsLocalization L₂ W']
:
CategoryTheory.Functor.comp L₁ (CategoryTheory.Localization.uniq L₁ L₂ W').functor ≅ L₂
The functor of equivalence of localized categories given by Localization.uniq is
compatible with the localization functors.
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)
[CategoryTheory.Functor.IsLocalization L₁ W']
[CategoryTheory.Functor.IsLocalization L₂ W']
:
CategoryTheory.Functor.comp L₂ (CategoryTheory.Localization.uniq L₁ L₂ W').inverse ≅ L₁
The inverse functor of equivalence of localized categories given by Localization.uniq is
compatible with the localization functors.
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)
[CategoryTheory.Functor.IsLocalization L₁ W']
[CategoryTheory.Functor.IsLocalization L₂ 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)
[CategoryTheory.Functor.IsLocalization L₁ W']
[CategoryTheory.Functor.IsLocalization L₂ 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)
[CategoryTheory.Functor.IsLocalization L₁ W']
[CategoryTheory.Functor.IsLocalization L₂ W']
(F : CategoryTheory.Functor D₁ D₂)
(e : CategoryTheory.Functor.comp L₁ F ≅ L₂)
:
F ≅ (CategoryTheory.Localization.uniq L₁ L₂ W').functor
If L₁ : C ⥤ D₁ and L₂ : C ⥤ D₂ are two localization functors for the
same MorphismProperty C, any functor F : D₁ ⥤ D₂ equipped with an isomorphism
L₁ ⋙ F ≅ L₂ is isomorphic to the functor of the equivalence given by uniq.
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 = ((CategoryTheory.MorphismProperty.Q W).toPrefunctor.map f = (CategoryTheory.MorphismProperty.Q W).toPrefunctor.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)
[CategoryTheory.Functor.IsLocalization L W]
:
CategoryTheory.AreEqualizedByLocalization W f g ↔ L.toPrefunctor.map f = L.toPrefunctor.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)
[CategoryTheory.Functor.IsLocalization L W]
(h : L.toPrefunctor.map f = L.toPrefunctor.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)
[CategoryTheory.Functor.IsLocalization L W]
:
L.toPrefunctor.map f = L.toPrefunctor.map g