Documentation

Mathlib.CategoryTheory.Localization.Bousfield

Bousfield localization #

Given a predicate P : ObjectProperty C on the objects of a category C, we define W.isLocal : MorphismProperty C as the class of morphisms f : X ⟶ Y such that for any Z : C such that P Z, the precomposition with f induces a bijection (Y ⟶ Z) ≃ (X ⟶ Z).

(This construction is part of the left Bousfield localization in the context of model categories.)

When G ⊣ F is an adjunction with F : C ⥤ D fully faithful, then G : D ⥤ C is a localization functor for the class isLocal (· ∈ Set.range F.obj), which then identifies to the inverse image by G of the class of isomorphisms in C.

The dual results are also obtained.

References #

https://ncatlab.org/nlab/show/left+Bousfield+localization+of+model+categories

Left Bousfield localization #

def CategoryTheory.ObjectProperty.isLocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

MorphismProperty C

Given P : ObjectProperty C, this is the class of morphisms f : X ⟶ Y such that for all Z : C such that P Z, the precomposition with f induces a bijection (Y ⟶ Z) ≃ (X ⟶ Z). (One of the applications of this notion is the left Bousfield localization of model categories.)

Equations

P.isLocal f = ∀ (Z : C), P Z → Function.Bijective fun (g : x✝ ⟶ Z) => CategoryTheory.CategoryStruct.comp f g

Instances For

noncomputable def CategoryTheory.ObjectProperty.isLocal.homEquiv {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} {X Y : C} {f : X ⟶ Y} (hf : P.isLocal f) (Z : C) (hZ : P Z) :

(Y ⟶ Z) ≃ (X ⟶ Z)

The bijection (Y ⟶ Z) ≃ (X ⟶ Z) induced by f : X ⟶ Y when P.isLocal f and P Z.

Equations

hf.homEquiv Z hZ = Equiv.ofBijective (fun (g : Y ⟶ Z) => CategoryTheory.CategoryStruct.comp f g) ⋯

Instances For

@[simp]

theorem CategoryTheory.ObjectProperty.isLocal.homEquiv_apply {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} {X Y : C} {f : X ⟶ Y} (hf : P.isLocal f) (Z : C) (hZ : P Z) (g : Y ⟶ Z) :

(hf.homEquiv Z hZ) g = CategoryStruct.comp f g

theorem CategoryTheory.ObjectProperty.isoClosure_isLocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P.isoClosure.isLocal = P.isLocal

instance CategoryTheory.ObjectProperty.instIsMultiplicativeIsLocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P.isLocal.IsMultiplicative

instance CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsLocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P.isLocal.HasTwoOutOfThreeProperty

theorem CategoryTheory.ObjectProperty.isLocal_of_isIso {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) [IsIso f] :

theorem CategoryTheory.ObjectProperty.isLocal_iff_isIso {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) (hX : P X) (hY : P Y) :

P.isLocal f ↔ IsIso f

instance CategoryTheory.ObjectProperty.instRespectsIsoIsLocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P.isLocal.RespectsIso

theorem CategoryTheory.ObjectProperty.le_isLocal_iff {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) (W : MorphismProperty C) :

W ≤ P.isLocal ↔ P ≤ W.isLocal

theorem CategoryTheory.ObjectProperty.galoisConnection_isLocal {C : Type u_1} [Category.{v_1, u_1} C] :

GaloisConnection (⇑OrderDual.toDual ∘ isLocal) (MorphismProperty.isLocal ∘ ⇑OrderDual.ofDual)

Right Bousfield localization #

def CategoryTheory.ObjectProperty.isColocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

MorphismProperty C

Given P : ObjectProperty C, this is the class of morphisms g : Y ⟶ Z such that for all X : C such that P X, the postcomposition with g induces a bijection (X ⟶ Y) ≃ (X ⟶ Z). (One of the applications of this notion is the right Bousfield localization of model categories.)

Equations

P.isColocal g = ∀ (X : C), P X → Function.Bijective fun (f : X ⟶ x✝¹) => CategoryTheory.CategoryStruct.comp f g

Instances For

noncomputable def CategoryTheory.ObjectProperty.isColocal.homEquiv {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} {Y Z : C} {g : Y ⟶ Z} (hg : P.isColocal g) (X : C) (hX : P X) :

(X ⟶ Y) ≃ (X ⟶ Z)

The bijection (X ⟶ Y) ≃ (X ⟶ Z) induced by g : Y ⟶ Z when P.isColocal g and P X.

Equations

hg.homEquiv X hX = Equiv.ofBijective (fun (f : X ⟶ Y) => CategoryTheory.CategoryStruct.comp f g) ⋯

Instances For

@[simp]

