feat(analysis/normed_space/spectrum): an algebra homomorphism into th…

…e base field is bounded (#11494)

We prove basic facts about `φ : A →ₐ[𝕜] 𝕜` when `A` is a Banach algebra, namely that `φ` maps elements of `A` to their spectrum, and that `φ` is bounded.



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

src/algebra/algebra/spectrum.lean

@@ -329,3 +329,20 @@ end
 end scalar_field
 
 end spectrum
+
+namespace alg_hom
+
+variables {R : Type*} {A : Type*} [comm_ring R] [ring A] [algebra R A]
+local notation `σ` := spectrum R
+local notation `↑ₐ` := algebra_map R A
+
+lemma apply_mem_spectrum [nontrivial R] (φ : A →ₐ[R] R) (a : A) : φ a ∈ σ a :=
+begin
+  have h : ↑ₐ(φ a) - a ∈ φ.to_ring_hom.ker,
+  { simp only [ring_hom.mem_ker, coe_to_ring_hom, commutes, algebra.id.map_eq_id,
+               to_ring_hom_eq_coe, ring_hom.id_apply, sub_self, map_sub] },
+  simp only [spectrum.mem_iff, ←mem_nonunits_iff,
+             coe_subset_nonunits (φ.to_ring_hom.ker_ne_top) h],
+end
+
+end alg_hom

src/analysis/normed_space/spectrum.lean

@@ -45,11 +45,12 @@ noncomputable def spectral_radius (𝕜 : Type*) {A : Type*} [normed_field 𝕜]
   [algebra 𝕜 A] (a : A) : ℝ≥0∞ :=
 ⨆ k ∈ spectrum 𝕜 a, ∥k∥₊
 
+variables {𝕜 : Type*} {A : Type*}
+
 namespace spectrum
 
 section spectrum_compact
 
-variables {𝕜 : Type*} {A : Type*}
 variables [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
 
 local notation `σ` := spectrum 𝕜
@@ -114,7 +115,6 @@ end spectrum_compact
 
 section resolvent_deriv
 
-variables {𝕜 : Type*} {A : Type*}
 variables [nondiscrete_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
 
 local notation `ρ` := resolvent_set 𝕜
@@ -132,3 +132,33 @@ end
 end resolvent_deriv
 
 end spectrum
+
+namespace alg_hom
+
+section normed_field
+variables [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
+local notation `↑ₐ` := algebra_map 𝕜 A
+
+/-- An algebra homomorphism into the base field, as a continuous linear map (since it is
+automatically bounded). -/
+@[simps] def to_continuous_linear_map (φ : A →ₐ[𝕜] 𝕜) : A →L[𝕜] 𝕜 :=
+φ.to_linear_map.mk_continuous_of_exists_bound $
+  ⟨1, λ a, (one_mul ∥a∥).symm ▸ spectrum.norm_le_norm_of_mem (φ.apply_mem_spectrum _)⟩
+
+lemma continuous (φ : A →ₐ[𝕜] 𝕜) : continuous φ := φ.to_continuous_linear_map.continuous
+
+end normed_field
+
+section nondiscrete_normed_field
+variables [nondiscrete_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
+local notation `↑ₐ` := algebra_map 𝕜 A
+
+@[simp] lemma to_continuous_linear_map_norm [norm_one_class A] (φ : A →ₐ[𝕜] 𝕜) :
+  ∥φ.to_continuous_linear_map∥ = 1 :=
+continuous_linear_map.op_norm_eq_of_bounds zero_le_one
+  (λ a, (one_mul ∥a∥).symm ▸ spectrum.norm_le_norm_of_mem (φ.apply_mem_spectrum _))
+  (λ _ _ h, by simpa only [to_continuous_linear_map_apply, mul_one, map_one, norm_one] using h 1)
+
+end nondiscrete_normed_field
+
+end alg_hom

src/ring_theory/ideal/operations.lean

@@ -1270,6 +1270,9 @@ by rw [ring_hom.ker_eq_comap_bot, ideal.comap_comap, ring_hom.ker_eq_comap_bot]
 lemma not_one_mem_ker [nontrivial S] (f : R →+* S) : (1:R) ∉ ker f :=
 by { rw [mem_ker, f.map_one], exact one_ne_zero }
 
+lemma ker_ne_top [nontrivial S] (f : R →+* S) : f.ker ≠ ⊤ :=
+(ideal.ne_top_iff_one _).mpr $ not_one_mem_ker f
+
 end semiring
 
 section ring