English
For a fixed index i, comul composed with the projection to the i-th component (lsingle) equals the tensor-product map that acts on the i-th component after comultiplication in that component.
Русский
Для фиксированного индекса i копуляция после проекции на i-й компонент (lsingle) равна тензорному отображению, действующему только на i-й компоненте после копуляции в этом компоненте.
LaTeX
$$$ \operatorname{comul} \circ \mathrm{lsingle}_{i} = (\mathrm{TensorProduct.map} (\mathrm{lsingle}_{i}) (\mathrm{lsingle}_{i})) \circ \operatorname{comul}_{i}$$$
Lean4
@[simp]
theorem comul_single (i : ι) (a : A i) :
comul (R := R) (DFinsupp.single i a) =
(TensorProduct.map (DFinsupp.lsingle i) (DFinsupp.lsingle i) : _ →ₗ[R] _) (comul a) :=
lsum_single _ _ _ _
