English
Given a separating family X : α → C and a loopless complex shape c, the indexed family in HomologicalComplex C c, defined by separatingFamily c X, is a separating family in degree range α × ι, consisting of complexes nonzero in at most two consecutive degrees.
Русский
Пусть X : α → C является разделяющей семейством и c — форма комплекса без петель. Тогда семейство, заданное separatingFamily c X на индексах α × ι, образует разделяющее множество в HomologicalComplex C c, и каждый комплекс ненулевой в не более чем двух последовательных степенях.
LaTeX
$$$\text{Let } X: \alpha \to C \text{ be separating and } c \text{ have no loop}.\quad \mathrm{separatingFamily}\,c\,X : (\alpha\times \iota) \to \mathrm{HomologicalComplex}(C,c) \text{ is a separating family.}$$$
Lean4
/-- If `X : α → C` is a separating family, and `c : ComplexShape ι` has no loop,
then this is a separating family indexed by `α × ι` in `HomologicalComplex C c`,
which consists of homological complexes that are nonzero in at most
two (consecutive) degrees. -/
noncomputable def separatingFamily (j : α × ι) : HomologicalComplex C c :=
evalCompCoyonedaCorepresentative c (X j.1) j.2
