From 2e09d79080f1d1538a2199ac77a6c3696878ea79 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 29 Sep 2022 12:54:41 +0000
Subject: [PATCH] feat(topology/algebra/algebra): `algebra_clm` does not need a
 normed space or field (#16690)

This also clean up the variables in the `topology/algebra/algebra.lean` file, to ensure that the type variables come first (as this is a useful convention for when using `@` notation).
---
 src/analysis/normed_space/basic.lean       | 19 ---------------
 src/analysis/normed_space/exponential.lean |  3 ++-
 src/analysis/normed_space/spectrum.lean    |  2 +-
 src/topology/algebra/algebra.lean          | 27 ++++++++++++++++------
 4 files changed, 23 insertions(+), 28 deletions(-)

diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 462b1fb9034ba..3e5f384e385ef 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -455,25 +455,6 @@ begin
   rw [dist_eq_norm, dist_eq_norm, ← ring_hom.map_sub, norm_algebra_map'],
 end
 
-/-- The inclusion of the base field in a normed algebra as a continuous linear map. -/
-@[simps]
-def algebra_map_clm : 𝕜 →L[𝕜] 𝕜' :=
-{ to_fun := algebra_map 𝕜 𝕜',
-  map_add' := (algebra_map 𝕜 𝕜').map_add,
-  map_smul' := λ r x, by rw [algebra.id.smul_eq_mul, map_mul, ring_hom.id_apply, algebra.smul_def],
-  cont :=
-    have lipschitz_with ∥(1 : 𝕜')∥₊ (algebra_map 𝕜 𝕜') := λ x y, begin
-      rw [edist_eq_coe_nnnorm_sub, edist_eq_coe_nnnorm_sub, ←map_sub, ←ennreal.coe_mul,
-        ennreal.coe_le_coe, mul_comm],
-      exact (nnnorm_algebra_map _ _).le,
-    end, this.continuous }
-
-lemma algebra_map_clm_coe :
-  (algebra_map_clm 𝕜 𝕜' : 𝕜 → 𝕜') = (algebra_map 𝕜 𝕜' : 𝕜 → 𝕜') := rfl
-
-lemma algebra_map_clm_to_linear_map :
-  (algebra_map_clm 𝕜 𝕜').to_linear_map = algebra.linear_map 𝕜 𝕜' := rfl
-
 instance normed_algebra.id : normed_algebra 𝕜 𝕜 :=
 { .. normed_field.to_normed_space,
   .. algebra.id 𝕜}
diff --git a/src/analysis/normed_space/exponential.lean b/src/analysis/normed_space/exponential.lean
index 3135feba55d1b..81581cc4ea78e 100644
--- a/src/analysis/normed_space/exponential.lean
+++ b/src/analysis/normed_space/exponential.lean
@@ -8,6 +8,7 @@ import analysis.analytic.basic
 import analysis.complex.basic
 import data.nat.choose.cast
 import data.finset.noncomm_prod
+import topology.algebra.algebra
 
 /-!
 # Exponential in a Banach algebra
@@ -289,7 +290,7 @@ end complete_algebra
 lemma algebra_map_exp_comm_of_mem_ball [complete_space 𝕂] (x : 𝕂)
   (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) :
   algebra_map 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebra_map 𝕂 𝔸 x) :=
-map_exp_of_mem_ball _ (algebra_map_clm _ _).continuous _ hx
+map_exp_of_mem_ball _ (continuous_algebra_map 𝕂 𝔸) _ hx
 
 end any_field_any_algebra
 
diff --git a/src/analysis/normed_space/spectrum.lean b/src/analysis/normed_space/spectrum.lean
index 1529e7b246779..995ef43a4dc3b 100644
--- a/src/analysis/normed_space/spectrum.lean
+++ b/src/analysis/normed_space/spectrum.lean
@@ -71,7 +71,7 @@ not_not.mp $ λ hn, h.not_le $ le_supr₂ k hn
 variable [complete_space A]
 
 lemma is_open_resolvent_set (a : A) : is_open (ρ a) :=
-units.is_open.preimage ((algebra_map_clm 𝕜 A).continuous.sub continuous_const)
+units.is_open.preimage ((continuous_algebra_map 𝕜 A).sub continuous_const)
 
 lemma is_closed (a : A) : is_closed (σ a) :=
 (is_open_resolvent_set a).is_closed_compl
diff --git a/src/topology/algebra/algebra.lean b/src/topology/algebra/algebra.lean
index a339814d41144..f79c7f66f4cc1 100644
--- a/src/topology/algebra/algebra.lean
+++ b/src/topology/algebra/algebra.lean
@@ -28,11 +28,11 @@ open_locale classical
 universes u v w
 
 section topological_algebra
-variables (R : Type*) [topological_space R] [comm_semiring R]
-variables (A : Type u) [topological_space A]
-variables [semiring A]
+variables (R : Type*) (A : Type u)
+variables [comm_semiring R] [semiring A] [algebra R A]
+variables [topological_space R] [topological_space A] [topological_semiring A]
 
-lemma continuous_algebra_map_iff_smul [algebra R A] [topological_semiring A] :
+lemma continuous_algebra_map_iff_smul :
   continuous (algebra_map R A) ↔ continuous (λ p : R × A, p.1 • p.2) :=
 begin
   refine ⟨λ h, _, λ h, _⟩,
@@ -41,15 +41,28 @@ begin
 end
 
 @[continuity]
-lemma continuous_algebra_map [algebra R A] [topological_semiring A] [has_continuous_smul R A] :
+lemma continuous_algebra_map [has_continuous_smul R A] :
   continuous (algebra_map R A) :=
 (continuous_algebra_map_iff_smul R A).2 continuous_smul
 
-lemma has_continuous_smul_of_algebra_map [algebra R A] [topological_semiring A]
-  (h : continuous (algebra_map R A)) :
+lemma has_continuous_smul_of_algebra_map (h : continuous (algebra_map R A)) :
   has_continuous_smul R A :=
 ⟨(continuous_algebra_map_iff_smul R A).1 h⟩
 
+variables [has_continuous_smul R A]
+
+/-- The inclusion of the base ring in a topological algebra as a continuous linear map. -/
+@[simps]
+def algebra_map_clm : R →L[R] A :=
+{ to_fun := algebra_map R A,
+  cont := continuous_algebra_map R A,
+  .. algebra.linear_map R A }
+
+lemma algebra_map_clm_coe : ⇑(algebra_map_clm R A) = algebra_map R A := rfl
+
+lemma algebra_map_clm_to_linear_map :
+  (algebra_map_clm R A).to_linear_map = algebra.linear_map R A := rfl
+
 end topological_algebra
 
 section topological_algebra