English
If each component A_i is cocommutative, then the Finsupp space ι →₀ A is cocommutative.
Русский
Если каждая A_i кококоммутативна, то Finsupp ι →₀ A кокономмутативна.
LaTeX
$$$\text{IsCocomm}_{R}(\,\iota \to A_{i}\,)$ with Δ commuting under the flip on the tensor product.$$
Lean4
/-- The `R`-module whose elements are functions `ι → A` 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. -/
noncomputable instance instCoalgebra : Coalgebra R (ι →₀ A)
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]
