English
For any algebra homomorphism F: MonoidAlgebra k G →ₐ[k] A and any f ∈ MonoidAlgebra k G, F(f) equals the finite sum of the coefficients times F applied to basis elements: F(f) = ∑_{a,b} b · F(single a 1), where f = ∑ a b.
Русский
Для любого алгебра-гомоморфизма F: MonoidAlgebra k G →ₐ[k] A и любого f ∈ MonoidAlgebra k G выполняется разложение F(f) по базису: F(f) = ∑_{a} b_a · F(single a 1), если f = ∑ a b_a.
LaTeX
$$$F(f) = \\sum_{a,b} b \\cdot F(\\mathrm{single}(a,1)).$$$
Lean4
/-- Decomposition of a `k`-algebra homomorphism from `MonoidAlgebra k G` by
its values on `F (single a 1)`. -/
theorem lift_unique (F : MonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) :
F f = f.sum fun a b => b • F (single a 1) := by
conv_lhs =>
rw [lift_unique' F]
simp [lift_apply]
