English
If A is a bialgebra over R and M is an additive monoid, then AddMonoidAlgebra A M carries a natural bialgebra structure over R.
Русский
Если A — биалгебра над R и M — аддитивный моноид, то AddMonoidAlgebra A M обладает естественной структурой биалгебры над R.
LaTeX
$$AddMonoidAlgebra.instBialgebra R A M$$
Lean4
instance instBialgebra : Bialgebra R A[M]
where
counit_one := by simp only [one_def, counit_single, Bialgebra.counit_one]
mul_compr₂_counit := by ext; simp [single_mul_single]
comul_one := by
simp only [one_def, comul_single, Bialgebra.comul_one, Algebra.TensorProduct.one_def, TensorProduct.map_tmul,
lsingle_apply]
mul_compr₂_comul := by
ext a b c d
simp only [Function.comp_apply, LinearMap.coe_comp, LinearMap.compr₂_apply, LinearMap.mul_apply', single_mul_single,
comul_single, Bialgebra.comul_mul, ← (Coalgebra.Repr.arbitrary R b).eq, ← (Coalgebra.Repr.arbitrary R d).eq,
Finset.sum_mul_sum, Algebra.TensorProduct.tmul_mul_tmul, map_sum, TensorProduct.map_tmul, lsingle_apply,
LinearMap.compl₁₂_apply, LinearMap.coeFn_sum, Finset.sum_apply,
Finset.sum_comm (s := (Coalgebra.Repr.arbitrary R b).index)]
-- TODO: Generalise to `A[M] →ₐc[R] A[N]` under `Bialgebra R A`
