English
The coalgebra structure on DFinsupp is given by comul as above and counit as lsum of counits; this defines a coalgebra structure on the DFinsupp type.
Русский
Коалгебраическая структура на DFinsupp задаётся копуляцией и коунитом как выше; это определяет коалгебраическую структуру на тип DFinsupp.
LaTeX
$$$\text{comul}_{\mathrm{DFinsupp}} = \sum_i (\mathrm{lsingle}_i \otimes \mathrm{lsingle}_i) \circ \mathrm{comul}$, $\varepsilon_{\mathrm{DFinsupp}} = \sum_i \varepsilon_i$$$
Lean4
/-- The `R`-module whose elements are dependent functions `(i : ι) → A i` which are zero on all but
finitely many elements of `ι` has a coalgebra structure.
The coproduct `Δ` is given by `Δ(fᵢ a) = fᵢ a₁ ⊗ fᵢ a₂` where `Δ(a) = a₁ ⊗ a₂` and the counit `ε`
by `ε(fᵢ a) = ε(a)`, where `fᵢ a` is the function sending `i` to `a` and all other elements of `ι`
to zero. -/
instance instCoalgebra : Coalgebra R (Π₀ i, A i)
where
rTensor_counit_comp_comul := by
ext : 1
rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle, ← lTensor_comp_rTensor,
comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
lTensor_counit_comp_comul := by
ext : 1
rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, counit_comp_lsingle, ← rTensor_comp_lTensor,
comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
coassoc := by
ext i : 1
simp_rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, comul_comp_lsingle, comp_assoc, ←
comp_assoc comul, rTensor_comp_map, comul_comp_lsingle, ← map_comp_rTensor, ← map_comp_lTensor, comp_assoc, ←
coassoc, ← comp_assoc comul, ← comp_assoc, TensorProduct.map_map_comp_assoc_eq]
