English
Let R and S be commutative semirings, A and B be semirings with S- and R-bialgebra structures respectively, and an IsScalarTower relation between R, S and A. The comultiplication on the tensor product A ⊗[R] B, viewed as a coalgebra over S, is obtained by first applying the tensor product of the comultiplications on A and B and then reassembling via the canonical tensor-commutation isomorphism; precisely, comul on A ⊗[R] B equals the composition of the canonical tensor-commutation map with the tensor-product of comuls, viewed as a linear map.
Русский
Пусть R и S — коммутативные полукольца, A и B — полукольца, на A действует структура билингв S, на B — билингв R, при этом есть отношение IsScalarTower между R, S и A. Коумуляция на тензорном произведении A ⊗[R] B, рассматриваемом как коалгебра над S, получается как композиция тензорного отображения комулумов на A и B с каноническим тензорно-коммутирующим сепаратором; точнее, comul на A ⊗[R] B равен композиции (toAlgHom{tensorTensorTensorComm}) ∘ (Algebra.TensorProduct.map(комулAlgHom_SA, комулAlgHom_RB)) с последующим переходом к линейному отображению.
LaTeX
$$$\operatorname{comul}_{S}^{A\otimes_R B} = \left(\left(\operatorname{Algebra.TensorProduct.tensorTensorTensorComm} \; R \; S \; R \; S \; A \; A \; B \; B\right)^{\mathrm{toAlgHom}} \circ \operatorname{Algebra.TensorProduct.map}\left(\mathrm{Bialgebra.comulAlgHom} S A, \mathrm{Bialgebra.comulAlgHom} R B\right)\right)^{\mathrm{toLinearMap}}$$$
Lean4
theorem comul_eq_algHom_toLinearMap :
Coalgebra.comul (R := S) (A := A ⊗[R] B) =
((Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B).toAlgHom.comp
(Algebra.TensorProduct.map (Bialgebra.comulAlgHom S A) (Bialgebra.comulAlgHom R B))).toLinearMap :=
rfl
