feat(CategoryTheory): right Bousfield localization (#32469)

This PR dualises definitions and basic results about `ObjectProperty.isLocal` and `MorphismProperty.isLocal`. The dual definitions are named `ObjectProperty.isColocal` and `MorphismProperty.isColocal`.

Author: joelriou

Mathlib/CategoryTheory/Localization/Adjunction.lean

@@ -6,8 +6,9 @@ Authors: Joël Riou
 module
 
 public import Mathlib.CategoryTheory.CatCommSq
-public import Mathlib.CategoryTheory.Localization.Predicate
+public import Mathlib.CategoryTheory.Localization.Opposite
 public import Mathlib.CategoryTheory.Adjunction.FullyFaithful
+public import Mathlib.CategoryTheory.Adjunction.Opposites
 
 /-!
 # Localization of adjunctions
@@ -149,6 +150,14 @@ lemma isLocalization [F.Full] [F.Faithful] :
   apply Functor.IsLocalization.of_equivalence_target W.Q W G e
     (Localization.fac G hG W.Q)
 
+include adj in
+/-- This is the dual statement to `Adjunction.isLocalization`. -/
+lemma isLocalization' [G.Full] [G.Faithful] :
+    F.IsLocalization ((MorphismProperty.isomorphisms C₁).inverseImage F) := by
+  rw [← Functor.IsLocalization.op_iff, MorphismProperty.op_inverseImage,
+    MorphismProperty.op_isomorphisms]
+  exact adj.op.isLocalization
+
 end Adjunction
 
 end CategoryTheory

Mathlib/CategoryTheory/Localization/Bousfield.lean

@@ -25,6 +25,8 @@ When `G ⊣ F` is an adjunction with `F : C ⥤ D` fully faithful, then
 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
@@ -121,6 +123,91 @@ lemma galoisConnection_isLocal :
 
 end
 
+/-! ### Right Bousfield localization -/
+
+section
+
+variable (P : ObjectProperty 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.) -/
+def isColocal : MorphismProperty C := fun _ _ g =>
+  ∀ X, P X → Function.Bijective (fun (f : X ⟶ _) => f ≫ g)
+
+variable {P} in
+/-- The bijection `(X ⟶ Y) ≃ (X ⟶ Z)` induced by `g : Y ⟶ Z` when `P.isColocal g`
+and `P X`. -/
+@[simps! apply]
+noncomputable def isColocal.homEquiv {Y Z : C} {g : Y ⟶ Z} (hg : P.isColocal g) (X : C) (hX : P X) :
+    (X ⟶ Y) ≃ (X ⟶ Z) :=
+  Equiv.ofBijective _ (hg X hX)
+
+lemma isoClosure_isColocal : P.isoClosure.isColocal = P.isColocal := by
+  ext Y Z g
+  constructor
+  · intro hg X hX
+    exact hg _ (P.le_isoClosure _ hX)
+  · rintro hg X ⟨X', hX', ⟨e⟩⟩
+    constructor
+    · intro f₁ f₂ eq
+      rw [← cancel_epi e.inv]
+      apply (hg _ hX').1
+      simp [eq]
+    · intro f
+      obtain ⟨a, h⟩ := (hg _ hX').2 (e.inv ≫ f)
+      exact ⟨e.hom ≫ a, by simp [h]⟩
+
+instance : P.isColocal.IsMultiplicative where
+  id_mem _ _ _ := by simpa [id_comp] using Function.bijective_id
+  comp_mem f g hf hg X hX := by
+    convert Function.Bijective.comp (hg X hX) (hf X hX)
+    cat_disch
+
+instance : P.isColocal.HasTwoOutOfThreeProperty where
+  of_postcomp f g hg hfg X hX := by
+    rw [← Function.Bijective.of_comp_iff' (hg X hX)]
+    convert hfg X hX
+    cat_disch
+  of_precomp f g hf hfg X hX := by
+    rw [← Function.Bijective.of_comp_iff _ (hf X hX)]
+    convert hfg X hX
+    cat_disch
+
+lemma isColocal_of_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] : P.isColocal f := fun Z _ => by
+  constructor
+  · intro g₁ g₂ _
+    simpa only [← cancel_mono f]
+  · intro g
+    exact ⟨g ≫ inv f, by simp⟩
+
+lemma isColocal_iff_isIso {X Y : C} (f : X ⟶ Y) (hX : P X) (hY : P Y) :
+    P.isColocal f ↔ IsIso f := by
+  constructor
+  · intro hf
+    obtain ⟨g, hg⟩ := (hf _ hY).2 (𝟙 Y)
+    exact ⟨g, (hf _ hX).1 (by cat_disch), hg⟩
+  · apply isColocal_of_isIso
+
+instance : P.isColocal.RespectsIso where
+  precomp f (_ : IsIso f) g hg := P.isColocal.comp_mem f g (isColocal_of_isIso _ f) hg
+  postcomp f (_ : IsIso f) g hg := P.isColocal.comp_mem g f hg (isColocal_of_isIso _ f)
+
+lemma le_isColocal_iff (P : ObjectProperty C) (W : MorphismProperty C) :
+    W ≤ P.isColocal ↔ P ≤ W.isColocal :=
+  ⟨fun h _ hZ _ _ _ hf ↦ h _ hf _ hZ,
+    fun h _ _ _ hf _ hZ ↦ h _ hZ _ hf⟩
+
+lemma galoisConnection_isColocal :
+    GaloisConnection (OrderDual.toDual ∘ isColocal (C := C))
+      (MorphismProperty.isColocal ∘ OrderDual.ofDual) :=
+  le_isColocal_iff
+
+end
+
+/-! ### Bousfield localization and adjunctions -/
+
 section
 
 variable {F : C ⥤ D} {G : D ⥤ C} (adj : G ⊣ F) [F.Full] [F.Faithful]
@@ -135,17 +222,12 @@ lemma isLocal_adj_unit_app (X : D) : isLocal (· ∈ Set.range F.obj) (adj.unit.
 
 lemma isLocal_iff_isIso_map {X Y : D} (f : X ⟶ Y) :
     isLocal (· ∈ Set.range F.obj) f ↔ IsIso (G.map f) := by
-  rw [← (isLocal (· ∈ Set.range F.obj)).postcomp_iff _ _ (isLocal_adj_unit_app adj Y)]
-  erw [adj.unit.naturality f]
-  rw [(isLocal (· ∈ Set.range F.obj)).precomp_iff _ _ (isLocal_adj_unit_app adj X),
+  have := adj.unit.naturality f
+  dsimp at this
+  rw [← (isLocal (· ∈ Set.range F.obj)).postcomp_iff _ _ (isLocal_adj_unit_app adj Y),
+    this, (isLocal (· ∈ Set.range F.obj)).precomp_iff _ _ (isLocal_adj_unit_app adj X),
     isLocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩]
-  constructor
-  · intro h
-    dsimp at h
-    exact isIso_of_fully_faithful F (G.map f)
-  · intro
-    rw [Functor.comp_map]
-    infer_instance
+  exact ⟨fun _ ↦ isIso_of_fully_faithful F (G.map f), fun _ ↦ inferInstance⟩
 
 lemma isLocal_eq_inverseImage_isomorphisms :
     isLocal (· ∈ Set.range F.obj) = (MorphismProperty.isomorphisms _).inverseImage G := by
@@ -159,6 +241,39 @@ lemma isLocalization_isLocal : G.IsLocalization (isLocal (· ∈ Set.range F.obj
 
 end
 
+section
+
+variable {F : C ⥤ D} {G : D ⥤ C} (adj : G ⊣ F) [G.Full] [G.Faithful]
+include adj
+
+lemma isColocal_adj_counit_app (X : C) : isColocal (· ∈ Set.range G.obj) (adj.counit.app X) := by
+  rintro _ ⟨Y, rfl⟩
+  convert ((Functor.FullyFaithful.ofFullyFaithful G).homEquiv.symm.trans
+    (adj.homEquiv Y X).symm).bijective using 1
+  dsimp [Adjunction.homEquiv]
+  cat_disch
+
+lemma isColocal_iff_isIso_map {X Y : C} (f : X ⟶ Y) :
+    isColocal (· ∈ Set.range G.obj) f ↔ IsIso (F.map f) := by
+  have := adj.counit.naturality f
+  dsimp at this
+  rw [← (isColocal _).precomp_iff _ _ (isColocal_adj_counit_app adj X),
+    ← this, (isColocal _).postcomp_iff _ _ (isColocal_adj_counit_app adj Y),
+    isColocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩]
+  exact ⟨fun _ ↦ isIso_of_fully_faithful G (F.map f), fun _ ↦ inferInstance⟩
+
+lemma isColocal_eq_inverseImage_isomorphisms :
+    isColocal (· ∈ Set.range G.obj) = (MorphismProperty.isomorphisms _).inverseImage F := by
+  ext P₁ P₂ f
+  rw [isColocal_iff_isIso_map adj]
+  rfl
+
+lemma isLocalization_isColocal : F.IsLocalization (isColocal (· ∈ Set.range G.obj)) := by
+  rw [isColocal_eq_inverseImage_isomorphisms adj]
+  exact adj.isLocalization'
+
+end
+
 end ObjectProperty
 
 open Localization
@@ -171,6 +286,14 @@ lemma MorphismProperty.le_isLocal_isLocal (W : MorphismProperty C) :
     W ≤ W.isLocal.isLocal := by
   rw [ObjectProperty.le_isLocal_iff]
 
+lemma ObjectProperty.le_isColocal_isColocal (P : ObjectProperty C) :
+    P ≤ P.isColocal.isColocal := by
+  rw [← le_isColocal_iff]
+
+lemma MorphismProperty.le_isColocal_isColocal (W : MorphismProperty C) :
+    W ≤ W.isColocal.isColocal := by
+  rw [ObjectProperty.le_isColocal_iff]
+
 @[deprecated (since := "2025-11-20")] alias ObjectProperty.le_isLocal_W :=
   ObjectProperty.le_isLocal_isLocal
 @[deprecated (since := "2025-11-20")] alias MorphismProperty.le_leftBousfieldW_isLocal :=

Mathlib/CategoryTheory/Localization/Opposite.lean

@@ -72,11 +72,13 @@ instance IsLocalization.unop (L : Cᵒᵖ ⥤ Dᵒᵖ) (W : MorphismProperty C
       infer_instance)
 
 @[simp]
-lemma op_iff (L : C ⥤ D) (W : MorphismProperty C) :
+lemma IsLocalization.op_iff (L : C ⥤ D) (W : MorphismProperty C) :
     L.op.IsLocalization W.op ↔ L.IsLocalization W :=
   ⟨fun _ ↦ inferInstanceAs (L.op.unop.IsLocalization W.op.unop),
     fun _ ↦ inferInstance⟩
 
+@[deprecated (since := "2025-12-10")] alias op_iff := IsLocalization.op_iff
+
 end Functor
 
 namespace Localization

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -118,6 +118,10 @@ def inverseImage (P : MorphismProperty D) (F : C ⥤ D) : MorphismProperty C :=
 lemma inverseImage_iff (P : MorphismProperty D) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) :
     P.inverseImage F f ↔ P (F.map f) := by rfl
 
+@[simp]
+lemma op_inverseImage (P : MorphismProperty D) (F : C ⥤ D) :
+    (P.inverseImage F).op = P.op.inverseImage F.op := rfl
+
 /-- The (strict) image of a `MorphismProperty C` by a functor `C ⥤ D` -/
 inductive strictMap (P : MorphismProperty C) (F : C ⥤ D) : MorphismProperty D where
   | map {X Y : C} {f : X ⟶ Y} (hf : P f) : strictMap _ _ (F.map f)
@@ -263,6 +267,11 @@ def monomorphisms : MorphismProperty C := fun _ _ f => Mono f
 /-- The `MorphismProperty C` satisfied by epimorphisms in `C`. -/
 def epimorphisms : MorphismProperty C := fun _ _ f => Epi f
 
+@[simp]
+lemma op_isomorphisms : (isomorphisms C).op = isomorphisms Cᵒᵖ := by
+  ext
+  apply isIso_unop_iff
+
 section
 
 variable {C}

Mathlib/CategoryTheory/ObjectProperty/Local.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
 public import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
+public import Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
 public import Mathlib.CategoryTheory.MorphismProperty.Basic
 
 /-!
@@ -19,6 +20,8 @@ the precomposition with `f` gives a bijection `(Y ⟶ Z) ≃ (X ⟶ Z)`.
 part of a Galois connection, with "dual" construction
 `ObjectProperty.isLocal : ObjectProperty C → MorphismProperty C`.)
 
+We also introduce the dual notion `W.isColocal : ObjectProperty C`.
+
 -/
 
 @[expose] public section
@@ -48,12 +51,31 @@ lemma isLocal_iff (Z : C) :
     W.isLocal Z ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
       W f → Function.Bijective (fun (g : _ ⟶ Z) ↦ f ≫ g) := Iff.rfl
 
+/-- Given `W : MorphismProperty C`, this is the property of `W`-colocal objects, i.e.
+the objects `X` such that for any `g : Y ⟶ Z` such that `W g` holds, the postcomposition
+with `g` gives a bijection `(X ⟶ Y) ≃ (X ⟶ Z)`.
+(See the file `Mathlib/CategoryTheory/Localization/Bousfield.lean` for the "dual" construction
+`ObjectProperty.isColocal : ObjectProperty C → MorphismProperty C`.) -/
+def isColocal : ObjectProperty C :=
+  fun X ↦ ∀ ⦃Y Z : C⦄ (g : Y ⟶ Z),
+    W g → Function.Bijective (fun (f : X ⟶ _) ↦ f ≫ g)
+
+lemma isColocal_iff (X : C) :
+    W.isColocal X ↔ ∀ ⦃Y Z : C⦄ (g : Y ⟶ Z),
+      W g → Function.Bijective (fun (f : X ⟶ Y) ↦ f ≫ g) := Iff.rfl
+
 instance : W.isLocal.IsClosedUnderIsomorphisms where
   of_iso {Z Z'} e hZ X Y f hf := by
     rw [← Function.Bijective.of_comp_iff _ (Iso.homToEquiv e).bijective]
     convert (Iso.homToEquiv e).bijective.comp (hZ f hf) using 1
     aesop
 
+instance : W.isColocal.IsClosedUnderIsomorphisms where
+  of_iso {X X'} e hX Y Z g hg := by
+    rw [← Function.Bijective.of_comp_iff _ (Iso.homFromEquiv e).bijective]
+    convert (Iso.homFromEquiv e).bijective.comp (hX g hg) using 1
+    aesop
+
 instance (J : Type u') [Category.{v'} J] :
     W.isLocal.IsClosedUnderLimitsOfShape J where
   limitsOfShape_le := fun Z ⟨p⟩ X Y f hf ↦ by
@@ -66,6 +88,18 @@ instance (J : Type u') [Category.{v'} J] :
           (by simp [reassoc_of% h, h, p.w a]) }),
       p.isLimit.hom_ext (fun j ↦ by simp [p.isLimit.fac, h])⟩
 
+instance (J : Type u') [Category.{v'} J] :
+    W.isColocal.IsClosedUnderColimitsOfShape J where
+  colimitsOfShape_le := fun X ⟨p⟩ Y Z g hg ↦ by
+    refine ⟨fun f₁ f₂ h ↦ p.isColimit.hom_ext
+      (fun j ↦ (p.prop_diag_obj j g hg).1 (by simp [h])), fun f ↦ ?_⟩
+    choose app h using fun j ↦ (p.prop_diag_obj j g hg).2 (p.ι.app j ≫ f)
+    exact ⟨p.isColimit.desc (Cocone.mk _
+      { app := app
+        naturality _ _ a := (p.prop_diag_obj _ g hg).1
+          (by simp [h]) }),
+      p.isColimit.hom_ext (fun j ↦ by simp [p.isColimit.fac_assoc, h])⟩
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/Triangulated/Orthogonal.lean

@@ -83,6 +83,23 @@ lemma isLocal_trW [P.IsTriangulated] :
       α (hY _ (P.le_shift _ _ hX₃))
     exact ⟨β, rfl⟩
 
+lemma isColocal_trW [P.IsTriangulated] :
+    P.trW.isColocal = P.leftOrthogonal := by
+  ext X
+  refine ⟨fun hX Y f hY ↦ ?_, fun hX Y₂ Y₃ h hh ↦ ?_⟩
+  · exact (hX _ (trW.mk P (contractible_distinguished₂ Y) (P.le_shift _ _ hY))).injective (by simp)
+  · rw [trW_iff'] at hh
+    obtain ⟨Y₁, f, g, hT, hY₁⟩ := hh
+    refine ⟨?_, fun α ↦ ?_⟩
+    · suffices ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0 from fun α₁ α₂ hα ↦ by
+        simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero])
+      intro α hα
+      obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ hT α hα
+      simp [hX β hY₁]
+    · obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ (rot_of_distTriang _ hT)
+        α (hX _ (P.le_shift _ _ hY₁))
+      exact ⟨β, rfl⟩
+
 variable {P} in
 lemma rightOrthogonal.map_bijective_of_isTriangulated
     [P.IsTriangulated] [IsTriangulated C] {Y : C} (hY : P.rightOrthogonal Y)
@@ -100,6 +117,23 @@ lemma rightOrthogonal.map_bijective_of_isTriangulated
     rw [hφ, ← cancel_epi (L.map φ.s), MorphismProperty.RightFraction.map_s_comp_map,
       ← hα, Functor.map_comp]
 
+variable {P} in
+lemma leftOrthogonal.map_bijective_of_isTriangulated
+    [P.IsTriangulated] [IsTriangulated C] {X : C} (hX : P.leftOrthogonal X)
+    (L : C ⥤ D) [L.IsLocalization P.trW] (Y : C) :
+    Function.Bijective (L.map : (X ⟶ Y) → _) := by
+  rw [← isColocal_trW] at hX
+  refine ⟨fun f₁ f₂ hf ↦ ?_, fun g ↦ ?_⟩
+  · rw [MorphismProperty.map_eq_iff_postcomp L P.trW] at hf
+    obtain ⟨Z, s, hs, eq⟩ := hf
+    exact (hX _ hs).1 eq
+  · obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.trW g
+    have := Localization.inverts L P.trW φ.s φ.hs
+    obtain ⟨α, hα⟩ := (hX _ φ.hs).2 φ.f
+    refine ⟨α, ?_⟩
+    rw [hφ, ← cancel_mono (L.map φ.s), MorphismProperty.LeftFraction.map_comp_map_s,
+      ← hα, Functor.map_comp]
+
 end ObjectProperty
 
 end CategoryTheory