English
The Gelfand transform is an algebra homomorphism from A to the algebra of continuous 𝕜-valued functions on the character space, defined by (gelfandTransform(a))(φ) = φ(a).
Русский
Гелфанд-трансформ — это алгебро-гомоморфизм из A в алгебру непрерывных функций на пространстве характеров, заданный формулой (gelfandTransform(a))(φ) = φ(a).
LaTeX
$$$\mathrm{gelfandTransform}: A \to_{\mathbb{k}} C\big(\mathrm{Char}_{\mathbb{k}}(A), \mathbb{k}\big), \quad a \mapsto (\phi \mapsto \phi(a)).$$$
Lean4
/-- The **Gelfand transform** is an algebra homomorphism (over `𝕜`) from a topological `𝕜`-algebra
`A` into the `𝕜`-algebra of continuous `𝕜`-valued functions on the `characterSpace 𝕜 A`.
The character space itself consists of all algebra homomorphisms from `A` to `𝕜`. -/
@[simps]
def gelfandTransform : A →ₐ[𝕜] C(characterSpace 𝕜 A, 𝕜)
where
toFun
a :=
{ toFun := fun φ => φ a
continuous_toFun := (eval_continuous a).comp continuous_induced_dom }
map_one' := by ext a; simp only [coe_mk, coe_one, Pi.one_apply, map_one a]
map_mul' a b := by ext; simp only [map_mul, coe_mk, coe_mul, Pi.mul_apply]
map_zero' := by ext; simp only [map_zero, coe_mk, coe_zero, Pi.zero_apply]
map_add' a b := by ext; simp only [map_add, coe_mk, coe_add, Pi.add_apply]
commutes' k := by ext; simp [AlgHomClass.commutes]
