The monoid-algebra counit is the coefficient sum

This identifies the bialgebra counit with the augmentation used in the ideal-theoretic exactness of monoid algebras, and the bialgebra map induced by a monoid homomorphism with the ring map MonoidAlgebra.mapDomainRingHom appearing there.

@[simp]

theorem TauCeti.MonoidAlgebra.counitAlgHom_toRingHom (R : Type u_1) (M : Type u_2) [CommRing R] [Monoid M] : ↑(Bialgebra.counitAlgHom R (MonoidAlgebra R M)) = augmentation R M

The counit of a monoid algebra over its coefficient ring is its coefficient-sum augmentation.

@[simp]

theorem TauCeti.MonoidAlgebra.mapDomainBialgHom_toRingHom (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommSemiring R] [Monoid M] [Monoid N] (f : M →* N) : ↑↑(MonoidAlgebra.mapDomainBialgHom R f) = MonoidAlgebra.mapDomainRingHom R f

The bialgebra map of monoid algebras induced by a monoid homomorphism is, as a ring homomorphism, MonoidAlgebra.mapDomainRingHom.