English
The tensor product of two bialgebra morphisms is again a bialgebra morphism. Concretely, if f is a S-bialgebra morphism A → C and g is an R-bialgebra morphism B → D, then their tensor product map A ⊗[R] B → C ⊗[R] D is a BialgHom over S.
Русский
Тензорный произведение двух морфизмов билигебр снова является морфизмом билигебр. Пусть f — морфизм билигебр A → C над S, а g — билигебр B → D над R; тогда их тензорный произведение $A\otimes_R B \to C\otimes_R D$ является билигебральным морфизмом над S.
LaTeX
$$$\text{map}(f,g) : A \otimes_R B \to_{S} C \otimes_R D \; \text{is a } BialgHom\; S\; A B\; C D$$$
Lean4
/-- The tensor product of two bialgebra morphisms as a bialgebra morphism. -/
noncomputable def map (f : A →ₐc[S] C) (g : B →ₐc[R] D) : A ⊗[R] B →ₐc[S] C ⊗[R] D :=
{ Coalgebra.TensorProduct.map (f : A →ₗc[S] C) (g : B →ₗc[R] D),
Algebra.TensorProduct.map (f : A →ₐ[S] C) (g : B →ₐ[R] D) with }
