English
For every finite subset s of the index set, there is a canonical additive group homomorphism that sends a family of elements indexed by s to the full dependent product, by placing the given elements in coordinates in s and zeros elsewhere.
Русский
Пусть s — конечное подмножество индексов. Существует канонический аддитивный гомоморфизм, переходящий семейство элементов, индексируемых по s, в полный зависимый произведение, отправляющий (x_i) на функцию i ↦ x_i если i ∈ s и 0 иначе.
LaTeX
$$$\\text{mk}_s: \\prod_{i \\in s} \\beta_i \\to \\prod_{i \\in \\iota} \\beta_i,\\quad (x_i)_{i \\in s} \\mapsto (i \\mapsto \\begin{cases} x_i & i \\in s \\\\ 0 & i \\notin s \\end{cases}).$$$
Lean4
/-- If `s` is a subset of `ι` then `mk_addGroupHom s` is the canonical additive
group homomorphism from $\prod_{i\in s}\beta_i$ to $\prod_{\mathtt{i : \iota}}\beta_i$. -/
def mkAddGroupHom [∀ i, AddGroup (β i)] (s : Finset ι) : (∀ i : (s : Set ι), β ↑i) →+ Π₀ i : ι, β i
where
toFun := mk s
map_zero' := mk_zero
map_add' _ _ := mk_add
