Theorems · Definition · category theory
HasDerivedCategory.standard
(C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : CategoryTheory.Abelian C] → HasDerivedCategory CThe derived category obtained using the constructed localized category of cochain complexes with respect to quasi-isomorphisms. This should be used only while proving statements which do not involve the derived category.
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- CategoryTheory.Abelianstatement and proof · cited by 1,753
- ComplexShape.upproof · cited by 1,123
- HasDerivedCategorystatement · cited by 190
- HomologicalComplex.quasiIsoproof · cited by 42
- CategoryTheory.MorphismProperty.HasLocalization.standardproof · cited by 1
Cited by43
Results whose statement or proof uses this declaration.
- CategoryTheory.HasExt.standardproof · cited by 22
- CategoryTheory.Abelian.Ext.mk₀_comp_mk₀proof · cited by 10
- CategoryTheory.Abelian.Ext.zero_compproof · cited by 10
- CategoryTheory.Abelian.Ext.mk₀_zeroproof · cited by 7
- CategoryTheory.Abelian.Ext.comp_zeroproof · cited by 7
- CategoryTheory.Abelian.Ext.mk₀_id_compproof · cited by 5
- CategoryTheory.Abelian.Ext.comp_mk₀_idproof · cited by 5
- CategoryTheory.Abelian.Ext.eq_zero_of_projectiveproof · cited by 4
- CategoryTheory.Abelian.Ext.hom'statement · cited by 4
- CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁'proof · cited by 4
- CategoryTheory.Abelian.Ext.covariant_sequence_exact₃'proof · cited by 4
- CategoryTheory.Abelian.Ext.eq_zero_of_injectiveproof · cited by 4