feat(topology/algebra/star): continuity of star (#13855)

This adds the obvious instances for `pi`, `prod`, `units`, `mul_opposite`, `real`, `complex`, `is_R_or_C`, and `matrix`.

We already had a `continuous_star` lemma, but it had stronger typeclass assumptions.

This resolves multiple TODO comments.



Co-authored-by: Johan Commelin <johan@commelin.net>

src/analysis/complex/basic.lean

@@ -197,7 +197,9 @@ det_conj_ae
 @[simp] lemma linear_equiv_det_conj_lie : conj_lie.to_linear_equiv.det = -1 :=
 linear_equiv_det_conj_ae
 
-@[continuity] lemma continuous_conj : continuous (conj : ℂ → ℂ) := conj_lie.continuous
+instance : has_continuous_star ℂ := ⟨conj_lie.continuous⟩
+
+@[continuity] lemma continuous_conj : continuous (conj : ℂ → ℂ) := continuous_star
 
 /-- Continuous linear equiv version of the conj function, from `ℂ` to `ℂ`. -/
 def conj_cle : ℂ ≃L[ℝ] ℂ := conj_lie

src/analysis/normed_space/star/basic.lean

@@ -57,36 +57,9 @@ def star_normed_group_hom : normed_group_hom E E :=
 lemma star_isometry : isometry (star : E → E) :=
 star_add_equiv.to_add_monoid_hom.isometry_of_norm norm_star
 
-lemma continuous_star : continuous (star : E → E) := star_isometry.continuous
-
-lemma continuous_on_star {s : set E} : continuous_on star s := continuous_star.continuous_on
-
-lemma continuous_at_star {x : E} : continuous_at star x := continuous_star.continuous_at
-
-lemma continuous_within_at_star {s : set E} {x : E} : continuous_within_at star s x :=
-continuous_star.continuous_within_at
-
-lemma tendsto_star (x : E) : filter.tendsto star (𝓝 x) (𝓝 x⋆) := continuous_star.tendsto x
-
-lemma filter.tendsto.star {f : α → E} {l : filter α} {y : E} (h : filter.tendsto f l (𝓝 y)) :
-  filter.tendsto (λ x, (f x)⋆) l (𝓝 y⋆) :=
-(continuous_star.tendsto y).comp h
-
-variables [topological_space α]
-
-lemma continuous.star {f : α → E} (hf : continuous f) : continuous (λ y, star (f y)) :=
-continuous_star.comp hf
-
-lemma continuous_at.star {f : α → E} {x : α} (hf : continuous_at f x) :
-  continuous_at (λ x, (f x)⋆) x :=
-continuous_at_star.comp hf
-
-lemma continuous_on.star {f : α → E} {s : set α} (hf : continuous_on f s) :
-  continuous_on (λ x, (f x)⋆) s :=
-continuous_star.comp_continuous_on hf
-
-lemma continuous_within_at.star {f : α → E} {s : set α} {x : α}
-  (hf : continuous_within_at f s x) : continuous_within_at (λ x, (f x)⋆) s x := hf.star
+@[priority 100]
+instance normed_star_group.to_has_continuous_star : has_continuous_star E :=
+⟨star_isometry.continuous⟩
 
 end normed_star_group
 

src/data/complex/is_R_or_C.lean

@@ -846,7 +846,10 @@ noncomputable def conj_cle : K ≃L[ℝ] K := @conj_lie K _
 @[simp, is_R_or_C_simps] lemma conj_cle_norm : ∥(@conj_cle K _ : K →L[ℝ] K)∥ = 1 :=
 (@conj_lie K _).to_linear_isometry.norm_to_continuous_linear_map
 
-@[continuity] lemma continuous_conj : continuous (conj : K → K) := conj_lie.continuous
+@[priority 100]
+instance : has_continuous_star K := ⟨conj_lie.continuous⟩
+
+@[continuity] lemma continuous_conj : continuous (conj : K → K) := continuous_star
 
 /-- The `ℝ → K` coercion, as a linear map -/
 noncomputable def of_real_am : ℝ →ₐ[ℝ] K := algebra.of_id ℝ K

src/topology/algebra/star.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2022 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import algebra.star.pi
+import algebra.star.prod
+import topology.algebra.group
+
+/-!
+# Continuity of `star`
+
+This file defines the `has_continuous_star` typeclass, along with instances on `pi`, `prod`,
+`mul_opposite`, and `units`.
+-/
+
+
+open_locale filter topological_space
+open filter
+
+universes u
+
+variables {ι α R S : Type*}
+
+/-- Basic hypothesis to talk about a topological space with a continuous `star` operator. -/
+class has_continuous_star (R : Type u) [topological_space R] [has_star R] : Prop :=
+(continuous_star : continuous (star : R → R))
+
+export has_continuous_star (continuous_star)
+
+section continuity
+
+variables [topological_space R] [has_star R] [has_continuous_star R]
+
+lemma continuous_on_star {s : set R} : continuous_on star s :=
+continuous_star.continuous_on
+
+lemma continuous_within_at_star {s : set R} {x : R} : continuous_within_at star s x :=
+continuous_star.continuous_within_at
+
+lemma continuous_at_star {x : R} : continuous_at star x :=
+continuous_star.continuous_at
+
+lemma tendsto_star (a : R) : tendsto star (𝓝 a) (𝓝 (star a)) :=
+continuous_at_star
+
+lemma filter.tendsto.star {f : α → R} {l : filter α} {y : R} (h : tendsto f l (𝓝 y)) :
+  tendsto (λ x, star (f x)) l (𝓝 (star y)) :=
+(continuous_star.tendsto y).comp h
+
+variables [topological_space α] {f : α → R} {s : set α} {x : α}
+
+@[continuity]
+lemma continuous.star (hf : continuous f) : continuous (λ x, star (f x)) :=
+continuous_star.comp hf
+
+lemma continuous_at.star (hf : continuous_at f x) : continuous_at (λ x, star (f x)) x :=
+continuous_at_star.comp hf
+
+lemma continuous_on.star (hf : continuous_on f s) : continuous_on (λ x, star (f x)) s :=
+continuous_star.comp_continuous_on hf
+
+lemma continuous_within_at.star (hf : continuous_within_at f s x) :
+  continuous_within_at (λ x, star (f x)) s x :=
+hf.star
+
+end continuity
+
+section instances
+
+instance [has_star R] [has_star S] [topological_space R] [topological_space S]
+  [has_continuous_star R] [has_continuous_star S] : has_continuous_star (R × S) :=
+⟨(continuous_star.comp continuous_fst).prod_mk (continuous_star.comp continuous_snd)⟩
+
+instance {C : ι → Type*} [∀ i, topological_space (C i)]
+  [∀ i, has_star (C i)] [∀ i, has_continuous_star (C i)] : has_continuous_star (Π i, C i) :=
+{ continuous_star := continuous_pi (λ i, continuous.star (continuous_apply i)) }
+
+instance [has_star R] [topological_space R] [has_continuous_star R] : has_continuous_star Rᵐᵒᵖ :=
+⟨mul_opposite.continuous_op.comp $ mul_opposite.continuous_unop.star⟩
+
+instance [monoid R] [star_semigroup R] [topological_space R] [has_continuous_star R] :
+  has_continuous_star Rˣ :=
+⟨continuous_induced_rng units.continuous_embed_product.star⟩
+
+end instances

src/topology/continuous_function/zero_at_infty.lean

@@ -423,15 +423,14 @@ section star
 /-! ### Star structure
 
 It is possible to equip `C₀(α, β)` with a pointwise `star` operation whenever there is a continuous
-`star : β → β` for which `star (0 : β) = 0`. However, we have no such minimal type classes (e.g.,
-`has_continuous_star` or `star_zero_class`) and so the type class assumptions on `β` sufficient to
-guarantee these conditions are `[normed_group β]`, `[star_add_monoid β]` and
-`[normed_star_group β]`, which allow for the corresponding classes on `C₀(α, β)` essentially
-inherited from their counterparts on `α →ᵇ β`. Ultimately, when `β` is a C⋆-ring, then so is
-`C₀(α, β)`.
+`star : β → β` for which `star (0 : β) = 0`. We don't have quite this weak a typeclass, but
+`star_add_monoid` is close enough.
+
+The `star_add_monoid` and `normed_star_group` classes on `C₀(α, β)` are inherited from their
+counterparts on `α →ᵇ β`. Ultimately, when `β` is a C⋆-ring, then so is `C₀(α, β)`.
 -/
 
-variables [normed_group β] [star_add_monoid β] [normed_star_group β]
+variables [topological_space β] [add_monoid β] [star_add_monoid β] [has_continuous_star β]
 
 instance : has_star C₀(α, β) :=
 { star := λ f,
@@ -446,20 +445,26 @@ lemma coe_star (f : C₀(α, β)) : ⇑(star f) = star f := rfl
 lemma star_apply (f : C₀(α, β)) (x : α) :
   (star f) x = star (f x) := rfl
 
-instance : star_add_monoid C₀(α, β) :=
+instance [has_continuous_add β] : star_add_monoid C₀(α, β) :=
 { star_involutive := λ f, ext $ λ x, star_star (f x),
   star_add := λ f g, ext $ λ x, star_add (f x) (g x) }
 
+end star
+
+section normed_star
+
+variables [normed_group β] [star_add_monoid β] [normed_star_group β]
+
 instance : normed_star_group C₀(α, β) :=
 { norm_star := λ f, (norm_star f.to_bcf : _) }
 
-end star
+end normed_star
 
 section star_module
 
-variables {𝕜 : Type*} [semiring 𝕜] [has_star 𝕜]
-  [normed_group β] [star_add_monoid β] [normed_star_group β]
-  [module 𝕜 β] [has_continuous_const_smul 𝕜 β] [star_module 𝕜 β]
+variables {𝕜 : Type*} [has_zero 𝕜] [has_star 𝕜]
+  [add_monoid β] [star_add_monoid β] [topological_space β] [has_continuous_star β]
+  [smul_with_zero 𝕜 β] [has_continuous_const_smul 𝕜 β] [star_module 𝕜 β]
 
 instance : star_module 𝕜 C₀(α, β) :=
 { star_smul := λ k f, ext $ λ x, star_smul k (f x) }
@@ -468,16 +473,21 @@ end star_module
 
 section star_ring
 
-variables [non_unital_normed_ring β] [star_ring β]
+variables [non_unital_semiring β] [star_ring β] [topological_space β] [has_continuous_star β]
+  [topological_semiring β]
 
-instance [normed_star_group β] : star_ring C₀(α, β) :=
+instance : star_ring C₀(α, β) :=
 { star_mul := λ f g, ext $ λ x, star_mul (f x) (g x),
   ..zero_at_infty_continuous_map.star_add_monoid }
 
-instance [cstar_ring β] : cstar_ring C₀(α, β) :=
+end star_ring
+
+section cstar_ring
+
+instance [non_unital_normed_ring β] [star_ring β] [cstar_ring β] : cstar_ring C₀(α, β) :=
 { norm_star_mul_self := λ f, @cstar_ring.norm_star_mul_self _ _ _ _ f.to_bcf }
 
-end star_ring
+end cstar_ring
 
 /-! ### C₀ as a functor
 

src/topology/instances/matrix.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash, Eric Wieser
 -/
 import linear_algebra.determinant
-import topology.algebra.ring
 import topology.algebra.infinite_sum
+import topology.algebra.ring
+import topology.algebra.star
 
 /-!
 # Topological properties of matrices
@@ -69,13 +70,12 @@ lemma continuous.matrix_transpose {A : X → matrix m n R} (hA : continuous A) :
   continuous (λ x, (A x)ᵀ) :=
 continuous_matrix $ λ i j, hA.matrix_elem j i
 
-/-! TODO: add a `has_continuous_star` typeclass so we can write
-```
-lemma continuous.matrix.conj_transpose [has_star R] {A : X → matrix m n R} (hA : continuous A) :
-  continuous (λ x, (A x)ᴴ) :=
+lemma continuous.matrix_conj_transpose [has_star R] [has_continuous_star R] {A : X → matrix m n R}
+  (hA : continuous A) : continuous (λ x, (A x)ᴴ) :=
 hA.matrix_transpose.matrix_map continuous_star
-```
--/
+
+instance [has_star R] [has_continuous_star R] : has_continuous_star (matrix m m R) :=
+⟨continuous_id.matrix_conj_transpose⟩
 
 @[continuity]
 lemma continuous.matrix_col {A : X → n → R} (hA : continuous A) : continuous (λ x, col (A x)) :=
@@ -265,6 +265,31 @@ begin
     rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, transpose_zero] },
 end
 
