singleFunctors — Mathlib

English

Definition of the collection of all single functors along with their shift compatibilities.

Русский

Определение множества всех одинарных функторов вместе с совместимостями со сдвигами.

LaTeX

$$$\\text{singleFunctors} : C \\mapsto \\text{(collection of functors } C \\to \\text{CochainComplex}(C,\\mathbb{Z}))$$$

Lean4

/-- The collection of all single functors `C ⥤ HomotopyCategory C (ComplexShape.up ℤ))`
for `n : ℤ` along with their compatibilites with shifts. -/
noncomputable def singleFunctors : SingleFunctors C (HomotopyCategory C (ComplexShape.up ℤ)) ℤ :=
  (CochainComplex.singleFunctors C).postcomp (HomotopyCategory.quotient _ _)

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