isLocalHom_algebraMap — Mathlib

English

If the base algebra map is a local-hom, then the induced map to MonoidAlgebra is also a local-hom.

Русский

Если базовый алгебра-гомоморфизм является локальным, то индуцируемый переход в MonoidAlgebra тоже локален.

LaTeX

$$IsLocalHom (algebraMap k (MonoidAlgebra A G))$$

Lean4

@[to_additive (dont_translate := k)]
instance isLocalHom_algebraMap {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G]
    [IsLocalHom (algebraMap k A)] : IsLocalHom (algebraMap k (MonoidAlgebra A G)) where
  map_nonunit _ hx := .of_map _ _ <| isLocalHom_singleOneAlgHom (k := k).map_nonunit _ hx

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