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.
- inverts : CategoryTheory.MorphismProperty.IsInvertedBy W L
the functor inverts the given
MorphismProperty
- nonempty_isEquivalence : Nonempty (CategoryTheory.IsEquivalence (CategoryTheory.Localization.Construction.lift L (_ : CategoryTheory.MorphismProperty.IsInvertedBy W L)))
the induced functor from the constructed localized category is an equivalence
The predicate expressing that, up to equivalence, a functor L : C ⥤ D
identifies the category D
with the localized category of C
with respect
to W : MorphismProperty C
.
Instances
- inverts : CategoryTheory.MorphismProperty.IsInvertedBy W L
the functor
L
invertsW
- lift : (F : CategoryTheory.Functor C E) → CategoryTheory.MorphismProperty.IsInvertedBy W F → CategoryTheory.Functor D E
any functor
C ⥤ E
which invertsW
can be lifted as a functorD ⥤ E
- fac : ∀ (F : CategoryTheory.Functor C E) (hF : CategoryTheory.MorphismProperty.IsInvertedBy W F), CategoryTheory.Functor.comp L (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.lift s F hF) = F
there is a factorisation involving the lifted functor
- uniq : ∀ (F₁ F₂ : CategoryTheory.Functor D E), CategoryTheory.Functor.comp L F₁ = CategoryTheory.Functor.comp L F₂ → F₁ = F₂
uniqueness of the lifted functor
This universal property states that a functor L : C ⥤ D
inverts morphisms
in W
and the all functors D ⥤ E
(for a fixed category E
) uniquely factors
through L
.
Instances For
The localized category W.Localization
that was constructed satisfies
the universal property of the localization.
Instances For
When W
consists of isomorphisms, the identity satisfies the universal property
of the localization.
Instances For
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
.
Instances For
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
.
Instances For
Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D
,
one may identify the functors W.Q
and L
.
Instances For
Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D
,
one may identify the functors L
and W.Q
.
Instances For
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
.
Instances For
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
.
Instances For
The functor (D ⥤ E) ⥤ (C ⥤ E)
given by the composition with a localization
functor L : C ⥤ D
with respect to W : MorphismProperty C
.
Instances For
- iso' : CategoryTheory.Functor.comp L F' ≅ F
the isomorphism relating the localization functor and the two other given functors
When L : C ⥤ D
is a localization functor for W : MorphismProperty C
and
F : C ⥤ E
is a functor, we shall say that F' : D ⥤ E
lifts F
if the obvious diagram
is commutative up to an isomorphism.
Instances
The distinguished isomorphism L ⋙ F' ≅ F
given by [Lifting L W F F']
.
Instances For
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
.
Instances For
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
.
Instances For
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₂'
.
Instances For
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₂'
.
Instances For
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₁
.
Instances For
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.
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₂
.
Instances For
The functor of equivalence of localized categories given by Localization.uniq
is
compatible with the localization functors.
Instances For
The inverse functor of equivalence of localized categories given by Localization.uniq
is
compatible with the localization functors.
Instances For
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
.