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

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 := ⋯ }

@[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 := ⋯ }

@[simp]

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

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 := ⋯ }

@[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 := ⋯ }

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₁

@[implicit_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₂ }

@[implicit_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₂) : Prop

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

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₂) : Prop

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

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

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] : G.Faithful

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] : G.Full

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₂)

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 := ⋯ }

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₂) : Prop

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

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

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 := ⋯ }

@[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