theorem CategoryTheory.ObjectProperty.isColocal.homEquiv_apply {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} {Y Z : C} {g : Y ⟶ Z} (hg : P.isColocal g) (X : C) (hX : P X) (f : X ⟶ Y) :

(hg.homEquiv X hX) f = CategoryStruct.comp f g

theorem CategoryTheory.ObjectProperty.isoClosure_isColocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P.isoClosure.isColocal = P.isColocal

instance CategoryTheory.ObjectProperty.instIsMultiplicativeIsColocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P.isColocal.IsMultiplicative

instance CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsColocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P.isColocal.HasTwoOutOfThreeProperty

theorem CategoryTheory.ObjectProperty.isColocal_of_isIso {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) [IsIso f] :

theorem CategoryTheory.ObjectProperty.isColocal_iff_isIso {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) (hX : P X) (hY : P Y) :

P.isColocal f ↔ IsIso f

instance CategoryTheory.ObjectProperty.instRespectsIsoIsColocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P.isColocal.RespectsIso

theorem CategoryTheory.ObjectProperty.le_isColocal_iff {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) (W : MorphismProperty C) :

W ≤ P.isColocal ↔ P ≤ W.isColocal

theorem CategoryTheory.ObjectProperty.galoisConnection_isColocal {C : Type u_1} [Category.{v_1, u_1} C] :

GaloisConnection (⇑OrderDual.toDual ∘ isColocal) (MorphismProperty.isColocal ∘ ⇑OrderDual.ofDual)

Bousfield localization and adjunctions #

theorem CategoryTheory.ObjectProperty.isLocal_adj_unit_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] (X : D) :

isLocal (fun (x : D) => x ∈ Set.range F.obj) (adj.unit.app X)

theorem CategoryTheory.ObjectProperty.isLocal_iff_isIso_map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] {X Y : D} (f : X ⟶ Y) :

isLocal (fun (x : D) => x ∈ Set.range F.obj) f ↔ IsIso (G.map f)

theorem CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] :

(isLocal fun (x : D) => x ∈ Set.range F.obj) = (MorphismProperty.isomorphisms C).inverseImage G

theorem CategoryTheory.ObjectProperty.isLocalization_isLocal {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] :

G.IsLocalization (isLocal fun (x : D) => x ∈ Set.range F.obj)

theorem CategoryTheory.ObjectProperty.isColocal_adj_counit_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [G.Full] [G.Faithful] (X : C) :

isColocal (fun (x : C) => x ∈ Set.range G.obj) (adj.counit.app X)

theorem CategoryTheory.ObjectProperty.isColocal_iff_isIso_map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [G.Full] [G.Faithful] {X Y : C} (f : X ⟶ Y) :

isColocal (fun (x : C) => x ∈ Set.range G.obj) f ↔ IsIso (F.map f)

