singleFunctor — Mathlib

English

The family of single functors in the Homotopy category obtained by postcomposing those from CochainComplex with the quotient construction.

Русский

Семейство одинарных функторов в гомотопической категории, получаемое путём посткомпозиции из CochainComplex с факторизацией.

LaTeX

$$$\text{HomotopyCategory.singleFunctors} : C \to \text{HomotopyCategory}(C,\text{ComplexShape.up})$$$

Lean4

/-- The single functor `C ⥤ HomotopyCategory C (ComplexShape.up ℤ)`
which sends `X` to the complex consisting of `X` in degree `n : ℤ` and zero otherwise. -/
noncomputable abbrev singleFunctor (n : ℤ) : C ⥤ HomotopyCategory C (ComplexShape.up ℤ) :=
  (singleFunctors C).functor n

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