feat(CategoryTheory/Triangulated): the heart of a t-structure

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

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)⟩

Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean

@@ -0,0 +1,114 @@
+/-
+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-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]
+
+-/
+
+@[expose] public section
+
+universe v' u' v u
+
+namespace CategoryTheory.Triangulated.TStructure
+
+open Pretriangulated Limits
+
+variable {C : Type u} [Category.{v} 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 u'
+  /-- The category structure on the heart. -/
+  [category : Category.{v'} 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