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 #
- [Bruno Kahn and Georges Maltsiniotis, Structures de dérivabilité][KahnMaltsiniotis2008]
structure
CategoryTheory.LocalizerMorphism
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
(W₁ : CategoryTheory.MorphismProperty C₁)
(W₂ : CategoryTheory.MorphismProperty C₂)
:
Type (max (max (max u₁ u₂) v₁) v₂)
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₁ ⊆ CategoryTheory.MorphismProperty.inverseImage W₂ self.functor
the functor is compatible with the
MorphismProperty
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.id_functor
{C₁ : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C₁]
(W₁ : CategoryTheory.MorphismProperty C₁)
:
(CategoryTheory.LocalizerMorphism.id W₁).functor = CategoryTheory.Functor.id C₁
def
CategoryTheory.LocalizerMorphism.id
{C₁ : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C₁]
(W₁ : CategoryTheory.MorphismProperty C₁)
:
The identity functor as a morphism of localizers.
Equations
- CategoryTheory.LocalizerMorphism.id W₁ = { functor := CategoryTheory.Functor.id C₁, map := (_ : ∀ (x x_1 : C₁) (x_2 : x ⟶ x_1), W₁ x_2 → W₁ x_2) }
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.comp_functor
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
{W₃ : CategoryTheory.MorphismProperty C₃}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(Ψ : CategoryTheory.LocalizerMorphism W₂ W₃)
:
(CategoryTheory.LocalizerMorphism.comp Φ Ψ).functor = CategoryTheory.Functor.comp Φ.functor Ψ.functor
def
CategoryTheory.LocalizerMorphism.comp
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
{W₃ : CategoryTheory.MorphismProperty C₃}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(Ψ : CategoryTheory.LocalizerMorphism W₂ W₃)
:
The composition of two localizers morphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.LocalizerMorphism.inverts
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
:
CategoryTheory.MorphismProperty.IsInvertedBy W₁ (CategoryTheory.Functor.comp Φ.functor L₂)
noncomputable def
CategoryTheory.LocalizerMorphism.localizedFunctor
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₁ : Type u₄}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₄, u₄} D₁]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
:
CategoryTheory.Functor D₁ D₂
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
- One or more equations did not get rendered due to their size.
Instances For
noncomputable instance
CategoryTheory.LocalizerMorphism.instLiftingCompFunctorLocalizedFunctor
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₁ : Type u₄}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₄, u₄} D₁]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
:
CategoryTheory.Localization.Lifting L₁ W₁ (CategoryTheory.Functor.comp Φ.functor L₂)
(CategoryTheory.LocalizerMorphism.localizedFunctor Φ L₁ L₂)
Equations
- CategoryTheory.LocalizerMorphism.instLiftingCompFunctorLocalizedFunctor Φ L₁ L₂ = id inferInstance
noncomputable instance
CategoryTheory.LocalizerMorphism.catCommSq
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₁ : Type u₄}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₄, u₄} D₁]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
:
CategoryTheory.CatCommSq Φ.functor L₁ L₂ (CategoryTheory.LocalizerMorphism.localizedFunctor Φ L₁ L₂)
The 2-commutative square expressing that Φ.localizedFunctor L₁ L₂ lifts the
functor Φ.functor
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.LocalizerMorphism.isEquivalence_imp
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₁ : Type u₄}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₄, u₄} D₁]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
(G : CategoryTheory.Functor D₁ D₂)
[CategoryTheory.CatCommSq Φ.functor L₁ L₂ G]
{D₁' : Type u₄'}
{D₂' : Type u₅'}
[CategoryTheory.Category.{v₄', u₄'} D₁']
[CategoryTheory.Category.{v₅', u₅'} D₂']
(L₁' : CategoryTheory.Functor C₁ D₁')
(L₂' : CategoryTheory.Functor C₂ D₂')
[CategoryTheory.Functor.IsLocalization L₁' W₁]
[CategoryTheory.Functor.IsLocalization L₂' W₂]
(G' : CategoryTheory.Functor D₁' D₂')
[CategoryTheory.CatCommSq Φ.functor L₁' L₂' G']
[CategoryTheory.IsEquivalence G]
:
If a localizer morphism induces an equivalence on some choice of localized categories, it will be so for any choice of localized categoriees.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.LocalizerMorphism.nonempty_isEquivalence_iff
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₁ : Type u₄}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₄, u₄} D₁]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
(G : CategoryTheory.Functor D₁ D₂)
[CategoryTheory.CatCommSq Φ.functor L₁ L₂ G]
{D₁' : Type u₄'}
{D₂' : Type u₅'}
[CategoryTheory.Category.{v₄', u₄'} D₁']
[CategoryTheory.Category.{v₅', u₅'} D₂']
(L₁' : CategoryTheory.Functor C₁ D₁')
(L₂' : CategoryTheory.Functor C₂ D₂')
[CategoryTheory.Functor.IsLocalization L₁' W₁]
[CategoryTheory.Functor.IsLocalization L₂' W₂]
(G' : CategoryTheory.Functor D₁' D₂')
[CategoryTheory.CatCommSq Φ.functor L₁' L₂' G']
:
class
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
:
Condition that a LocalizerMorphism induces an equivalence on the localized categories
- nonempty_isEquivalence : Nonempty (CategoryTheory.IsEquivalence (CategoryTheory.LocalizerMorphism.localizedFunctor Φ (CategoryTheory.MorphismProperty.Q W₁) (CategoryTheory.MorphismProperty.Q W₂)))
the induced functor on the constructed localized categories is an equivalence
Instances
theorem
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk'
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₁ : Type u₄}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₄, u₄} D₁]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
(G : CategoryTheory.Functor D₁ D₂)
[CategoryTheory.CatCommSq Φ.functor L₁ L₂ G]
[CategoryTheory.IsEquivalence G]
:
noncomputable def
CategoryTheory.LocalizerMorphism.isEquivalence
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₁ : Type u₄}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₄, u₄} D₁]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
(G : CategoryTheory.Functor D₁ D₂)
[h : CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence Φ]
[CategoryTheory.CatCommSq Φ.functor L₁ L₂ G]
:
If a LocalizerMorphism is a localized equivalence, then any compatible functor
between the localized categories is an equivalence.
Equations
- CategoryTheory.LocalizerMorphism.isEquivalence Φ L₁ L₂ G = Nonempty.some (_ : Nonempty (CategoryTheory.IsEquivalence G))
Instances For
noncomputable instance
CategoryTheory.LocalizerMorphism.localizedFunctor_isEquivalence
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₁ : Type u₄}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₄, u₄} D₁]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
[CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence Φ]
:
If a LocalizerMorphism is a localized equivalence, then the induced functor on
the localized categories is an equivalence
theorem
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₂ : Type u₅}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₂ : CategoryTheory.Functor C₂ D₂)
[CategoryTheory.Functor.IsLocalization L₂ W₂]
[CategoryTheory.Functor.IsLocalization (CategoryTheory.Functor.comp Φ.functor L₂) W₁]
:
When Φ : LocalizerMorphism W₁ W₂, if the composition Φ.functor ⋙ L₂ is a
localization functor for W₁, then Φ is a localized equivalence.
theorem
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
[CategoryTheory.IsEquivalence Φ.functor]
(h : W₂ ⊆ CategoryTheory.MorphismProperty.map W₁ Φ.functor)
:
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.