feat(topology/algebra/module/character_space): Introduce the character space of an algebra (#12838)

The character space of a topological algebra is the subset of elements of the weak dual that are also algebra homomorphisms. This space is used in the Gelfand transform, which gives an isomorphism between a commutative C⋆-algebra and continuous functions on the character space of the algebra. This, in turn, is used to construct the continuous functional calculus on C⋆-algebras.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Author: dupuisf

src/topology/algebra/module/character_space.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2022 Frédéric Dupuis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Frédéric Dupuis
+-/
+
+import topology.algebra.module.weak_dual
+import algebra.algebra.spectrum
+
+/-!
+# Character space of a topological algebra
+
+The character space of a topological algebra is the subset of elements of the weak dual that
+are also algebra homomorphisms. This space is used in the Gelfand transform, which gives an
+isomorphism between a commutative C⋆-algebra and continuous functions on the character space
+of the algebra. This, in turn, is used to construct the continuous functional calculus on
+C⋆-algebras.
+
+
+## Implementation notes
+
+We define `character_space 𝕜 A` as a subset of the weak dual, which automatically puts the
+correct topology on the space. We then define `to_alg_hom` which provides the algebra homomorphism
+corresponding to any element. We also provide `to_clm` which provides the element as a
+continuous linear map. (Even though `weak_dual 𝕜 A` is a type copy of `A →L[𝕜] 𝕜`, this is
+often more convenient.)
+
+## TODO
+
+* Prove that the character space is a compact subset of the weak dual. This requires the
+  Banach-Alaoglu theorem.
+
+## Tags
+
+character space, Gelfand transform, functional calculus
+
+-/
+
+namespace weak_dual
+
+/-- The character space of a topological algebra is the subset of elements of the weak dual that
+are also algebra homomorphisms. -/
+def character_space (𝕜 : Type*) (A : Type*) [comm_semiring 𝕜] [topological_space 𝕜]
+  [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜]
+  [non_unital_non_assoc_semiring A] [topological_space A] [module 𝕜 A] :=
+  {φ : weak_dual 𝕜 A | (φ ≠ 0) ∧ (∀ (x y : A), φ (x * y) = (φ x) * (φ y))}
+
+variables {𝕜 : Type*} {A : Type*}
+
+namespace character_space
+
+section non_unital_non_assoc_semiring
+
+variables [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜]
+  [has_continuous_const_smul 𝕜 𝕜] [non_unital_non_assoc_semiring A] [topological_space A]
+  [module 𝕜 A]
+
+lemma coe_apply (φ : character_space 𝕜 A) (x : A) : (φ : weak_dual 𝕜 A) x = φ x := rfl
+
+/-- An element of the character space, as a continuous linear map. -/
+def to_clm (φ : character_space 𝕜 A) : A →L[𝕜] 𝕜 := (φ : weak_dual 𝕜 A)
+
+lemma to_clm_apply (φ : character_space 𝕜 A) (x : A) : φ x = to_clm φ x := rfl
+
+/-- An element of the character space, as an non-unital algebra homomorphism. -/
+@[simps] def to_non_unital_alg_hom (φ : character_space 𝕜 A) : non_unital_alg_hom 𝕜 A 𝕜 :=
+{ to_fun := (φ : A → 𝕜),
+  map_mul' := φ.prop.2,
+  map_smul' := (to_clm φ).map_smul,
+  map_zero' := continuous_linear_map.map_zero _,
+  map_add' := continuous_linear_map.map_add _ }
+
+lemma map_zero (φ : character_space 𝕜 A) : φ 0 = 0 := (to_non_unital_alg_hom φ).map_zero
+lemma map_add (φ : character_space 𝕜 A) (x y : A) : φ (x + y) = φ x + φ y :=
+  (to_non_unital_alg_hom φ).map_add _ _
+lemma map_smul (φ : character_space 𝕜 A) (r : 𝕜) (x : A) : φ (r • x) = r • (φ x) :=
+  (to_clm φ).map_smul _ _
+lemma map_mul (φ : character_space 𝕜 A) (x y : A) : φ (x * y) = φ x * φ y :=
+  (to_non_unital_alg_hom φ).map_mul _ _
+lemma continuous (φ : character_space 𝕜 A) : continuous φ := (to_clm φ).continuous
+
+end non_unital_non_assoc_semiring
+
+section unital
+
+variables [comm_ring 𝕜] [no_zero_divisors 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜]
+  [has_continuous_const_smul 𝕜 𝕜] [topological_space A] [semiring A] [algebra 𝕜 A]
+
+lemma map_one (φ : character_space 𝕜 A) : φ 1 = 1 :=
+begin
+  have h₁ : (φ 1) * (1 - φ 1) = 0 := by rw [mul_sub, sub_eq_zero, mul_one, ←map_mul φ, one_mul],
+  rcases mul_eq_zero.mp h₁ with h₂|h₂,
+  { exfalso,
+    apply φ.prop.1,
+    ext,
+    rw [continuous_linear_map.zero_apply, ←one_mul x, coe_apply, map_mul φ, h₂, zero_mul] },
+  { rw [sub_eq_zero] at h₂,
+    exact h₂.symm },
+end
+
+/-- An element of the character space, as an algebra homomorphism. -/
+@[simps] def to_alg_hom (φ : character_space 𝕜 A) : A →ₐ[𝕜] 𝕜 :=
+{ map_one' := map_one φ,
+  commutes' := λ r, by
+  { rw [algebra.algebra_map_eq_smul_one, algebra.id.map_eq_id, ring_hom.id_apply],
+    change ((φ : weak_dual 𝕜 A) : A →L[𝕜] 𝕜) (r • 1) = r,
+    rw [continuous_linear_map.map_smul, algebra.id.smul_eq_mul, coe_apply, map_one φ, mul_one] },
+  ..to_non_unital_alg_hom φ }
+
+end unital
+
+section ring
+
+variables [comm_ring 𝕜] [no_zero_divisors 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜]
+  [has_continuous_const_smul 𝕜 𝕜] [topological_space A] [ring A] [algebra 𝕜 A]
+
+lemma apply_mem_spectrum [nontrivial 𝕜] (φ : character_space 𝕜 A) (a : A) : φ a ∈ spectrum 𝕜 a :=
+(to_alg_hom φ).apply_mem_spectrum a
+
+end ring
+
+end character_space
+
+end weak_dual

src/topology/algebra/module/weak_dual.lean

@@ -9,7 +9,7 @@ import topology.algebra.module.basic
 # Weak dual topology
 
 This file defines the weak topology given two vector spaces `E` and `F` over a commutative semiring
-`𝕜` and a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`. The weak topology on `E` is the coarest topology
+`𝕜` and a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`. The weak topology on `E` is the coarsest topology
 such that for all `y : F` every map `λ x, B x y` is continuous.
 
 In the case that `F = E →L[𝕜] 𝕜` and `B` being the canonical pairing, we obtain the weak-* topology,
@@ -180,8 +180,8 @@ weak_bilin (top_dual_pairing 𝕜 E)
 
 instance : inhabited (weak_dual 𝕜 E) := continuous_linear_map.inhabited
 
-instance fun_like_weak_dual : fun_like (weak_dual 𝕜 E) E (λ _, 𝕜) :=
-by {dunfold weak_dual, dunfold weak_bilin, apply_instance}
+instance add_monoid_hom_class_weak_dual : add_monoid_hom_class (weak_dual 𝕜 E) E 𝕜 :=
+continuous_linear_map.add_monoid_hom_class
 
 /-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
 multiplication on `𝕜`, then it acts on `weak_dual 𝕜 E`. -/