Morphisms of localizers #
A morphism of localizers consists of a functor F : C₁ ⥤ C₂
between
two categories equipped with morphism properties W₁
and W₂
such
that F
sends morphisms in W₁
to morphisms in W₂
.
If Φ : LocalizerMorphism W₁ W₂
, and that L₁ : C₁ ⥤ D₁
and L₂ : C₂ ⥤ D₂
are localization functors for W₁
and W₂
, the induced functor D₁ ⥤ D₂
is denoted Φ.localizedFunctor L₁ L₂
; we introduce the condition
Φ.IsLocalizedEquivalence
which expresses that this functor is an equivalence
of categories. This condition is independent of the choice of the
localized categories.
References #
If W₁ : MorphismProperty C₁
and W₂ : MorphismProperty C₂
, a LocalizerMorphism W₁ W₂
is the datum of a functor C₁ ⥤ C₂
which sends morphisms in W₁
to morphisms in W₂
- functor : CategoryTheory.Functor C₁ C₂
a functor between the two categories
- map : W₁ ≤ W₂.inverseImage self.functor
the functor is compatible with the
MorphismProperty
Instances For
the functor is compatible with the MorphismProperty
The identity functor as a morphism of localizers.
Equations
- CategoryTheory.LocalizerMorphism.id W₁ = { functor := CategoryTheory.Functor.id C₁, map := ⋯ }
Instances For
The composition of two localizers morphisms.
Equations
- Φ.comp Ψ = { functor := Φ.functor.comp Ψ.functor, map := ⋯ }
Instances For
The opposite localizer morphism LocalizerMorphism W₁.op W₂.op
deduced
from Φ : LocalizerMorphism W₁ W₂
.
Equations
- Φ.op = { functor := Φ.functor.op, map := ⋯ }
Instances For
When Φ : LocalizerMorphism W₁ W₂
and that L₁
and L₂
are localization functors
for W₁
and W₂
, then Φ.localizedFunctor L₁ L₂
is the induced functor on the
localized categories. -
Equations
- Φ.localizedFunctor L₁ L₂ = CategoryTheory.Localization.lift (Φ.functor.comp L₂) ⋯ L₁
Instances For
The 2-commutative square expressing that Φ.localizedFunctor L₁ L₂
lifts the
functor Φ.functor
Equations
- Φ.catCommSq L₁ L₂ = { iso' := (CategoryTheory.Localization.Lifting.iso L₁ W₁ (Φ.functor.comp L₂) (Φ.localizedFunctor L₁ L₂)).symm }
If a localizer morphism induces an equivalence on some choice of localized categories, it will be so for any choice of localized categoriees.
Condition that a LocalizerMorphism
induces an equivalence on the localized categories
- isEquivalence : (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence
the induced functor on the constructed localized categories is an equivalence
Instances
the induced functor on the constructed localized categories is an equivalence
If a LocalizerMorphism
is a localized equivalence, then any compatible functor
between the localized categories is an equivalence.
If a LocalizerMorphism
is a localized equivalence, then the induced functor on
the localized categories is an equivalence
Equations
- ⋯ = ⋯
When Φ : LocalizerMorphism W₁ W₂
, if the composition Φ.functor ⋙ L₂
is a
localization functor for W₁
, then Φ
is a localized equivalence.
When the underlying functor Φ.functor
of Φ : LocalizerMorphism W₁ W₂
is
an equivalence of categories and that W₁
and W₂
essentially correspond to each
other via this equivalence, then Φ
is a localized equivalence.
Equations
- ⋯ = ⋯
The localizer morphism from W₁.arrow
to W₂.arrow
that is induced by
Φ : LocalizerMorphism W₁ W₂
.
Equations
- Φ.arrow = { functor := Φ.functor.mapArrow, map := ⋯ }