comul_single — Mathlib

English

If every A_i is cocommutative over R, then the Finsupp space ι →₀ A carries a cocommutative coalgebra structure.

Русский

Если каждая A_i кококоммутативна над R, то Finsupp ι →₀ A обладает кококоммутативной коалгебраической структурой.

LaTeX

$$$\text{IsCocomm}_{R} (\Pi_0 i, A_i)$ with $\Delta = \sum_i (\mathrm{lsingle}_i \otimes \mathrm{lsingle}_i) \circ \Delta_i$ and $\varepsilon = \sum_i \varepsilon_i$$$

Lean4

@[simp]
theorem comul_single (i : ι) (a : A) :
    comul (R := R) (Finsupp.single i a) =
      (TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i) : _ →ₗ[R] _) (comul a) :=
  lsum_single _ _ _ _

Похожие утверждения