feat(Algebra/Homology): the canonical t-structure on the derived category

[joelriou]

---

• depends on: feat(Algebra/Homology): complementary embeddings #27536

[github-actions]

PR summary 7a8536d9ba

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
10 files Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Sites.SheafCohomology.Basic	1
Mathlib.Algebra.Homology.Embedding.AreComplementary (new file)	995
Mathlib.Algebra.Homology.DerivedCategory.TStructure (new file)	1310

---

Declarations diff

+ AreComplementary
+ Boundary
+ IsGE
+ IsLE
+ TStructure.t
+ desc
+ desc'
+ desc'_inl
+ desc'_inr
+ desc.aux
+ desc.aux_trans
+ desc_inl
+ desc_inr
+ embeddingUpInt_areComplementary
+ equiv_inl
+ equiv_inr
+ exists_iso_Q_obj_of_isGE
+ exists_iso_Q_obj_of_isGE_of_isLE
+ exists_iso_Q_obj_of_isLE
+ exists_i₁
+ exists_i₂
+ exists₁
+ exists₂
+ fromSum
+ fromSum_bijective
+ fst
+ fst_inj
+ hom_ext
+ hom_ext'
+ indexOfBoundaryGE
+ indexOfBoundaryLE
+ instance (K : CochainComplex C ℤ) (n : ℤ) [K.IsGE n] :
+ instance (K : CochainComplex C ℤ) (n : ℤ) [K.IsLE n] :
+ instance (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsGE n := by
+ instance (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsLE n := by
+ instance : (Q : _ ⥤ DerivedCategory C).EssSurj
+ instance : (Qh : _ ⥤ DerivedCategory C).EssSurj
+ instance : QuasiIso (K.shortComplexTruncLEX₃ToTruncGE ac)
+ isGE_Q_obj_iff
+ isGE_iff
+ isGE_of_iso
+ isLE_Q_obj_iff
+ isLE_iff
+ isLE_of_iso
+ isStrictlySupportedOutside₁_iff
+ isStrictlySupportedOutside₂_iff
+ isSupportedOutside₁_iff
+ isSupportedOutside₂_iff
+ isZero_of_isGE
+ isZero_of_isLE
+ of_boundaryGE
+ of_boundaryLE
+ shortComplexTruncLE
+ shortComplexTruncLE_shortExact
+ singleFunctorIsoCompQ
+ snd
+ snd_inj
+ symm
++ equiv
++ g_shortComplexTruncLEX₃ToTruncGE
++ shortComplexTruncLEX₃ToTruncGE

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 script/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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Algebra/Homology): complementary embeddings #27536
  By Dependent Issues (🤖). Happy coding!