English
For k and A, the domain-algebra-hom induced by the identity on G coincides with the identity on MonoidAlgebra A G: mapDomainAlgHom k A (MonoidHom.id G) = AlgHom.id k (MonoidAlgebra A G).
Русский
Для отображения домена и алгебры, индуцированного тождественным отображением на G, получаем тождественный алгебро-гомоморфизм: mapDomainAlgHom k A (MonoidHom.id G) = AlgHom.id k (MonoidAlgebra A G).
LaTeX
$$$\\mathrm{mapDomainAlgHom}\\ k\\;A\\;\\big(\\mathrm{MonoidHom.id}\\ G\\big) = \\mathrm{AlgHom.id}\\ k\\; (\\mathrm{MonoidAlgebra}\\; A\\; G).$$$
Lean4
@[to_additive (attr := simp)]
theorem mapDomainAlgHom_id (k A) [CommSemiring k] [Semiring A] [Algebra k A] :
mapDomainAlgHom k A (MonoidHom.id G) = AlgHom.id k (MonoidAlgebra A G) := by ext;
simp [MonoidHom.id, ← Function.id_def]
