From 870c82473a6d5eaf2fcdf0cfd32ab68c434ad713 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 16 Feb 2026 08:36:08 +0100 Subject: [PATCH 1/2] feat(CategoryTheory/Triangulated): the heart of a t-structure --- Mathlib.lean | 1 + .../Triangulated/TStructure/Basic.lean | 18 ++++ .../Triangulated/TStructure/Heart.lean | 101 ++++++++++++++++++ 3 files changed, 120 insertions(+) create mode 100644 Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean diff --git a/Mathlib.lean b/Mathlib.lean index cd72d6d36a5d31..7c425be61e07bf 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3235,6 +3235,7 @@ public import Mathlib.CategoryTheory.Triangulated.Rotate public import Mathlib.CategoryTheory.Triangulated.SpectralObject public import Mathlib.CategoryTheory.Triangulated.Subcategory public import Mathlib.CategoryTheory.Triangulated.TStructure.Basic +public import Mathlib.CategoryTheory.Triangulated.TStructure.Heart public import Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE public import Mathlib.CategoryTheory.Triangulated.TriangleShift public import Mathlib.CategoryTheory.Triangulated.Triangulated diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean index 052b91c067e9ee..f7de6472da66c4 100644 --- a/Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean @@ -188,6 +188,24 @@ lemma isGE_of_ge (X : C) (p q : ℤ) (hpq : p ≤ q := by lia) [t.IsGE X q] : t. @[deprecated (since := "2026-01-30")] alias isLE_of_LE := isLE_of_le @[deprecated (since := "2026-01-30")] alias isGE_of_GE := isGE_of_ge +@[simp] +lemma le_iff_isLE (X : C) (n : ℤ) : t.le n X ↔ t.IsLE X n := + ⟨fun h ↦ ⟨h⟩, fun _ ↦ t.le_of_isLE X n⟩ + +@[simp] +lemma ge_iff_isGE (X : C) (n : ℤ) : t.ge n X ↔ t.IsGE X n := + ⟨fun h ↦ ⟨h⟩, fun _ ↦ t.ge_of_isGE X n⟩ + +instance (n : ℤ) : (t.le n).IsClosedUnderIsomorphisms where + of_iso e h := by + simp only [le_iff_isLE] at h ⊢ + exact t.isLE_of_iso e _ + +instance (n : ℤ) : (t.ge n).IsClosedUnderIsomorphisms where + of_iso e h := by + simp only [ge_iff_isGE] at h ⊢ + exact t.isGE_of_iso e _ + lemma isLE_shift (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) [t.IsLE X n] : t.IsLE (X⟦a⟧) n' := ⟨t.le_shift n a n' hn' X (t.le_of_isLE X n)⟩ diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean new file mode 100644 index 00000000000000..cbf9bbda84076f --- /dev/null +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean @@ -0,0 +1,101 @@ +/- +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.Abelian.Basic +public import Mathlib.CategoryTheory.Triangulated.TStructure.Basic + +/-! +# The heart of a t-structures + + +## References +* [Beilinson, Bernstein, Deligne, Gabber, *Faisceaux pervers*][bbd-1982] + +-/ + +@[expose] public section + +namespace CategoryTheory.Triangulated.TStructure + +open Pretriangulated Limits + +variable {C : Type*} [Category* C] [Preadditive C] [HasZeroObject C] [HasShift C ℤ] + [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] + (t : TStructure C) + +/-- The heart of a t-structure, as the property of objects +that are both `≤ 0` and `≥ 0`. -/ +def heart : ObjectProperty C := t.le 0 ⊓ t.ge 0 + deriving ObjectProperty.IsClosedUnderIsomorphisms + +lemma mem_heart_iff (X : C) : + t.heart X ↔ t.IsLE X 0 ∧ t.IsGE X 0 := by + simp [heart] + +/-- Given `t : TStructure C`, a `t.HasHeart` instance consists of a choice +of a preadditive category which identifies to the fullsubcategory of `C` +consisting of the objects satisfying the property `t.heart`. This +category can be accessed as `t.Heart`. -/ +@[nolint checkUnivs] +class HasHeart where + /-- A preadditive category which is equivalent to the fullsubcategory defined by + the property `t.heart`. -/ + H : Type* + /-- The category structure on the heart. -/ + [category : Category H] + /-- The heart is a preadditive category. -/ + [preadditive : Preadditive H] + /-- The inclusion functor. -/ + ι : H ⥤ C + additive_ι : ι.Additive := by infer_instance + fullι : ι.Full := by infer_instance + faithful_ι : ι.Faithful := by infer_instance + essImage_eq_heart : ι.essImage = t.heart := by simp + +/-- Unless a better candidate category is available, the full subcategory +of objects satisfying `t.heart` can be chosen as the heart of a t-structure `t`. -/ +def hasHeartFullSubcategory : t.HasHeart where + H := t.heart.FullSubcategory + ι := t.heart.ι + essImage_eq_heart := by + ext X + exact ⟨fun ⟨⟨Y, hY⟩, ⟨e⟩⟩ ↦ t.heart.prop_of_iso e hY, + fun hX ↦ ⟨⟨X, hX⟩, ⟨Iso.refl _⟩⟩⟩ + +variable [t.HasHeart] + +/-- The heart of a t-structure, when an instance `t.HasHeart` is available. -/ +def Heart := HasHeart.H (t := t) + +instance : Category t.Heart := HasHeart.category + +instance : Preadditive t.Heart := HasHeart.preadditive + +/-- The inclusion functor `t.Heart ⥤ C` of the heart of +a t-structure `t : TStructure C`. -/ +def ιHeart : t.Heart ⥤ C := HasHeart.ι + +instance : t.ιHeart.Full := HasHeart.fullι +instance : t.ιHeart.Faithful := HasHeart.faithful_ι +instance : t.ιHeart.Additive := HasHeart.additive_ι + +@[simp] +lemma essImage_ιHeart : + t.ιHeart.essImage = t.heart := + HasHeart.essImage_eq_heart + +lemma ιHeart_obj_mem (X : t.Heart) : t.heart (t.ιHeart.obj X) := by + rw [← t.essImage_ιHeart] + exact t.ιHeart.obj_mem_essImage X + +instance (X : t.Heart) : t.IsLE (t.ιHeart.obj X) 0 := + ⟨(t.ιHeart_obj_mem X).1⟩ + +instance (X : t.Heart) : t.IsGE (t.ιHeart.obj X) 0 := + ⟨(t.ιHeart_obj_mem X).2⟩ + +end CategoryTheory.Triangulated.TStructure From 08c8f80b5bf0973518023643ea6f680f3e56b9b5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 16 Feb 2026 08:41:41 +0100 Subject: [PATCH 2/2] wip --- .../Triangulated/TStructure/Heart.lean | 21 +++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean index cbf9bbda84076f..78bf23c5d5cab9 100644 --- a/Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean @@ -9,8 +9,19 @@ public import Mathlib.CategoryTheory.Abelian.Basic public import Mathlib.CategoryTheory.Triangulated.TStructure.Basic /-! -# The heart of a t-structures +# The heart of a t-structure +Let `t` be a t-structure on a triangulated category `C`. We define +the heart of `t` as a property `t.heart : ObjectProperty C`. As the +the heart is usually identified to a particular category in the applications +(e.g. the heart of the canonical t-structure on the derived category of +an abelian category `A` identifies to `A`), instead of working +with the full subcategory defined by `t.heart`, we introduce a typeclass +`t.HasHeart` which contains the data of a preadditive category that +is equivalent to it: this heart can be accessed as `t.Heart`. + +## TODO (@joelriou) +* Show that `t.Heart` is an abelian category. ## References * [Beilinson, Bernstein, Deligne, Gabber, *Faisceaux pervers*][bbd-1982] @@ -19,11 +30,13 @@ public import Mathlib.CategoryTheory.Triangulated.TStructure.Basic @[expose] public section +universe v' u' v u + namespace CategoryTheory.Triangulated.TStructure open Pretriangulated Limits -variable {C : Type*} [Category* C] [Preadditive C] [HasZeroObject C] [HasShift C ℤ] +variable {C : Type u} [Category.{v} C] [Preadditive C] [HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) @@ -44,9 +57,9 @@ category can be accessed as `t.Heart`. -/ class HasHeart where /-- A preadditive category which is equivalent to the fullsubcategory defined by the property `t.heart`. -/ - H : Type* + H : Type u' /-- The category structure on the heart. -/ - [category : Category H] + [category : Category.{v'} H] /-- The heart is a preadditive category. -/ [preadditive : Preadditive H] /-- The inclusion functor. -/