feat(CategoryTheory/Triangulated/TStucture): induced t-structures

[joelriou]

This PR introduces a typeclass P.HasInducedTStructure t when P is a triangulated subcategory of a (pre)triangulated category C and t a t-structure on C. This essentially says that P is stable by the truncations. In this situation, we define the induced t-structure on the full subcategory defined by P. In particular, this applies to bounded above/bounded below/bounded objects for a given t-structure.

---

• depends on: feat(CategoryTheory/Triangulated/TStructure): truncLE and truncGT #35364
• depends on: feat(CategoryTheory/Triangulated/TStructure): properties of truncLT and truncGE which use the octahedron axiom #35363
• depends on: feat(CategoryTheory/Triangulated/TStructure): more on truncLT and truncGE #35362

[github-actions]

PR summary 99884c2730

Import changes exceeding 2%

%	File
+7.31%	Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE	1080	1159	+79 (+7.31%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE	79
Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (new file)	1160
Mathlib.CategoryTheory.Triangulated.TStructure.Induced (new file)	1161

---

Declarations diff

+ HasInducedTStructure
+ HasInducedTStructure.mk'
+ descTruncGE
+ descTruncGE_aux
+ descTruncGT
+ descTruncGT_aux
+ from_truncGE_obj_ext
+ instance (P P' : ObjectProperty C) [P.IsTriangulated] [P'.IsTriangulated] (t : TStructure C)
+ instance (X : C) (a b : ℤ) : t.IsGE ((t.truncGELE a b).obj X) a := by
+ instance (X : C) (a b : ℤ) : t.IsGE ((t.truncGELT a b).obj X) a := by
+ instance (X : C) (a b : ℤ) : t.IsLE ((t.truncLTGE a b).obj X) (b - 1) := by
+ instance (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGE b).obj X) a := by
+ instance (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGT b).obj X) a := by
+ instance (X : C) (a b : ℤ) [t.IsLE X b] :
+ instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncGE a).obj X) b := by
+ instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLE a).obj X) b := by
+ instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLT a).obj X) b := by
+ instance (X : C) (n : ℤ) : IsIso ((t.truncGE n).map ((t.truncGEπ n).app X))
+ instance (X : C) (n : ℤ) : IsIso ((t.truncLE n).map ((t.truncLEι n).app X))
+ instance (X : C) (n : ℤ) : IsIso ((t.truncLT n).map ((t.truncLTι n).app X))
+ instance (X : C) (n : ℤ) : t.IsGE ((t.truncGE n).obj X) n
+ instance (X : C) (n : ℤ) : t.IsLE ((t.truncLT (n + 1)).obj X) n
+ instance (X : C) (n : ℤ) : t.IsLE ((t.truncLT n).obj X) (n - 1)
+ instance (X : C) (n : ℤ) [t.IsGE X n] : IsIso ((t.truncGEπ n).app X) := by
+ instance (X : C) (n : ℤ) [t.IsLE X n] : IsIso ((t.truncLEι n).app X) := by
+ instance (a b : ℤ) : IsIso (t.truncGELTToLTGE a b) := by
+ instance (n : ℤ) (X : C) : t.IsGE ((t.truncGT (n - 1)).obj X) n
+ instance (n : ℤ) (X : C) : t.IsGE ((t.truncGT n).obj X) (n + 1)
+ instance (n : ℤ) (X : C) : t.IsLE ((t.truncLE n).obj X) n
+ instance (n : ℤ) : (t.truncGT n).Additive := by
+ instance (n : ℤ) : (t.truncLE n).Additive := by
+ instance (n : ℤ) : t.IsGE (0 : C) n := t.isGE_of_isZero (isZero_zero C) n
+ instance (n : ℤ) : t.IsLE (0 : C) n := t.isLE_of_isZero (isZero_zero C) n
+ instance : t.bounded.HasInducedTStructure t := by
+ instance : t.bounded.IsTriangulated := by
+ instance : t.minus.HasInducedTStructure t
+ instance : t.minus.IsTriangulated
+ instance : t.plus.HasInducedTStructure t
+ instance : t.plus.IsTriangulated
+ isGE_iff_isIso_truncGEπ_app
+ isGE_iff_isIso_truncGTπ_app
+ isGE_iff_isZero_truncLE_obj
+ isGE_iff_isZero_truncLT_obj
+ isGE_iff_orthogonal
+ isGE_of_isZero
+ isGE_truncGE_obj
+ isGE_truncGT_obj
+ isGE₂
+ isIso_truncGE_map_iff
+ isIso_truncGE_map_truncGEπ_app
+ isIso_truncGT_map_iff
+ isIso_truncGT_map_truncGTπ_app
+ isIso_truncLE_map_iff
+ isIso_truncLE_map_truncLEι_app
+ isIso_truncLT_map_iff
+ isIso_truncLT_map_truncLTι_app
+ isIso₁_truncLE_map_of_isGE
+ isIso₁_truncLT_map_of_isGE
+ isIso₂_truncGE_map_of_isLE
+ isIso₂_truncGT_map_of_isLE
+ isLE_iff_isIso_truncLEι_app
+ isLE_iff_isIso_truncLTι_app
+ isLE_iff_isZero_truncGE_obj
+ isLE_iff_isZero_truncGT_obj
+ isLE_iff_orthogonal
+ isLE_of_isZero
+ isLE_truncLE_obj
+ isLE_truncLT_obj
+ isLE₂
+ isZero_truncGE_obj_of_isLE
+ isZero_truncLE_obj_of_isGE
+ isZero_truncLT_obj_of_isGE
+ liftTruncLE
+ liftTruncLE_aux
+ liftTruncLE_ι
+ liftTruncLT
+ liftTruncLT_aux
+ liftTruncLT_ι
+ mem_of_hasInductedTStructure
+ natTransTriangleLTGEOfLE
+ natTransTriangleLTGEOfLE_refl
+ natTransTriangleLTGEOfLE_trans
+ natTransTruncGEOfLE
+ natTransTruncGEOfLE_refl
+ natTransTruncGEOfLE_refl_app
+ natTransTruncGEOfLE_trans
+ natTransTruncGEOfLE_trans_app
+ natTransTruncLEOfLE
+ natTransTruncLEOfLE_refl
+ natTransTruncLEOfLE_refl_app
+ natTransTruncLEOfLE_trans
+ natTransTruncLEOfLE_trans_app
+ natTransTruncLEOfLE_ι
+ natTransTruncLEOfLE_ι_app
+ natTransTruncLTOfLE
+ natTransTruncLTOfLE_refl
+ natTransTruncLTOfLE_refl_app
+ natTransTruncLTOfLE_trans
+ natTransTruncLTOfLE_trans_app
+ natTransTruncLTOfLE_ι
+ natTransTruncLTOfLE_ι_app
+ onBounded
+ onMinus
+ onPlus
+ tStructure
+ tStructure_isGE_iff
+ tStructure_isLE_iff
+ to_truncLE_obj_ext
+ to_truncLT_obj_ext
+ triangleFunctorNatTransOfLE
+ triangleFunctorNatTransOfLE_app_hom₂
+ triangleFunctorNatTransOfLE_refl
+ triangleFunctorNatTransOfLE_trans
+ triangleLEGE
+ triangleLEGEIsoTriangleLTGE
+ triangleLEGE_distinguished
+ triangleLEGT
+ triangleLEGTIsoTriangleLEGE
+ triangleLEGT_distinguished
+ triangleLTLTGELT
+ triangleLTLTGELT_distinguished
+ triangleMapOfLE
+ truncGELE
+ truncGELEIsoLEGE
+ truncGELEIsoTruncGELT
+ truncGELT
+ truncGELTIsoLTGE
+ truncGELTToLTGE
+ truncGELTToLTGE_app_pentagon
+ truncGELTToLTGE_app_pentagon_uniqueness
+ truncGELTδLT
+ truncGE_map_truncGEπ_app
+ truncGEδLE
+ truncGEδLT_comp_natTransTruncLTOfLE_app
+ truncGEδLT_comp_truncLTι
+ truncGEδLT_comp_truncLTι_app
+ truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE
+ truncGEπ_comp_truncGEδLT
+ truncGEπ_comp_truncGEδLT_app
+ truncGEπ_naturality
+ truncGT
+ truncGTIsoTruncGE
+ truncGTδLE
+ truncGTπ
+ truncLE
+ truncLEGE
+ truncLEIsoTruncLT
+ truncLEIsoTruncLT_hom_ι
+ truncLEIsoTruncLT_hom_ι_app
+ truncLEIsoTruncLT_inv_ι
+ truncLEIsoTruncLT_inv_ι_app
+ truncLEι
+ truncLTGE
+ truncLT_map_truncGE_map_truncLTι_app_fac
+ truncLT_map_truncLTι_app
+ truncLTι_comp_truncGEπ
+ truncLTι_comp_truncGEπ_app
+ π_descTruncGE
+ π_descTruncGT
+ π_natTransTruncGEOfLE
+ π_natTransTruncGEOfLE_app
+ π_truncGTIsoTruncGE_hom
+ π_truncGTIsoTruncGE_hom_ι_app
+ π_truncGTIsoTruncGE_inv
+ π_truncGTIsoTruncGE_inv_ι_app
++ instance (a b : ℤ) (X : C) :
+++ instance (X : C) (a b : ℤ) :
+++ instance (X : C) (a b : ℤ) [t.IsGE X a] :
- instance (X : C) (n : ℤ) : t.IsGE ((t.truncGE n).obj X) n := by
- instance (X : C) (n : ℤ) : t.IsLE ((t.truncLT n).obj X) (n - 1) := by

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory/Triangulated/TStructure): truncLE and truncGT #35364
• feat(CategoryTheory/Triangulated/TStructure): properties of truncLT and truncGE which use the octahedron axiom #35363
• feat(CategoryTheory/Triangulated/TStructure): more on truncLT and truncGE #35362
  By Dependent Issues (🤖). Happy coding!