feat(analysis/normed_space/star/character_space): compactness of the …

…character space of a normed algebra (#14135)

This PR puts a `compact_space` instance on `character_space 𝕜 A` for a normed algebra `A` using the Banach-Alaoglu theorem. This is a key step in developing the continuous functional calculus.



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

src/analysis/normed_space/algebra.lean

@@ -0,0 +1,58 @@
+/-
+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.character_space
+import analysis.normed_space.weak_dual
+import analysis.normed_space.spectrum
+
+/-!
+# Normed algebras
+
+This file contains basic facts about normed algebras.
+
+## Main results
+
+* We show that the character space of a normed algebra is compact using the Banach-Alaoglu theorem.
+
+## TODO
+
+* Show compactness for topological vector spaces; this requires the TVS version of Banach-Alaoglu.
+
+## Tags
+
+normed algebra, character space, continuous functional calculus
+
+-/
+
+variables {𝕜 : Type*} {A : Type*}
+
+namespace weak_dual
+namespace character_space
+
+variables [nondiscrete_normed_field 𝕜] [normed_ring A]
+  [normed_algebra 𝕜 A] [complete_space A] [norm_one_class A]
+
+lemma norm_one (φ : character_space 𝕜 A) : ∥to_normed_dual (φ : weak_dual 𝕜 A)∥ = 1 :=
+begin
+  refine continuous_linear_map.op_norm_eq_of_bounds zero_le_one (λ a, _) (λ x hx h, _),
+  { rw [one_mul],
+    exact spectrum.norm_le_norm_of_mem (apply_mem_spectrum φ a) },
+  { have : ∥φ 1∥ ≤ x * ∥(1 : A)∥ := h 1,
+    simpa only [norm_one, mul_one, map_one] using this },
+end
+
+instance [proper_space 𝕜] : compact_space (character_space 𝕜 A) :=
+begin
+  rw [←is_compact_iff_compact_space],
+  have h : character_space 𝕜 A ⊆ to_normed_dual ⁻¹' metric.closed_ball 0 1,
+  { intros φ hφ,
+    rw [set.mem_preimage, mem_closed_ball_zero_iff],
+    exact (le_of_eq $ norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ : _), },
+  exact compact_of_is_closed_subset (is_compact_closed_ball 𝕜 0 1) is_closed h,
+end
+
+end character_space
+end weak_dual

src/analysis/normed_space/weak_dual.lean

@@ -142,6 +142,8 @@ mapping). It is a linear equivalence. Here it is implemented as the inverse of t
 equivalence `normed_space.dual.to_weak_dual` in the other direction. -/
 def to_normed_dual : weak_dual 𝕜 E ≃ₗ[𝕜] dual 𝕜 E := normed_space.dual.to_weak_dual.symm
 
+lemma to_normed_dual_apply (x : weak_dual 𝕜 E) (y : E) : (to_normed_dual x) y = x y := rfl
+
 @[simp] lemma coe_to_normed_dual (x' : weak_dual 𝕜 E) : ⇑(x'.to_normed_dual) = x' := rfl
 
 @[simp] lemma to_normed_dual_eq_iff (x' y' : weak_dual 𝕜 E) :

src/topology/algebra/module/character_space.lean

@@ -25,11 +25,6 @@ corresponding to any element. We also provide `to_clm` which provides the elemen
 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
@@ -107,6 +102,28 @@ end
     rw [continuous_linear_map.map_smul, algebra.id.smul_eq_mul, coe_apply, map_one φ, mul_one] },
   ..to_non_unital_alg_hom φ }
 
+lemma eq_set_map_one_map_mul [nontrivial 𝕜] : character_space 𝕜 A =
+  {φ : weak_dual 𝕜 A | (φ 1 = 1) ∧ (∀ (x y : A), φ (x * y) = (φ x) * (φ y))} :=
+begin
+  ext x,
+  refine ⟨λ h, ⟨map_one ⟨x, h⟩, h.2⟩, λ h, ⟨_, h.2⟩⟩,
+  rintro rfl,
+  simpa using h.1,
+end
+
+lemma is_closed [nontrivial 𝕜] [t2_space 𝕜] [has_continuous_mul 𝕜] :
+  is_closed (character_space 𝕜 A) :=
+begin
+  rw [eq_set_map_one_map_mul],
+  refine is_closed.inter (is_closed_eq (eval_continuous _) continuous_const) _,
+  change is_closed {φ : weak_dual 𝕜 A | ∀ x y : A, φ (x * y) = φ x * φ y},
+  rw [set.set_of_forall],
+  refine is_closed_Inter (λ a, _),
+  rw [set.set_of_forall],
+  exact is_closed_Inter (λ _, is_closed_eq (eval_continuous _)
+    ((eval_continuous _).mul (eval_continuous _)))
+end
+
 end unital
 
 section ring