English
A k-algebra homomorphism from MonoidAlgebra k G to A is determined by its values on the basis elements single x 1; two homomorphisms agree on those basis elements are equal.
Русский
K-алгебра-гомоморфизм из MonoidAlgebra k G в A определяется значениями на базисах single x 1; если они согласуются на них, то гомоморфизмы равны.
LaTeX
$$algHom_ext ⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄ (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂$$
Lean4
/-- A `k`-algebra homomorphism from `MonoidAlgebra k G` is uniquely defined by its
values on the functions `single a 1`. -/
@[to_additive (dont_translate := k) /-- A `k`-algebra homomorphism from `k[G]` is uniquely defined by its
values on the functions `single a 1`. -/
]
theorem algHom_ext ⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄ (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
AlgHom.toLinearMap_injective <|
Finsupp.lhom_ext' fun a =>
LinearMap.ext_ring
(h a)
-- The priority must be `high`.
