Theorems · Definition · category theory
DerivedCategory.TStructure.t
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.Abelian C] →
[inst_2 : HasDerivedCategory C] → CategoryTheory.Triangulated.TStructure (DerivedCategory C)The canonical t-structure on DerivedCategory C.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.Isoproof · cited by 3,963
- CategoryTheory.Abelianstatement and proof · cited by 1,753
- CochainComplexproof · cited by 1,016
- CategoryTheory.Triangulated.TStructurestatement · cited by 318
- HasDerivedCategorystatement and proof · cited by 190
- DerivedCategorystatement and proof · cited by 165
- DerivedCategory.Qproof · cited by 102
- CochainComplex.IsStrictlyGEproof · cited by 34
- CochainComplex.IsStrictlyLEproof · cited by 20
Cited by31
Results whose statement or proof uses this declaration.
- DerivedCategory.IsGEproof · cited by 8
- DerivedCategory.IsLEproof · cited by 7
- DerivedCategory.Plusproof · cited by 7
- DerivedCategory.Plus.ιstatement and proof · cited by 6
- DerivedCategory.Plus.homologyFunctorstatement · cited by 3
- CochainComplex.Plus.modelCategoryQuillen.exists_quasiIso_injectiveproof · cited by 1
- DerivedCategory.isGE_iffproof · cited by 1
- DerivedCategory.isLE_iffproof · cited by 1
- DerivedCategory.Plus.Qstatement · cited by 1
- DerivedCategory.Plus.Qhstatement and proof · cited by 1
- DerivedCategory.Plus.isGE_ι_obj_iffstatement · cited by 1
- DerivedCategory.exists_iso_Q_obj_of_isGEproof · cited by 1