isLocalHom_singleOneAlgHom — Mathlib

English

The map sending a to the basis monomial corresponding to 1 in the MonoidAlgebra is a local homomorphism.

Русский

Отображение, отправляющее элемент a в базисный моном 1 в MonoidAlgebra, является локальным гомоморфизмом.

LaTeX

$$IsLocalHom (singleOneAlgHom : A →ₐ[k] MonoidAlgebra A G)$$

Lean4

@[to_additive]
instance isLocalHom_singleOneAlgHom {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
    IsLocalHom (singleOneAlgHom : A →ₐ[k] MonoidAlgebra A G) where
  map_nonunit := isLocalHom_singleOneRingHom.map_nonunit

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