noncomputable def Coalgebra.comulCoalgHom (R : Type u_1) (C : Type u_2) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [IsCocomm R C] : C →ₗc[R] TensorProduct R C C

Comultiplication as a coalgebra hom.

Equations

• Coalgebra.comulCoalgHom R C = { toLinearMap := CoalgebraStruct.comul, counit_comp := ⋯, map_comp_comul := ⋯ }