From 6f5fcab71b4959389a78679fcca8cbfbaed6d964 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 6 May 2026 08:58:13 +0200 Subject: [PATCH 1/4] feat(CategoryTheory/Triangulated): definition of localising subcategories --- Mathlib.lean | 1 + .../CalculusOfFractions/Fractions.lean | 1 - .../CalculusOfFractions/Preadditive.lean | 1 - .../ObjectProperty/ContainsZero.lean | 6 + Mathlib/CategoryTheory/Opposites.lean | 5 + .../Triangulated/LocalizingSubcategory.lean | 148 ++++++++++++++++++ .../Triangulated/Subcategory.lean | 37 +++++ 7 files changed, 197 insertions(+), 2 deletions(-) create mode 100644 Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean diff --git a/Mathlib.lean b/Mathlib.lean index 3435a680bbbdec..3096be03ef5ef3 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3411,6 +3411,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 diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean index de916a3feec983..7909502d5b18fa 100644 --- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean +++ b/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] diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean index 85cb86a3344a8d..4373e02609c531 100644 --- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean +++ b/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] diff --git a/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean b/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean index ccee814b58d77a..c6b298d022d804 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean +++ b/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` diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean index 56ea73ea8546e8..1ebe3871954b75 100644 --- a/Mathlib/CategoryTheory/Opposites.lean +++ b/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)) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean new file mode 100644 index 00000000000000..83dd63959b42ae --- /dev/null +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -0,0 +1,148 @@ +/- +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 +`IsTriangulatedRightLocalizing` and `IsTriangulatedLeftLocalizing`) +saying that `A` is right `B`-localizing (or left `B`-localizing). + +## References +* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][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`. +See `isTriangulatedRightLocalizing_iff` for another characterization. -/ +class IsTriangulatedRightLocalizing (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`. +See `isTriangulatedLeftLocalizing_iff` for another characterization. -/ +class IsTriangulatedLeftLocalizing (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.IsTriangulatedLeftLocalizing B] : + A.op.IsTriangulatedRightLocalizing B.op where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := + IsTriangulatedLeftLocalizing.fac f.unop hY hX + exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ + +instance (A B : ObjectProperty Cᵒᵖ) [A.IsTriangulatedLeftLocalizing B] : + A.unop.IsTriangulatedRightLocalizing B.unop where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedLeftLocalizing.fac f.op hY hX + exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ + +instance (A B : ObjectProperty C) [A.IsTriangulatedRightLocalizing B] : + A.op.IsTriangulatedLeftLocalizing B.op where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac f.unop hY hX + exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ + +instance (A B : ObjectProperty Cᵒᵖ) [A.IsTriangulatedRightLocalizing B] : + A.unop.IsTriangulatedLeftLocalizing B.unop where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac f.op hY hX + exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ + +variable (A B : ObjectProperty C) + +lemma isTriangulatedLeftLocalizing_op_iff : + A.op.IsTriangulatedLeftLocalizing B.op ↔ A.IsTriangulatedRightLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedRightLocalizing B.op.unop), + fun _ ↦ inferInstance⟩ + +lemma isTriangulatedRightLocalizing_op_iff : + A.op.IsTriangulatedRightLocalizing B.op ↔ A.IsTriangulatedLeftLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedLeftLocalizing B.op.unop), + fun _ ↦ inferInstance⟩ + +variable [HasZeroObject C] [HasShift C ℤ] [Preadditive C] + [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] + +lemma isTriangulatedRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] + [B.IsClosedUnderIsomorphisms] : + A.IsTriangulatedRightLocalizing 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⟩ := IsTriangulatedRightLocalizing.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 IsTriangulatedRightLocalizing.fac' + [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + [A.IsTriangulatedRightLocalizing 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' := + (isTriangulatedRightLocalizing_iff A B).1 inferInstance s hX hs + +lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] + [B.IsClosedUnderIsomorphisms] : + A.IsTriangulatedLeftLocalizing 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 [← isTriangulatedRightLocalizing_op_iff, isTriangulatedRightLocalizing_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 IsTriangulatedLeftLocalizing.fac' + [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + [A.IsTriangulatedLeftLocalizing 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' := + (isTriangulatedLeftLocalizing_iff A B).1 inferInstance s hY hs + +end ObjectProperty + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean index 7392b7fdceb0d4..20f61551c26639 100644 --- a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean +++ b/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 From 17715c1c9955164bafbc9467df16b144aa5bc4b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 18:31:42 +0200 Subject: [PATCH 2/4] ref --- Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 83dd63959b42ae..885d89534d71ed 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -17,7 +17,8 @@ subcategories of `C`, we define predicates (typeclasses saying that `A` is right `B`-localizing (or left `B`-localizing). ## References -* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] +* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*, + Proposition 2.3.5, Chapitre II][verdier1996] -/ From abd00d9dd02333f0beff9e6b7db26275e2e335c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 18:32:34 +0200 Subject: [PATCH 3/4] added TODO --- Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 885d89534d71ed..08f8c19394325e 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -15,6 +15,8 @@ Let `C` be a pretriangulated category. If `A` and `B` are triangulated subcategories of `C`, we define predicates (typeclasses `IsTriangulatedRightLocalizing` and `IsTriangulatedLeftLocalizing`) saying that `A` is right `B`-localizing (or left `B`-localizing). +When `B` is closed under isomorphisms, we shall show 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*, From a957b73e2aa80b8b95dc15ee70db447dcd57ee8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 19:07:42 +0200 Subject: [PATCH 4/4] IsVerdierLeft/RightLocalising --- .../Triangulated/LocalizingSubcategory.lean | 79 ++++++++++--------- 1 file changed, 42 insertions(+), 37 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 08f8c19394325e..05308db5f83fac 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -13,10 +13,11 @@ public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated Let `C` be a pretriangulated category. If `A` and `B` are triangulated subcategories of `C`, we define predicates (typeclasses -`IsTriangulatedRightLocalizing` and `IsTriangulatedLeftLocalizing`) +`IsVerdierRightLocalizing` and `IsVerdierLeftLocalizing`) saying that `A` is right `B`-localizing (or left `B`-localizing). -When `B` is closed under isomorphisms, we shall show that the functor -from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully faithful (TODO @joelriou). +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*, @@ -38,8 +39,10 @@ variable {C D D' : Type*} [Category* C] [Category* D] [Category* D'] 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`. -See `isTriangulatedRightLocalizing_iff` for another characterization. -/ -class IsTriangulatedRightLocalizing (A B : ObjectProperty C) : Prop where +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 @@ -47,60 +50,62 @@ class IsTriangulatedRightLocalizing (A B : ObjectProperty C) : Prop where 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`. -See `isTriangulatedLeftLocalizing_iff` for another characterization. -/ -class IsTriangulatedLeftLocalizing (A B : ObjectProperty C) : Prop where +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.IsTriangulatedLeftLocalizing B] : - A.op.IsTriangulatedRightLocalizing B.op where +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⟩ := - IsTriangulatedLeftLocalizing.fac f.unop hY hX + IsVerdierLeftLocalizing.fac f.unop hY hX exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ -instance (A B : ObjectProperty Cᵒᵖ) [A.IsTriangulatedLeftLocalizing B] : - A.unop.IsTriangulatedRightLocalizing B.unop where +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⟩ := IsTriangulatedLeftLocalizing.fac f.op hY hX + 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.IsTriangulatedRightLocalizing B] : - A.op.IsTriangulatedLeftLocalizing B.op where +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⟩ := IsTriangulatedRightLocalizing.fac f.unop hY hX + 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.IsTriangulatedRightLocalizing B] : - A.unop.IsTriangulatedLeftLocalizing B.unop where +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⟩ := IsTriangulatedRightLocalizing.fac f.op hY hX + 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 isTriangulatedLeftLocalizing_op_iff : - A.op.IsTriangulatedLeftLocalizing B.op ↔ A.IsTriangulatedRightLocalizing B := - ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedRightLocalizing B.op.unop), +lemma isVerdierLeftLocalizing_op_iff : + A.op.IsVerdierLeftLocalizing B.op ↔ A.IsVerdierRightLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsVerdierRightLocalizing B.op.unop), fun _ ↦ inferInstance⟩ -lemma isTriangulatedRightLocalizing_op_iff : - A.op.IsTriangulatedRightLocalizing B.op ↔ A.IsTriangulatedLeftLocalizing B := - ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedLeftLocalizing B.op.unop), +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 isTriangulatedRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] +lemma isVerdierRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : - A.IsTriangulatedRightLocalizing B ↔ + 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⟩ := IsTriangulatedRightLocalizing.fac a hW hX + 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) @@ -119,19 +124,19 @@ lemma isTriangulatedRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] by cat_disch⟩ variable {A B} in -lemma IsTriangulatedRightLocalizing.fac' +lemma IsVerdierRightLocalizing.fac' [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] - [A.IsTriangulatedRightLocalizing B] + [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' := - (isTriangulatedRightLocalizing_iff A B).1 inferInstance s hX hs + (isVerdierRightLocalizing_iff A B).1 inferInstance s hX hs -lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] +lemma isVerdierLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : - A.IsTriangulatedLeftLocalizing B ↔ + 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 [← isTriangulatedRightLocalizing_op_iff, isTriangulatedRightLocalizing_iff] + 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⟩ @@ -139,12 +144,12 @@ lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', by cat_disch⟩ variable {A B} in -lemma IsTriangulatedLeftLocalizing.fac' +lemma IsVerdierLeftLocalizing.fac' [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] - [A.IsTriangulatedLeftLocalizing B] + [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' := - (isTriangulatedLeftLocalizing_iff A B).1 inferInstance s hY hs + (isVerdierLeftLocalizing_iff A B).1 inferInstance s hY hs end ObjectProperty