singleOneAlgHom — Mathlib

English

There is a natural equivalence between monoid homomorphisms G →* A and algebra homomorphisms MonoidAlgebra k G →ₐ[k] A.

Русский

Существует естественное эквивалентное соответствие между гомоморфизмами моноидов G →* A и алгебра-гомоморфизмами MonoidAlgebra k G →ₐ[k] A.

LaTeX

$$$\\mathrm{lift} : (G \\to* A) \\simeq (MonoidAlgebra k G \\toₐ[k] A)$$$

Lean4

/-- `Finsupp.single 1` as an `AlgHom` -/
@[to_additive (dont_translate := k A) (attr := simps! apply) /-- `Finsupp.single 0` as an `AlgHom` -/
    ]
def singleOneAlgHom {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : A →ₐ[k] MonoidAlgebra A G :=
  { singleOneRingHom with
    commutes' := fun r => by
      ext
      simp
      rfl }

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