theorem CategoryTheory.ObjectProperty.isColocal_eq_inverseImage_isomorphisms {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [G.Full] [G.Faithful] :

(isColocal fun (x : C) => x ∈ Set.range G.obj) = (MorphismProperty.isomorphisms D).inverseImage F

theorem CategoryTheory.ObjectProperty.isLocalization_isColocal {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [G.Full] [G.Faithful] :

F.IsLocalization (isColocal fun (x : C) => x ∈ Set.range G.obj)

theorem CategoryTheory.ObjectProperty.le_isLocal_isLocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P ≤ P.isLocal.isLocal

theorem CategoryTheory.MorphismProperty.le_isLocal_isLocal {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) :

W ≤ W.isLocal.isLocal

theorem CategoryTheory.ObjectProperty.le_isColocal_isColocal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P ≤ P.isColocal.isColocal

theorem CategoryTheory.MorphismProperty.le_isColocal_isColocal {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) :

W ≤ W.isColocal.isColocal

@[deprecated CategoryTheory.ObjectProperty.le_isLocal_isLocal (since := "2025-11-20")]

theorem CategoryTheory.ObjectProperty.le_isLocal_W {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P ≤ P.isLocal.isLocal

Alias of CategoryTheory.ObjectProperty.le_isLocal_isLocal.

@[deprecated CategoryTheory.MorphismProperty.le_isLocal_isLocal (since := "2025-11-20")]

theorem CategoryTheory.MorphismProperty.le_leftBousfieldW_isLocal {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) :

W ≤ W.isLocal.isLocal

Alias of CategoryTheory.MorphismProperty.le_isLocal_isLocal.

@[deprecated CategoryTheory.ObjectProperty.isLocal (since := "2025-11-20")]

def CategoryTheory.Localization.LeftBousfield.W {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

MorphismProperty C

Alias of CategoryTheory.ObjectProperty.isLocal.

Given P : ObjectProperty C, this is the class of morphisms f : X ⟶ Y such that for all Z : C such that P Z, the precomposition with f induces a bijection (Y ⟶ Z) ≃ (X ⟶ Z). (One of the applications of this notion is the left Bousfield localization of model categories.)

Equations

@CategoryTheory.Localization.LeftBousfield.W = @CategoryTheory.ObjectProperty.isLocal

Instances For

@[deprecated CategoryTheory.ObjectProperty.isLocal.homEquiv (since := "2025-11-20")]

def CategoryTheory.Localization.LeftBousfield.W.homEquiv {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} {X Y : C} {f : X ⟶ Y} (hf : P.isLocal f) (Z : C) (hZ : P Z) :

(Y ⟶ Z) ≃ (X ⟶ Z)

Alias of CategoryTheory.ObjectProperty.isLocal.homEquiv.

The bijection (Y ⟶ Z) ≃ (X ⟶ Z) induced by f : X ⟶ Y when P.isLocal f and P Z.

Equations

@CategoryTheory.Localization.LeftBousfield.W.homEquiv = @CategoryTheory.ObjectProperty.isLocal.homEquiv

Instances For

@[deprecated CategoryTheory.ObjectProperty.isoClosure_isLocal (since := "2025-11-20")]

theorem CategoryTheory.Localization.LeftBousfield.W_isoClosure {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) :

P.isoClosure.isLocal = P.isLocal

Alias of CategoryTheory.ObjectProperty.isoClosure_isLocal.

@[deprecated CategoryTheory.ObjectProperty.isLocal_of_isIso (since := "2025-11-20")]

theorem CategoryTheory.Localization.LeftBousfield.W_of_isIso {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) [IsIso f] :

Alias of CategoryTheory.ObjectProperty.isLocal_of_isIso.

@[deprecated CategoryTheory.ObjectProperty.isLocal_iff_isIso (since := "2025-11-20")]

theorem CategoryTheory.Localization.LeftBousfield.W_iff_isIso {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) (hX : P X) (hY : P Y) :

P.isLocal f ↔ IsIso f

Alias of CategoryTheory.ObjectProperty.isLocal_iff_isIso.

@[deprecated CategoryTheory.ObjectProperty.le_isLocal_iff (since := "2025-11-20")]

theorem CategoryTheory.Localization.LeftBousfield.le_W_iff {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) (W : MorphismProperty C) :

W ≤ P.isLocal ↔ P ≤ W.isLocal

Alias of CategoryTheory.ObjectProperty.le_isLocal_iff.

@[deprecated CategoryTheory.ObjectProperty.galoisConnection_isLocal (since := "2025-11-20")]

theorem CategoryTheory.Localization.LeftBousfield.galoisConnection {C : Type u_1} [Category.{v_1, u_1} C] :

GaloisConnection (⇑OrderDual.toDual ∘ ObjectProperty.isLocal) (MorphismProperty.isLocal ∘ ⇑OrderDual.ofDual)

Alias of CategoryTheory.ObjectProperty.galoisConnection_isLocal.

@[deprecated CategoryTheory.ObjectProperty.isLocal_adj_unit_app (since := "2025-11-20")]

theorem CategoryTheory.Localization.LeftBousfield.W_adj_unit_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] (X : D) :

ObjectProperty.isLocal (fun (x : D) => x ∈ Set.range F.obj) (adj.unit.app X)

Alias of CategoryTheory.ObjectProperty.isLocal_adj_unit_app.

@[deprecated CategoryTheory.ObjectProperty.isLocal_iff_isIso_map (since := "2025-11-20")]

theorem CategoryTheory.Localization.LeftBousfield.W_iff_isIso_map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] {X Y : D} (f : X ⟶ Y) :

ObjectProperty.isLocal (fun (x : D) => x ∈ Set.range F.obj) f ↔ IsIso (G.map f)

Alias of CategoryTheory.ObjectProperty.isLocal_iff_isIso_map.

@[deprecated CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms (since := "2025-11-20")]

theorem CategoryTheory.Localization.LeftBousfield.W_eq_inverseImage_isomorphisms {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] :

(ObjectProperty.isLocal fun (x : D) => x ∈ Set.range F.obj) = (MorphismProperty.isomorphisms C).inverseImage G

Alias of CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms.

@[deprecated CategoryTheory.ObjectProperty.isLocalization_isLocal (since := "2025-11-20")]

theorem CategoryTheory.Localization.LeftBousfield.isLocalization {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] :

G.IsLocalization (ObjectProperty.isLocal fun (x : D) => x ∈ Set.range F.obj)

Alias of CategoryTheory.ObjectProperty.isLocalization_isLocal.