Documentation

Mathlib.CategoryTheory.Localization.LocalizerMorphism

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é

structure CategoryTheory.LocalizerMorphism {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] (W₁ : MorphismProperty C₁) (W₂ : 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 : Functor C₁ C₂
a functor between the two categories
map : W₁ ≤ W₂.inverseImage self.functor
the functor is compatible with the MorphismProperty

Instances For

def CategoryTheory.LocalizerMorphism.ofEq {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {F : Functor C₁ C₂} (hW : W₁ = W₂.inverseImage F) :

LocalizerMorphism W₁ W₂

Constructor for localizer morphisms given by a functor F : C₁ ⥤ C₂ under the stronger assumption that the classes of morphisms W₁ and W₂ satisfy W₁ = W₂.inverseImage F.

Equations

CategoryTheory.LocalizerMorphism.ofEq hW = { functor := F, map := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.LocalizerMorphism.ofEq_functor {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {F : Functor C₁ C₂} (hW : W₁ = W₂.inverseImage F) :

(ofEq hW).functor = F

def CategoryTheory.LocalizerMorphism.id {C₁ : Type u₁} [Category.{v₁, u₁} C₁] (W₁ : MorphismProperty C₁) :

LocalizerMorphism W₁ W₁

The identity functor as a morphism of localizers.

Equations

CategoryTheory.LocalizerMorphism.id W₁ = { functor := CategoryTheory.Functor.id C₁, map := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.LocalizerMorphism.id_functor {C₁ : Type u₁} [Category.{v₁, u₁} C₁] (W₁ : MorphismProperty C₁) :

(id W₁).functor = Functor.id C₁

instance CategoryTheory.LocalizerMorphism.instIsEquivalenceFunctorId {C₁ : Type u₁} [Category.{v₁, u₁} C₁] (W₁ : MorphismProperty C₁) :

(id W₁).functor.IsEquivalence

def CategoryTheory.LocalizerMorphism.comp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} (Φ : LocalizerMorphism W₁ W₂) (Ψ : LocalizerMorphism W₂ W₃) :

LocalizerMorphism W₁ W₃

The composition of two localizers morphisms.

Equations

Φ.comp Ψ = { functor := Φ.functor.comp Ψ.functor, map := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.LocalizerMorphism.comp_functor {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} (Φ : LocalizerMorphism W₁ W₂) (Ψ : LocalizerMorphism W₂ W₃) :

(Φ.comp Ψ).functor = Φ.functor.comp Ψ.functor

@[reducible, inline]

abbrev CategoryTheory.LocalizerMorphism.op {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) :

LocalizerMorphism W₁.op W₂.op

The opposite localizer morphism LocalizerMorphism W₁.op W₂.op deduced from Φ : LocalizerMorphism W₁ W₂.

Equations

Φ.op = { functor := Φ.functor.op, map := ⋯ }

Instances For

@[implicit_reducible]

def CategoryTheory.LocalizerMorphism.prod {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {C₁' : Type u_1} {C₂' : Type u_2} [Category.{v_1, u_1} C₁'] [Category.{v_2, u_2} C₂'] {W₁' : MorphismProperty C₁'} {W₂' : MorphismProperty C₂'} (Φ₁ : LocalizerMorphism W₁ W₂) (Φ₂ : LocalizerMorphism W₁' W₂') :

LocalizerMorphism (W₁.prod W₁') (W₂.prod W₂')

The external product of two morphisms of localizers.

Equations

Φ₁.prod Φ₂ = { functor := Φ₁.functor.prod Φ₂.functor, map := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.LocalizerMorphism.prod_functor {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {C₁' : Type u_1} {C₂' : Type u_2} [Category.{v_1, u_1} C₁'] [Category.{v_2, u_2} C₂'] {W₁' : MorphismProperty C₁'} {W₂' : MorphismProperty C₂'} (Φ₁ : LocalizerMorphism W₁ W₂) (Φ₂ : LocalizerMorphism W₁' W₂') :

(Φ₁.prod Φ₂).functor = Φ₁.functor.prod Φ₂.functor

theorem CategoryTheory.LocalizerMorphism.inverts {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] :

W₁.IsInvertedBy (Φ.functor.comp L₂)

noncomputable def CategoryTheory.LocalizerMorphism.localizedFunctor {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] :

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

Φ.localizedFunctor L₁ L₂ = CategoryTheory.Localization.lift (Φ.functor.comp L₂) ⋯ L₁

Instances For

@[instance_reducible]

noncomputable instance CategoryTheory.LocalizerMorphism.liftingLocalizedFunctor {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] :

Localization.Lifting L₁ W₁ (Φ.functor.comp L₂) (Φ.localizedFunctor L₁ L₂)

Equations

Φ.liftingLocalizedFunctor L₁ L₂ = { iso := CategoryTheory.LocalizerMorphism.liftingLocalizedFunctor._aux_1 Φ L₁ L₂ }

@[instance_reducible]

noncomputable instance CategoryTheory.LocalizerMorphism.catCommSq {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] :

CatCommSq Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)

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 }

theorem CategoryTheory.LocalizerMorphism.isEquivalence_imp {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [Category.{v₄', u₄'} D₁'] [Category.{v₅', u₅'} D₂'] (L₁' : Functor C₁ D₁') (L₂' : Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : Functor D₁' D₂') [CatCommSq Φ.functor L₁' L₂' G'] [G.IsEquivalence] :

G'.IsEquivalence

If a localizer morphism induces an equivalence on some choice of localized categories, it will be so for any choice of localized categories.

theorem CategoryTheory.LocalizerMorphism.isEquivalence_iff {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [Category.{v₄', u₄'} D₁'] [Category.{v₅', u₅'} D₂'] (L₁' : Functor C₁ D₁') (L₂' : Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : Functor D₁' D₂') [CatCommSq Φ.functor L₁' L₂' G'] :

G.IsEquivalence ↔ G'.IsEquivalence

theorem CategoryTheory.LocalizerMorphism.nonempty_fullyFaithful_iff {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [Category.{v₄', u₄'} D₁'] [Category.{v₅', u₅'} D₂'] (L₁' : Functor C₁ D₁') (L₂' : Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : Functor D₁' D₂') [CatCommSq Φ.functor L₁' L₂' G'] :

Nonempty G.FullyFaithful ↔ Nonempty G'.FullyFaithful

class CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) :

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

theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk' {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [CatCommSq Φ.functor L₁ L₂ G] [G.IsEquivalence] :

Φ.IsLocalizedEquivalence

theorem CategoryTheory.LocalizerMorphism.isEquivalence {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [h : Φ.IsLocalizedEquivalence] [CatCommSq Φ.functor L₁ L₂ G] :

G.IsEquivalence

If a LocalizerMorphism is a localized equivalence, then any compatible functor between the localized categories is an equivalence.

instance CategoryTheory.LocalizerMorphism.instIsLocalizedEquivalenceOppositeOpOp {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.IsLocalizedEquivalence] :

Φ.op.IsLocalizedEquivalence

instance CategoryTheory.LocalizerMorphism.localizedFunctor_isEquivalence {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedEquivalence] :

(Φ.localizedFunctor L₁ L₂).IsEquivalence

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₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] [(Φ.functor.comp L₂).IsLocalization W₁] :

Φ.IsLocalizedEquivalence

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₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] (h : W₂ ≤ W₁.map Φ.functor) :

Φ.IsLocalizedEquivalence

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.

instance CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedEquivalence] :

(Φ.functor.comp L₂).IsLocalization W₁

theorem CategoryTheory.LocalizerMorphism.isLocalizedEquivalence_of_unit_of_unit {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (Ψ : LocalizerMorphism W₂ W₁) (ε₁ : Functor.id C₁ ⟶ Φ.functor.comp Ψ.functor) (ε₂ : Functor.id C₂ ⟶ Ψ.functor.comp Φ.functor) (hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)) (hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)) :

Φ.IsLocalizedEquivalence

instance CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.id {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {W₁ : MorphismProperty C₁} :

(LocalizerMorphism.id W₁).IsLocalizedEquivalence

instance CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.comp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} (Φ : LocalizerMorphism W₁ W₂) [Φ.IsLocalizedEquivalence] (Ψ : LocalizerMorphism W₂ W₃) [Ψ.IsLocalizedEquivalence] :

(Φ.comp Ψ).IsLocalizedEquivalence

class CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) :

Condition that a LocalizerMorphism induces a fully faithful functor on the localized categories.

nonempty_fullyFaithful : Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful
the induced functor on the constructed localized categories is fully faithful

Instances

theorem CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk' {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [CatCommSq Φ.functor L₁ L₂ G] (hG : G.FullyFaithful) :

Φ.IsLocalizedFullyFaithful

instance CategoryTheory.LocalizerMorphism.instIsLocalizedFullyFaithfulOfIsLocalizedEquivalence {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.IsLocalizedEquivalence] :

Φ.IsLocalizedFullyFaithful

noncomputable def CategoryTheory.LocalizerMorphism.fullyFaithful {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [h : Φ.IsLocalizedFullyFaithful] [CatCommSq Φ.functor L₁ L₂ G] :

G.FullyFaithful

If a LocalizerMorphism becomes a fully faithful after localization, then any compatible functor between the localized categories is fully faithful.

Equations

Φ.fullyFaithful L₁ L₂ G = ⋯.some

Instances For

theorem CategoryTheory.LocalizerMorphism.faithful {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [Φ.IsLocalizedFullyFaithful] [CatCommSq Φ.functor L₁ L₂ G] :

theorem CategoryTheory.LocalizerMorphism.full {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [Φ.IsLocalizedFullyFaithful] [CatCommSq Φ.functor L₁ L₂ G] :

noncomputable def CategoryTheory.LocalizerMorphism.fullyFaithfulLocalizedFunctor {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedFullyFaithful] :

(Φ.localizedFunctor L₁ L₂).FullyFaithful

If a LocalizerMorphism becomes fully faithful after localization, then the induced functor on the localized categories is fully faithful.

Equations

Φ.fullyFaithfulLocalizedFunctor L₁ L₂ = Φ.fullyFaithful L₁ L₂ (Φ.localizedFunctor L₁ L₂)

Instances For

instance CategoryTheory.LocalizerMorphism.instFullLocalizedFunctorOfIsLocalizedFullyFaithful {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedFullyFaithful] :

(Φ.localizedFunctor L₁ L₂).Full

instance CategoryTheory.LocalizerMorphism.instFaithfulLocalizedFunctorOfIsLocalizedFullyFaithful {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedFullyFaithful] :

(Φ.localizedFunctor L₁ L₂).Faithful

instance CategoryTheory.LocalizerMorphism.instIsLocalizedFullyFaithfulOppositeOpOp {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.IsLocalizedFullyFaithful] :

Φ.op.IsLocalizedFullyFaithful

theorem CategoryTheory.LocalizerMorphism.isLocalization_of_isLocalizedFullyFaithful {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.IsLocalizedFullyFaithful] {L₂ : Functor C₂ D₂} [L₂.IsLocalization W₂] {L₁ : Functor C₁ D₁} {F : Functor D₁ D₂} (iso : Φ.functor.comp L₂ ≅ L₁.comp F) [F.Full] [F.Faithful] [L₁.EssSurj] :

L₁.IsLocalization W₁

Assume that a localizer morphism Φ : LocalizerMorphism W₁ W₂ induces a fully faithful functor on the localized categories. If L₂ : C₂ ⥤ D₂ is a localization functor for W₂ and we have a factorization iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F as an essentially surjective functor L₁ : C₁ ⥤ D₁ followed by a fully faithful functor F : D₁ ⥤ D₂, then L₁ is a localization functor for W₁.

instance CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.comp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} (Φ : LocalizerMorphism W₁ W₂) (Ψ : LocalizerMorphism W₂ W₃) [Φ.IsLocalizedFullyFaithful] [Ψ.IsLocalizedFullyFaithful] :

(Φ.comp Ψ).IsLocalizedFullyFaithful

@[reducible, inline]

abbrev CategoryTheory.LocalizerMorphism.arrow {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) :

LocalizerMorphism W₁.arrow W₂.arrow

The localizer morphism from W₁.arrow to W₂.arrow that is induced by Φ : LocalizerMorphism W₁ W₂.

Equations

Φ.arrow = { functor := Φ.functor.mapArrow, map := ⋯ }

Instances For

class CategoryTheory.LocalizerMorphism.IsInduced {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) :

If Φ : LocalizerMorphism W₁ W₂, the typeclass Φ.IsInduced says that W₂.inverseImage Φ.functor = W₁.

inverseImage_eq : W₂.inverseImage Φ.functor = W₁

Instances

instance CategoryTheory.LocalizerMorphism.instIsInducedOppositeOpOp {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.IsInduced] :

Φ.op.IsInduced

instance CategoryTheory.LocalizerMorphism.instIsInducedId {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {W₁ : MorphismProperty C₁} :

(id W₁).IsInduced

instance CategoryTheory.LocalizerMorphism.instIsInducedComp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} (Φ : LocalizerMorphism W₁ W₂) (Ψ : LocalizerMorphism W₂ W₃) [Φ.IsInduced] [Ψ.IsInduced] :

(Φ.comp Ψ).IsInduced

instance CategoryTheory.LocalizerMorphism.instIsInducedArrowArrowArrow {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.IsInduced] :

Φ.arrow.IsInduced

noncomputable def CategoryTheory.LocalizerMorphism.inv {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] :

LocalizerMorphism W₂ W₁

The inverse of a localizer morphism Φ : LocalizerMorphism W₁ W₂, when Φ.functor is an equivalence, W₁ is induced by W₂ and W₂ respects isomorphisms.

Equations

Φ.inv = { functor := Φ.functor.inv, map := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.LocalizerMorphism.inv_functor {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] :

Φ.inv.functor = Φ.functor.inv

instance CategoryTheory.LocalizerMorphism.instIsEquivalenceFunctorInv {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] :

Φ.inv.functor.IsEquivalence

instance CategoryTheory.LocalizerMorphism.instIsInducedInv {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] :

Φ.inv.IsInduced

theorem CategoryTheory.LocalizerMorphism.isLocalizedEquivalence_of_isInduced {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] :

Φ.IsLocalizedEquivalence