Theorems · Definition · category theory

CochainComplex.singleFunctor

(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasZeroObject C] → ℤ → CategoryTheory.Functor C (CochainComplex C ℤ)

The single functor C ⥤ CochainComplex C ℤ which sends X to the complex consisting of X in degree n : ℤ and zero otherwise. (This is definitionally equal to HomologicalComplex.single C (up ℤ) n, but singleFunctor C n is the preferred term when interactions with shifts are relevant.)

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Cited by

111 results in Mathlib

Foundations

Depth 66 from the axioms, rests on 1,235 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Limits.HasZeroObject