feat(topology/continuous_function/compact): cstar_ring instance on …

…`C(α, β)` when `α` is compact (#14437)

We define the star operation on `C(α, β)` by applying `β`'s star operation pointwise. In the case when `α` is compact, then `C(α, β)` has a norm, and we show that it is a `cstar_ring`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/topology/algebra/star.lean

@@ -64,6 +64,9 @@ lemma continuous_within_at.star (hf : continuous_within_at f s x) :
   continuous_within_at (λ x, star (f x)) s x :=
 hf.star
 
+/-- The star operation bundled as a continuous map. -/
+@[simps] def star_continuous_map : C(R, R) := ⟨star, continuous_star⟩
+
 end continuity
 
 section instances

src/topology/continuous_function/algebra.lean

@@ -7,6 +7,7 @@ import topology.algebra.module.basic
 import topology.continuous_function.ordered
 import topology.algebra.uniform_group
 import topology.uniform_space.compact_convergence
+import topology.algebra.star
 import algebra.algebra.subalgebra.basic
 import tactic.field_simp
 
@@ -756,4 +757,55 @@ ext (λ x, by simpa [mul_add] using @max_eq_half_add_add_abs_sub _ _ (f x) (g x)
 
 end lattice
 
+/-!
+### Star structure
+
+If `β` has a continuous star operation, we put a star structure on `C(α, β)` by using the
+star operation pointwise.
+
+If `β` is a ⋆-ring, then `C(α, β)` inherits a ⋆-ring structure.
+
+If `β` is a ⋆-ring and a ⋆-module over `R`, then the space of continuous functions from `α` to `β`
+is a ⋆-module over `R`.
+
+-/
+
+section star_structure
+variables {R α β : Type*}
+variables [topological_space α] [topological_space β]
+
+section has_star
+variables [has_star β] [has_continuous_star β]
+
+instance : has_star C(α, β) :=
+{ star := λ f, star_continuous_map.comp f }
+
+@[simp] lemma coe_star (f : C(α, β)) : ⇑(star f) = star f := rfl
+
+@[simp] lemma star_apply (f : C(α, β)) (x : α) : star f x = star (f x) := rfl
+
+end has_star
+
+instance [has_involutive_star β] [has_continuous_star β] : has_involutive_star C(α, β) :=
+{ star_involutive := λ f, ext $ λ x, star_star _ }
+
+instance [add_monoid β] [has_continuous_add β] [star_add_monoid β] [has_continuous_star β] :
+  star_add_monoid C(α, β) :=
+{ star_add := λ f g, ext $ λ x, star_add _ _ }
+
+instance [semigroup β] [has_continuous_mul β] [star_semigroup β] [has_continuous_star β] :
+  star_semigroup C(α, β) :=
+{ star_mul := λ f g, ext $ λ x, star_mul _ _ }
+
+instance [non_unital_semiring β] [topological_semiring β] [star_ring β] [has_continuous_star β] :
+  star_ring C(α, β) :=
+{ ..continuous_map.star_add_monoid }
+
+instance [has_star R] [has_star β] [has_scalar R β] [star_module R β]
+  [has_continuous_star β] [has_continuous_const_smul R β] :
+  star_module R C(α, β) :=
+{ star_smul := λ k f, ext $ λ x, star_smul _ _ }
+
+end star_structure
+
 end continuous_map

src/topology/continuous_function/compact.lean

@@ -427,4 +427,54 @@ end
 
 end weierstrass
 
+
+/-!
+### Star structures
+
+In this section, if `β` is a normed ⋆-group, then so is the space of
+continuous functions from `α` to `β`, by using the star operation pointwise.
+
+Furthermore, if `α` is compact and `β` is a C⋆-ring, then `C(α, β)` is a C⋆-ring.  -/
+
+section normed_space
+
+variables {α : Type*} {β : Type*}
+variables [topological_space α] [normed_group β] [star_add_monoid β] [normed_star_group β]
+
+lemma _root_.bounded_continuous_function.mk_of_compact_star [compact_space α] (f : C(α, β)) :
+  mk_of_compact (star f) = star (mk_of_compact f) := rfl
+
+instance [compact_space α] : normed_star_group C(α, β) :=
+{ norm_star := λ f, by rw [←bounded_continuous_function.norm_mk_of_compact,
+                          bounded_continuous_function.mk_of_compact_star, norm_star,
+                          bounded_continuous_function.norm_mk_of_compact] }
+
+end normed_space
+
+section cstar_ring
+
+variables {α : Type*} {β : Type*}
+variables [topological_space α] [normed_ring β] [star_ring β]
+
+instance [compact_space α] [cstar_ring β] : cstar_ring C(α, β) :=
+{ norm_star_mul_self :=
+  begin
+    intros f,
+    refine le_antisymm _ _,
+    { rw [←sq, continuous_map.norm_le _ (sq_nonneg _)],
+      intro x,
+      simp only [continuous_map.coe_mul, coe_star, pi.mul_apply, pi.star_apply,
+                 cstar_ring.norm_star_mul_self, ←sq],
+      refine sq_le_sq' _ _,
+      { linarith [norm_nonneg (f x), norm_nonneg f] },
+      { exact continuous_map.norm_coe_le_norm f x }, },
+    { rw [←sq, ←real.le_sqrt (norm_nonneg _) (norm_nonneg _),
+          continuous_map.norm_le _ (real.sqrt_nonneg _)],
+      intro x,
+      rw [real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ←cstar_ring.norm_star_mul_self],
+      exact continuous_map.norm_coe_le_norm (star f * f) x },
+  end }
+
+end cstar_ring
+
 end continuous_map