[Merged by Bors] - feat(CategoryTheory/Triangulated): definition of localising subcategories

Mathlib.lean

@@ -3413,6 +3413,7 @@ public import Mathlib.CategoryTheory.Triangulated.Basic
 public import Mathlib.CategoryTheory.Triangulated.Functor
 public import Mathlib.CategoryTheory.Triangulated.Generators
 public import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
+public import Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
 public import Mathlib.CategoryTheory.Triangulated.Opposite.Basic
 public import Mathlib.CategoryTheory.Triangulated.Opposite.Functor
 public import Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean

@@ -324,7 +324,6 @@ lemma exists_leftFraction₃ {X Y : C} (f f' f'' : L.obj X ⟶ L.obj Y) :
 
 end Localization
 
-
 lemma Functor.faithful_of_comp_of_hasLeftCalculusOfFractions
     {E : Type*} [Category* E] (F : D ⥤ E)
     [W.HasLeftCalculusOfFractions]

Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean

@@ -355,7 +355,6 @@ instance [HasZeroObject C] : HasZeroObject W.Localization' := W.Q'.hasZeroObject
 
 end Localization
 
-
 lemma Functor.faithful_of_comp_cancel_zero_of_hasLeftCalculusOfFractions
     {E : Type*} [Category* E] (F : D ⥤ E)
     [W.HasLeftCalculusOfFractions]

Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean

@@ -103,6 +103,12 @@ instance [P.ContainsZero] : HasZeroObject P.FullSubcategory where
     obtain ⟨X, h₁, h₂⟩ := P.exists_prop_of_containsZero
     exact ⟨_, IsZero.of_full_of_faithful_of_isZero P.ι ⟨X, h₂⟩ h₁⟩
 
+instance [P.ContainsZero] [Q.ContainsZero] [Q.IsClosedUnderIsomorphisms] :
+    (P ⊓ Q).ContainsZero where
+  exists_zero := by
+    obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero
+    exact ⟨Z, hZ, hP, Q.prop_of_isZero hZ⟩
+
 end ObjectProperty
 
 /-- Given a functor `F : C ⥤ D`, this is the property of objects of `C`

Mathlib/CategoryTheory/Opposites.lean

@@ -305,6 +305,11 @@ instance {F : C ⥤ D} [Faithful F] : Faithful F.op where
 protected def FullyFaithful.op {F : C ⥤ D} (hF : F.FullyFaithful) : F.op.FullyFaithful where
   preimage {X Y} f := .op <| hF.preimage f.unop
 
+/-- A functor is fully faithful when its opposite is fully faithful. -/
+protected def FullyFaithful.unop {F : Cᵒᵖ ⥤ Dᵒᵖ} (hF : F.FullyFaithful) :
+    F.unop.FullyFaithful where
+  preimage {X Y} f := (hF.preimage f.op).unop
+
 /-- If F is faithful then the `rightOp` of F is also faithful. -/
 instance rightOp_faithful {F : Cᵒᵖ ⥤ D} [Faithful F] : Faithful F.rightOp where
   map_injective h := Quiver.Hom.op_inj (map_injective F (Quiver.Hom.op_inj h))

Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean

@@ -0,0 +1,156 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
+public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
+
+/-!
+# Localizing subcategories
+
+Let `C` be a pretriangulated category. If `A` and `B` are triangulated
+subcategories of `C`, we define predicates (typeclasses
+`IsVerdierRightLocalizing` and `IsVerdierLeftLocalizing`)
+saying that `A` is right `B`-localizing (or left `B`-localizing).
+When `B` is closed under isomorphisms, we shall show that this implies that
+the functor from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully
+faithful (TODO @joelriou).
+
+## References
+* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*,
+  Proposition 2.3.5, Chapitre II][verdier1996]
+
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open Category Limits Pretriangulated Opposite
+
+namespace ObjectProperty
+
+variable {C D D' : Type*} [Category* C] [Category* D] [Category* D']
+
+/-- If `A` and `B` are triangulated subcategories of a (pre)triangulated
+category `C` (with `B` closed under isomorphisms), we say that `A` is
+right `B`-localizing if any morphism `X ⟶ Y` with `X` in `B` and
+`Y` in `A` factors through an object that is in `A` and `B`.
+Note that the definition does not use the (pre)triangulated structure:
+see `isVerdierRightLocalizing_iff` for a characterization which
+relies on it. -/
+class IsVerdierRightLocalizing (A B : ObjectProperty C) : Prop where
+  fac {X Y : C} (f : X ⟶ Y) (hX : B X) (hY : A Y) :
+    ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f
+
+/-- If `A` and `B` are triangulated subcategories of a (pre)triangulated
+category `C` (with `B` closed under isomorphisms), we say that `A` is
+left `B`-localizing if any morphism `X ⟶ Y` with `X` in `A` and
+`Y` in `B` factors through an object that is in `A` and `B`.
+Note that the definition does not use the (pre)triangulated structure:
+see `isVerdierLeftLocalizing_iff` for a characterization which
+relies on it. -/
+class IsVerdierLeftLocalizing (A B : ObjectProperty C) : Prop where
+  fac {X Y : C} (f : X ⟶ Y) (hX : A X) (hY : B Y) :
+    ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f
+
+instance (A B : ObjectProperty C) [A.IsVerdierLeftLocalizing B] :
+    A.op.IsVerdierRightLocalizing B.op where
+  fac f hX hY := by
+    obtain ⟨Z, a, b, h₁, h₂, fac⟩ :=
+      IsVerdierLeftLocalizing.fac f.unop hY hX
+    exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩
+
+instance (A B : ObjectProperty Cᵒᵖ) [A.IsVerdierLeftLocalizing B] :
+    A.unop.IsVerdierRightLocalizing B.unop where
+  fac f hX hY := by
+    obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierLeftLocalizing.fac f.op hY hX
+    exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩
+
+instance (A B : ObjectProperty C) [A.IsVerdierRightLocalizing B] :
+    A.op.IsVerdierLeftLocalizing B.op where
+  fac f hX hY := by
+    obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.unop hY hX
+    exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩
+
+instance (A B : ObjectProperty Cᵒᵖ) [A.IsVerdierRightLocalizing B] :
+    A.unop.IsVerdierLeftLocalizing B.unop where
+  fac f hX hY := by
+    obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.op hY hX
+    exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩
+
+variable (A B : ObjectProperty C)
+
+lemma isVerdierLeftLocalizing_op_iff :
+    A.op.IsVerdierLeftLocalizing B.op ↔ A.IsVerdierRightLocalizing B :=
+  ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsVerdierRightLocalizing B.op.unop),
+    fun _ ↦ inferInstance⟩
+
+lemma isVerdierRightLocalizing_op_iff :
+    A.op.IsVerdierRightLocalizing B.op ↔ A.IsVerdierLeftLocalizing B :=
+  ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsVerdierLeftLocalizing B.op.unop),
+    fun _ ↦ inferInstance⟩
+
+variable [HasZeroObject C] [HasShift C ℤ] [Preadditive C]
+  [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C]
+
+lemma isVerdierRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated]
+    [B.IsClosedUnderIsomorphisms] :
+    A.IsVerdierRightLocalizing B ↔
+      ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A X) (_ : B.trW s),
+        ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' := by
+  refine ⟨fun _ X Y s hX hs ↦ ?_, fun hA ↦ ⟨fun {X Y} f hX hY ↦ ?_⟩⟩
+  · rw [ObjectProperty.trW_iff'] at hs
+    obtain ⟨W, a, b, hT, hW⟩ := hs
+    obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac a hW hX
+    obtain ⟨U, hU, e, f, hT'⟩ := A.distinguished_cocone_triangle d h₁ hX
+    obtain ⟨g, hg, _⟩ := complete_distinguished_triangle_morphism _ _ hT hT'
+      c (𝟙 _) (by cat_disch)
+    refine ⟨U, e, g, hU, ?_, by cat_disch⟩
+    rw [ObjectProperty.trW_iff']
+    exact ⟨_, _, _, hT', h₁, h₂⟩
+  · obtain ⟨Z, s, b, hT⟩ := Pretriangulated.distinguished_cocone_triangle f
+    have hs : B.trW s := by
+      rw [trW_iff']
+      exact ⟨_, _, _, hT, hX⟩
+    obtain ⟨W, s', g, hW, hs', fac⟩ := hA s hY hs
+    obtain ⟨U, hU, a, c, hT'⟩ := A.distinguished_cocone_triangle₁ s' hY hW
+    obtain ⟨t, ht, ht'⟩ :=
+      complete_distinguished_triangle_morphism₁ _ _ hT hT' (𝟙 Y) g (by cat_disch)
+    exact ⟨U, t, a, hU, (B.trW_iff_of_distinguished' _ hT').1 (trW_monotone (by simp) _ hs'),
+      by cat_disch⟩
+
+variable {A B} in
+lemma IsVerdierRightLocalizing.fac'
+    [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
+    [A.IsVerdierRightLocalizing B]
+    {X Y : C} (s : X ⟶ Y) (hX : A X) (hs : B.trW s) :
+    ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' :=
+  (isVerdierRightLocalizing_iff A B).1 inferInstance s hX hs
+
+lemma isVerdierLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated]
+    [B.IsClosedUnderIsomorphisms] :
+    A.IsVerdierLeftLocalizing B ↔
+      ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A Y) (_ : B.trW s),
+        ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' := by
+  rw [← isVerdierRightLocalizing_op_iff, isVerdierRightLocalizing_iff]
+  refine ⟨fun hA X Y s hY hs ↦ ?_, fun hA X Y s hX hs ↦ ?_⟩
+  · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.op hY (by simpa [trW_op_iff])
+    exact ⟨Z'.unop, s'.unop, b.unop, hZ', trW_of_op _ hs', by cat_disch⟩
+  · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.unop hX (trW_of_op _ hs)
+    exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', by cat_disch⟩
+
+variable {A B} in
+lemma IsVerdierLeftLocalizing.fac'
+    [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
+    [A.IsVerdierLeftLocalizing B]
+    {X Y : C} (s : X ⟶ Y) (hY : A Y) (hs : B.trW s) :
+    ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' :=
+  (isVerdierLeftLocalizing_iff A B).1 inferInstance s hY hs
+
+end ObjectProperty
+
+end CategoryTheory

Mathlib/CategoryTheory/Triangulated/Subcategory.lean

@@ -90,6 +90,30 @@ lemma ext_of_isTriangulatedClosed₃'
     (h₁ : P T.obj₁) (h₂ : P T.obj₂) : P.isoClosure T.obj₃ :=
   IsTriangulatedClosed₃.ext₃' T hT h₁ h₂
 
+protected lemma distinguished_cocone_triangle [P.IsTriangulatedClosed₃]
+    {X Y : C} (a : X ⟶ Y) (hX : P X) (hY : P Y) :
+    ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk a b c ∈ distTriang _ := by
+  obtain ⟨Z, b, c, h⟩ := distinguished_cocone_triangle a
+  obtain ⟨Z', hZ', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₃' _ h hX hY
+  exact ⟨Z', hZ', b ≫ e.hom, e.inv ≫ c, isomorphic_distinguished _ h _
+    (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.symm )⟩
+
+protected lemma distinguished_cocone_triangle₁ [P.IsTriangulatedClosed₁]
+    {Y Z : C} (b : Y ⟶ Z) (hY : P Y) (hZ : P Z) :
+    ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk a b c ∈ distTriang _ := by
+  obtain ⟨X, a, c, h⟩ := distinguished_cocone_triangle₁ b
+  obtain ⟨X', hX', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₁' _ h hY hZ
+  exact ⟨X', hX', e.inv ≫ a, c ≫ e.hom⟦1⟧', isomorphic_distinguished _ h _
+    (Triangle.isoMk _ _ e.symm (Iso.refl _) (Iso.refl _))⟩
+
+protected lemma distinguished_cocone_triangle₂ [P.IsTriangulatedClosed₂]
+    {X Z : C} (c : Z ⟶ X⟦(1 : ℤ)⟧) (hX : P X) (hZ : P Z) :
+    ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z), Triangle.mk a b c ∈ distTriang _ := by
+  obtain ⟨Y, a, b, h⟩ := distinguished_cocone_triangle₂ c
+  obtain ⟨Y', hY', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ h hX hZ
+  exact ⟨Y', hY', a ≫ e.hom, e.inv ≫ b, isomorphic_distinguished _ h _
+    (Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _))⟩
+
 lemma ext_of_isTriangulatedClosed₁
     [P.IsTriangulatedClosed₁] [P.IsClosedUnderIsomorphisms]
     (T : Triangle C) (hT : T ∈ distTriang C)
@@ -154,6 +178,12 @@ instance [P.IsTriangulated] : P.IsTriangulatedClosed₃ where
 
 instance [P.IsTriangulated] : P.isoClosure.IsTriangulated where
 
+instance {Q : ObjectProperty C} [P.IsTriangulated] [Q.IsTriangulated]
+    [Q.IsClosedUnderIsomorphisms] :
+    (P ⊓ Q).IsTriangulated where
+  ext₂' T hT h₁ h₃ := by
+    obtain ⟨Y, hY, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' T hT h₁.1 h₃.1
+    exact ⟨Y, ⟨hY, Q.prop_of_iso e (Q.ext_of_isTriangulatedClosed₂ T hT h₁.2 h₃.2)⟩, ⟨e⟩⟩
 
 section
 
@@ -447,6 +477,13 @@ lemma trW_isoClosure : P.isoClosure.trW = P.trW := by
   · rintro ⟨Z, g, h, mem, hZ⟩
     exact ⟨Z, g, h, mem, ObjectProperty.le_isoClosure _ _ hZ⟩
 
+variable {P} in
+lemma trW_monotone {Q : ObjectProperty C} (h : P ≤ Q) : P.trW ≤ Q.trW := by
+  intro X Y f hf
+  rw [trW_iff] at hf ⊢
+  obtain ⟨Z, a, b, hT, hZ⟩ := hf
+  exact ⟨Z, a, b, hT, h _ hZ⟩
+
 set_option backward.isDefEq.respectTransparency false in
 instance : P.trW.RespectsIso where
   precomp {X' X Y} e (he : IsIso e) := by