singleFunctor — Mathlib

English

The canonical functor from C to CochainComplex C ℤ that places X in degree n and zeros elsewhere.

Русский

Канонический функтор от C к CochainComplex C ℤ, отправляющий объект X в степень n и нули в остальных степенях.

LaTeX

$$$\text{singleFunctor}(n) : C \to \text{CochainComplex } C \mathbb{Z}$$$

Lean4

/-- 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.) -/
noncomputable abbrev singleFunctor (n : ℤ) :=
  (singleFunctors C).functor n

Похожие утверждения