Theorems · Theorem · category theory

CochainComplex.isLE_shift

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n : ℤ) [K.IsLE n] (a n' : ℤ),
  a + n' = n → ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsLE n'

Defined in

Mathlib.Algebra.Homology.Embedding.CochainComplex

Cited by

0 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.CategoryWithHomologyCochainComplex.IsLE