mapDomainRingHom_comp_algebraMap — Mathlib

English

Domain-maps preserve the scalar embedding across monoid algebras: mapDomain f (algebraMap k (MonoidAlgebra A G) r) = algebraMap k (MonoidAlgebra A H) r.

Русский

Карта домена сохраняет скалярное вложение: mapDomain f (algebraMap k (MonoidAlgebra A G) r) = algebraMap k (MonoidAlgebra A H) r.

LaTeX

$$$\\operatorname{mapDomain} f(\\mathrm{algebraMap}_k(\\mathrm{MonoidAlgebra}\\;A\\;G)(r)) = \\mathrm{algebraMap}_k(\\mathrm{MonoidAlgebra}\\;A\\;H)(r)$$$

Lean4

@[to_additive (attr := simp)]
theorem mapDomainRingHom_comp_algebraMap (f : M →* N) :
    (mapDomainRingHom A f).comp (algebraMap R <| MonoidAlgebra A M) = algebraMap R (MonoidAlgebra A N) := by ext; simp

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