lift_unique — Mathlib

English

A k-algebra homomorphism F is determined by its values on single a 1, namely F(f) = sum over a of f(a) F(single a 1).

Русский

Гомоморфизм F: k[G]→ₐ[k] A определяется значениями на элементах single a 1: F(f) = ∑ a f(a) F(single a 1).

LaTeX

$$$F(f) = \\sum_{a \\in G} f(a) \\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 : 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]

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