English
If every component A i is cocommutative over R, then the index-wise direct function space Π₀ i, A i is cocommutative as an R-coalgebra.
Русский
Если у каждого индекса i компонент A_i является кооммутативной относительно R, то пространствo Π₀ i, A_i над R является коалгеброй, кокомутабельной относительно R.
LaTeX
$$$\\big( \\forall i, \\operatorname{IsCocomm} \\; R \\; (A_i) \\big) \\Rightarrow \\operatorname{IsCocomm} \\; R \\; \\Pi_0 i \\; A_i$$$
Lean4
instance instIsCocomm [∀ i, IsCocomm R (A i)] : IsCocomm R (Π₀ i, A i) where
comm_comp_comul :=
by
ext i : 1
-- TODO: Add `reassoc` for `LinearMap`. Then we wouldn't need to reassociate back and forth.
simp only [comp_assoc, comul_comp_lsingle]
simp only [← comp_assoc, ← TensorProduct.map_comp_comm_eq]
simp [LinearMap.comp_assoc]
