English
For coalgebra morphisms f and g, the map on the tensor product sends tmul x y to tmul (f x) (g y).
Русский
Для коалгебра морфизмов f и g отображение на тензорном произведении отправляет tmul x y в tmul (f x) (g y).
LaTeX
$$$\mathrm{map}\;f\;g\; (x \otimes y) = f(x) \otimes g(y).$$$
Lean4
/-- The tensor product of two coalgebra morphisms as a coalgebra morphism. -/
noncomputable def map (f : M →ₗc[S] N) (g : P →ₗc[R] Q) : M ⊗[R] P →ₗc[S] N ⊗[R] Q
where
toLinearMap := AlgebraTensorModule.map f.toLinearMap g.toLinearMap
counit_comp := by ext; simp
map_comp_comul := by
ext x y
dsimp
simp only [← CoalgHomClass.map_comp_comul_apply]
hopf_tensor_induction comul (R := S) x with x₁ x₂
hopf_tensor_induction comul (R := R) y with y₁ y₂
simp
