singleFunctor — Mathlib

English

The abbrev singleFunctor(n) is the functor obtained by restricting the family singleFunctors to a fixed integer n; it sends X to the chain complex with X sitting in degree n.

Русский

Сокращение singleFunctor(n) — это функтор из singleFunctors, фиксирующий целое n; отправляет X в цепной комплекс, в котором X размещено в степени n.

LaTeX

$$$\text{singleFunctor}(n) = (\text{singleFunctors}) \text{ at degree } n$$$

Lean4

/-- The shift functor `C ⥤ DerivedCategory C` which sends `X : C` to the
single cochain complex with `X` sitting in degree `n : ℤ`. -/
noncomputable abbrev singleFunctor (n : ℤ) :=
  (singleFunctors C).functor n

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