Mathlib Map

Theorems · Theorem · category theory

DerivedCategory.isLE_iff

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ),
  X.IsLE n ↔ ∀ (i : ℤ), n < i → CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor C i).obj X)
Defined in
Mathlib.Algebra.Homology.DerivedCategory.TStructure
Cited by
1 results in Mathlib
Foundations
Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategory
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

DerivedCategory.isZero_of_isLE · cited by 1DerivedCategory.isZero_of…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.Functor.obj · cited by 19642Functor.objCategoryTheory.Functor.map · cited by 8698Functor.mapCategoryTheory.Iso · cited by 3963CategoryTheory.IsoCategoryTheory.Abelian · cited by 1753CategoryTheory.AbelianCochainComplex · cited by 1016CochainComplexCategoryTheory.Iso.symm · cited by 993Iso.symmCategoryTheory.Iso.trans · cited by 566Iso.transCategoryTheory.Limits.IsZero · cited by 306Limits.IsZeroCategoryTheory.Iso.app · cited by 253Iso.appCategoryTheory.Functor.mapIso · cited by 224Functor.mapIsoHasDerivedCategory · cited by 190HasDerivedCategoryCategoryTheory.asIso · cited by 177CategoryTheory.asIsoDerivedCategory · cited by 165DerivedCategoryDerivedCategory.Q · cited by 102DerivedCategory.QDerivedCategory.isLE_iffCITED BYCITES

Cites32

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.