+lemma has_sum.matrix_conj_transpose [star_add_monoid R] [has_continuous_star R]
+  {f : X → matrix m n R} {a : matrix m n R} (hf : has_sum f a) :
+  has_sum (λ x, (f x)ᴴ) aᴴ :=
+(hf.map (@matrix.conj_transpose_add_equiv m n R _ _) continuous_id.matrix_conj_transpose : _)
+
+lemma summable.matrix_conj_transpose [star_add_monoid R] [has_continuous_star R]
+  {f : X → matrix m n R} (hf : summable f) :
+  summable (λ x, (f x)ᴴ) :=
+hf.has_sum.matrix_conj_transpose.summable
+
+@[simp] lemma summable_matrix_conj_transpose [star_add_monoid R] [has_continuous_star R]
+  {f : X → matrix m n R} :
+  summable (λ x, (f x)ᴴ) ↔ summable f :=
+(summable.map_iff_of_equiv (@matrix.conj_transpose_add_equiv m n R _ _)
+  (@continuous_id (matrix m n R) _).matrix_conj_transpose (continuous_id.matrix_conj_transpose) : _)
+
+lemma matrix.conj_transpose_tsum [star_add_monoid R] [has_continuous_star R] [t2_space R]
+  {f : X → matrix m n R} : (∑' x, f x)ᴴ = ∑' x, (f x)ᴴ :=
+begin
+  by_cases hf : summable f,
+  { exact hf.has_sum.matrix_conj_transpose.tsum_eq.symm },
+  { have hft := summable_matrix_conj_transpose.not.mpr hf,
+    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, conj_transpose_zero] },
+end
+
 lemma has_sum.matrix_diagonal [decidable_eq n] {f : X → n → R} {a : n → R} (hf : has_sum f a) :
   has_sum (λ x, diagonal (f x)) (diagonal a) :=
 (hf.map (diagonal_add_monoid_hom n R) $ continuous.matrix_diagonal $ by exact continuous_id : _)

src/topology/instances/real.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import topology.metric_space.basic
 import topology.algebra.uniform_group
 import topology.algebra.ring
+import topology.algebra.star
 import ring_theory.subring.basic
 import group_theory.archimedean
 import algebra.periodic
@@ -35,6 +36,8 @@ theorem real.uniform_continuous_neg : uniform_continuous (@has_neg.neg ℝ _) :=
 metric.uniform_continuous_iff.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
   by rw dist_comm at h; simpa [real.dist_eq] using h⟩
 
+instance : has_continuous_star ℝ := ⟨continuous_id⟩
+
 instance : uniform_add_group ℝ :=
 uniform_add_group.mk' real.uniform_continuous_add real.uniform_continuous_neg