Bousfield localization

Given a predicate P : C → Prop on the objects of a category C, we define Localization.LeftBousfield.W P : 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 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 W (· ∈ Set.range F.obj), which then identifies to the inverse image by G of the class of isomorphisms in C.

References

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

def CategoryTheory.Localization.LeftBousfield.W {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (P : C → Prop) : CategoryTheory.MorphismProperty C

Given a predicate P : C → Prop, 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).

Equations

• CategoryTheory.Localization.LeftBousfield.W P f = ∀ (Z : C), P Z → Function.Bijective fun (g : x ⟶ Z) => CategoryTheory.CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.Localization.LeftBousfield.W.homEquiv_apply {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {P : C → Prop} {X : C} {Y : C} {f : X ⟶ Y} (hf : CategoryTheory.Localization.LeftBousfield.W P f) (Z : C) (hZ : P Z) (g : Y ⟶ Z) : (hf.homEquiv Z hZ) g = CategoryTheory.CategoryStruct.comp f g

noncomputable def CategoryTheory.Localization.LeftBousfield.W.homEquiv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {P : C → Prop} {X : C} {Y : C} {f : X ⟶ Y} (hf : CategoryTheory.Localization.LeftBousfield.W P f) (Z : C) (hZ : P Z) : (Y ⟶ Z) ≃ (X ⟶ Z)

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

Equations

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

theorem CategoryTheory.Localization.LeftBousfield.W_isoClosure {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (P : C → Prop) : CategoryTheory.Localization.LeftBousfield.W (CategoryTheory.isoClosure P) = CategoryTheory.Localization.LeftBousfield.W P

instance CategoryTheory.Localization.LeftBousfield.instIsMultiplicativeW {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (P : C → Prop) : (CategoryTheory.Localization.LeftBousfield.W P).IsMultiplicative

Equations

• ⋯ = ⋯

instance CategoryTheory.Localization.LeftBousfield.instHasTwoOutOfThreePropertyW {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (P : C → Prop) : (CategoryTheory.Localization.LeftBousfield.W P).HasTwoOutOfThreeProperty

Equations

• ⋯ = ⋯

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

theorem CategoryTheory.Localization.LeftBousfield.W_iff_isIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (P : C → Prop) {X : C} {Y : C} (f : X ⟶ Y) (hX : P X) (hY : P Y) : CategoryTheory.Localization.LeftBousfield.W P f ↔ CategoryTheory.IsIso f

theorem CategoryTheory.Localization.LeftBousfield.W_adj_unit_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] (X : D) : CategoryTheory.Localization.LeftBousfield.W (fun (x : D) => x ∈ Set.range F.obj) (adj.unit.app X)

theorem CategoryTheory.Localization.LeftBousfield.W_iff_isIso_map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] {X : D} {Y : D} (f : X ⟶ Y) : CategoryTheory.Localization.LeftBousfield.W (fun (x : D) => x ∈ Set.range F.obj) f ↔ CategoryTheory.IsIso (G.map f)

theorem CategoryTheory.Localization.LeftBousfield.W_eq_inverseImage_isomorphisms {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] : (CategoryTheory.Localization.LeftBousfield.W fun (x : D) => x ∈ Set.range F.obj) = (CategoryTheory.MorphismProperty.isomorphisms C).inverseImage G

theorem CategoryTheory.Localization.LeftBousfield.isLocalization {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : G ⊣ F) [F.Full] [F.Faithful] : G.IsLocalization (CategoryTheory.Localization.LeftBousfield.W fun (x : D) => x ∈ Set.range F.obj)