English
The R-module of finitely supported functions ι → A carries a coalgebra structure, with comul and counit built from those of A by summing over indices using lsum and lsingle maps.
Русский
Модуль R на множество конечной поддержки функций ι → A имеет коалгебраическую структуру, копуляция и коунит строятся на основе копуляции A через суммирование по индексам с помощью lsum и lsingle.
LaTeX
$$$\Delta_{\mathrm{Finsupp}} = \sum_i (\mathrm{Finsupp.lsingle}_i \, \otimes \; \mathrm{Finsupp.lsingle}_i) \circ \Delta$, $\varepsilon_{\mathrm{Finsupp}} = \sum_i \varepsilon_i$$$
Lean4
noncomputable instance instCoalgebraStruct : CoalgebraStruct R (ι →₀ A)
where
comul := Finsupp.lsum R fun i => TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i) ∘ₗ comul
counit := Finsupp.lsum R fun _ => counit
