From 8f9efd688432cbbfe92c32a0b0b06c4d715f5c77 Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Mon, 22 Aug 2022 23:29:07 +0000
Subject: [PATCH] feat(topology/algebra/module/character_space): provide
 instances of `continuous_linear_map_class`, `non_unital_alg_hom_class` and
 `alg_hom_class` (#16178)

This updates `character_space` to utilize the new hom classes `continuous_linear_map_class`, `non_unital_alg_hom_class` and `alg_hom_class`. Also performs some minor housekeeping related to `simp` lemmas.
---
 .../algebra/module/character_space.lean       | 76 +++++++++++--------
 1 file changed, 45 insertions(+), 31 deletions(-)

diff --git a/src/topology/algebra/module/character_space.lean b/src/topology/algebra/module/character_space.lean
index d937e17b09bc9..ff31ed7f83132 100644
--- a/src/topology/algebra/module/character_space.lean
+++ b/src/topology/algebra/module/character_space.lean
@@ -50,29 +50,39 @@ variables [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜
   [has_continuous_const_smul 𝕜 𝕜] [non_unital_non_assoc_semiring A] [topological_space A]
   [module 𝕜 A]
 
-lemma coe_apply (φ : character_space 𝕜 A) (x : A) : (φ : weak_dual 𝕜 A) x = φ x := rfl
+@[simp, norm_cast, protected]
+lemma coe_coe (φ : character_space 𝕜 A) : ⇑(φ : weak_dual 𝕜 A) = φ := rfl
+
+/-- Elements of the character space are continuous linear maps. -/
+instance : continuous_linear_map_class (character_space 𝕜 A) 𝕜 A 𝕜 :=
+{ coe := λ φ, (φ : A → 𝕜),
+  coe_injective' := λ φ ψ h, by { ext, exact congr_fun h x },
+  map_smulₛₗ := λ φ, (φ : weak_dual 𝕜 A).map_smul,
+  map_add := λ φ, (φ : weak_dual 𝕜 A).map_add,
+  map_continuous := λ φ, (φ : weak_dual 𝕜 A).cont }
 
 /-- An element of the character space, as a continuous linear map. -/
 def to_clm (φ : character_space 𝕜 A) : A →L[𝕜] 𝕜 := (φ : weak_dual 𝕜 A)
 
-lemma to_clm_apply (φ : character_space 𝕜 A) (x : A) : φ x = to_clm φ x := rfl
+@[simp] lemma coe_to_clm (φ : character_space 𝕜 A) : ⇑(to_clm φ) = φ := rfl
+
+/-- Elements of the character space are non-unital algebra homomorphisms. -/
+instance : non_unital_alg_hom_class (character_space 𝕜 A) 𝕜 A 𝕜 :=
+{ map_smul := λ φ, map_smul φ,
+  map_zero := λ φ, map_zero φ,
+  map_mul := λ φ, φ.prop.2,
+  .. character_space.continuous_linear_map_class }
 
 /-- An element of the character space, as an non-unital algebra homomorphism. -/
-@[simps] def to_non_unital_alg_hom (φ : character_space 𝕜 A) : A →ₙₐ[𝕜] 𝕜 :=
+def to_non_unital_alg_hom (φ : character_space 𝕜 A) : A →ₙₐ[𝕜] 𝕜 :=
 { to_fun := (φ : A → 𝕜),
-  map_mul' := φ.prop.2,
-  map_smul' := (to_clm φ).map_smul,
-  map_zero' := continuous_linear_map.map_zero _,
-  map_add' := continuous_linear_map.map_add _ }
-
-lemma map_zero (φ : character_space 𝕜 A) : φ 0 = 0 := (to_non_unital_alg_hom φ).map_zero
-lemma map_add (φ : character_space 𝕜 A) (x y : A) : φ (x + y) = φ x + φ y :=
-  (to_non_unital_alg_hom φ).map_add _ _
-lemma map_smul (φ : character_space 𝕜 A) (r : 𝕜) (x : A) : φ (r • x) = r • (φ x) :=
-  (to_clm φ).map_smul _ _
-lemma map_mul (φ : character_space 𝕜 A) (x y : A) : φ (x * y) = φ x * φ y :=
-  (to_non_unital_alg_hom φ).map_mul _ _
-lemma continuous (φ : character_space 𝕜 A) : continuous φ := (to_clm φ).continuous
+  map_mul' := map_mul φ,
+  map_smul' := map_smul φ,
+  map_zero' := map_zero φ,
+  map_add' := map_add φ }
+
+@[simp]
+lemma coe_to_non_unital_alg_hom (φ : character_space 𝕜 A) : ⇑(to_non_unital_alg_hom φ) = φ := rfl
 
 end non_unital_non_assoc_semiring
 
@@ -81,32 +91,36 @@ section unital
 variables [comm_ring 𝕜] [no_zero_divisors 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜]
   [has_continuous_const_smul 𝕜 𝕜] [topological_space A] [semiring A] [algebra 𝕜 A]
 
-lemma map_one (φ : character_space 𝕜 A) : φ 1 = 1 :=
+/-- In a unital algebra, elements of the character space are algebra homomorphisms. -/
+instance : alg_hom_class (character_space 𝕜 A) 𝕜 A 𝕜 :=
+have map_one' : ∀ φ : character_space 𝕜 A, φ 1 = 1 := λ φ,
 begin
   have h₁ : (φ 1) * (1 - φ 1) = 0 := by rw [mul_sub, sub_eq_zero, mul_one, ←map_mul φ, one_mul],
-  rcases mul_eq_zero.mp h₁ with h₂|h₂,
-  { exfalso,
-    apply φ.prop.1,
-    ext,
-    rw [continuous_linear_map.zero_apply, ←one_mul x, coe_apply, map_mul φ, h₂, zero_mul] },
-  { rw [sub_eq_zero] at h₂,
-    exact h₂.symm },
-end
+  rcases mul_eq_zero.mp h₁ with h₂ | h₂,
+  { have : ∀ a, φ (a * 1) = 0 := λ a, by simp only [map_mul φ, h₂, mul_zero],
+    exact false.elim (φ.prop.1 $ continuous_linear_map.ext $ by simpa only [mul_one] using this) },
+  { exact (sub_eq_zero.mp h₂).symm },
+end,
+{ map_one := map_one',
+  commutes := λ φ r,
+  begin
+  { rw [algebra.algebra_map_eq_smul_one, algebra.id.map_eq_id, ring_hom.id_apply],
+    change ((φ : weak_dual 𝕜 A) : A →L[𝕜] 𝕜) (r • 1) = r,
+    rw [map_smul, algebra.id.smul_eq_mul, character_space.coe_coe, map_one' φ, mul_one] },
+  end,
+  .. character_space.non_unital_alg_hom_class }
 
-/-- An element of the character space, as an algebra homomorphism. -/
+/-- An element of the character space of a unital algebra, as an algebra homomorphism. -/
 @[simps] def to_alg_hom (φ : character_space 𝕜 A) : A →ₐ[𝕜] 𝕜 :=
 { map_one' := map_one φ,
-  commutes' := λ r, by
-  { rw [algebra.algebra_map_eq_smul_one, algebra.id.map_eq_id, ring_hom.id_apply],
-    change ((φ : weak_dual 𝕜 A) : A →L[𝕜] 𝕜) (r • 1) = r,
-    rw [continuous_linear_map.map_smul, algebra.id.smul_eq_mul, coe_apply, map_one φ, mul_one] },
+  commutes' := alg_hom_class.commutes φ,
   ..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⟩⟩,
+  refine ⟨λ h, ⟨map_one (⟨x, h⟩ : character_space 𝕜 A), h.2⟩, λ h, ⟨_, h.2⟩⟩,
   rintro rfl,
   simpa using h.1,
 end