mapDomainBialgHom — Mathlib

English

The map induced by the identity monoid hom on M is the identity endomorphism on the monoid algebra: mapDomainBialgHom R (.id M) = .id _ _.

Русский

Отображение domain, индуцированное тождественным морфизмом моноида на M, есть тождественный эндоморфизм на монодном алгебраическом объекте.

LaTeX

$$$\text{mapDomainBialgHom } R (\mathrm{id}_M) = \mathrm{id}_{R[M]}$$$

Lean4

/-- If `f : M → N` is a monoid hom, then `MonoidAlgebra.mapDomain f` is a bialgebra hom between
their monoid algebras. -/
@[simps!]
noncomputable def mapDomainBialgHom (f : M →* N) : MonoidAlgebra R M →ₐc[R] MonoidAlgebra R N :=
  .ofAlgHom (mapDomainAlgHom R R f) (by ext; simp) (by ext; simp)

Похожие утверждения