chore(field_theory/fixed): reuse existing mul_semiring_action.to_alg_hom by providing smul_comm_class (#8965)

This removes `fixed_points.to_alg_hom` as this is really just a bundled form of `mul_semiring_action.to_alg_hom` + `mul_semiring_action.to_alg_hom_injective`, once we provide the missing `smul_comm_class`.

Author: eric-wieser

src/algebra/algebra/basic.lean

@@ -1100,6 +1100,10 @@ This is a stronger version of `mul_semiring_action.to_ring_hom` and
 def to_alg_hom (m : M) : A →ₐ[R] A :=
 alg_hom.mk' (mul_semiring_action.to_ring_hom _ _ m) (smul_comm _)
 
+theorem to_alg_hom_injective [has_faithful_scalar M A] :
+  function.injective (mul_semiring_action.to_alg_hom R A : M → A →ₐ[R] A) :=
+λ m₁ m₂ h, eq_of_smul_eq_smul $ λ r, alg_hom.ext_iff.1 h r
+
 end
 
 section
@@ -1114,6 +1118,10 @@ def to_alg_equiv (g : G) : A ≃ₐ[R] A :=
 { .. mul_semiring_action.to_ring_equiv _ _ g,
   .. mul_semiring_action.to_alg_hom R A g }
 
+theorem to_alg_equiv_injective [has_faithful_scalar G A] :
+  function.injective (mul_semiring_action.to_alg_equiv R A : G → A ≃ₐ[R] A) :=
+λ m₁ m₂ h, eq_of_smul_eq_smul $ λ r, alg_equiv.ext_iff.1 h r
+
 end
 
 end mul_semiring_action

src/field_theory/fixed.lean

@@ -84,6 +84,11 @@ subfield.copy (⨅ (m : M), fixed_by.subfield F m) (fixed_points M F)
 instance : is_invariant_subfield M (fixed_points.subfield M F) :=
 { smul_mem := λ g x hx g', by rw [hx, hx] }
 
+instance : smul_comm_class M (fixed_points.subfield M F) F :=
+{ smul_comm := λ m f f', show m • (↑f * f') = f * (m • f'), by rw [smul_mul', f.prop m] }
+
+instance smul_comm_class' : smul_comm_class (fixed_points.subfield M F) M F :=
+smul_comm_class.symm _ _ _
 
 @[simp] theorem smul (m : M) (x : fixed_points.subfield M F) : m • x = x :=
 subtype.eq $ x.2 m
@@ -292,38 +297,27 @@ lemma finrank_alg_hom (K : Type u) (V : Type v)
 fintype_card_le_finrank_of_linear_independent $ linear_independent_to_linear_map K V V
 
 namespace fixed_points
-/-- Embedding produced from a faithful action. -/
-@[simps apply {fully_applied := ff}]
-def to_alg_hom (G : Type u) (F : Type v) [group G] [field F]
-  [mul_semiring_action G F] [has_faithful_scalar G F] : G ↪ (F →ₐ[fixed_points.subfield G F] F) :=
-{ to_fun := λ g, { commutes' := λ x, x.2 g,
-    .. mul_semiring_action.to_ring_hom G F g },
-  inj' := λ g₁ g₂ hg, to_ring_hom_injective G F $ ring_hom.ext $ λ x, alg_hom.ext_iff.1 hg x, }
-
-lemma to_alg_hom_apply_apply {G : Type u} {F : Type v} [group G] [field F]
-  [mul_semiring_action G F] [has_faithful_scalar G F] (g : G) (x : F) :
-  to_alg_hom G F g x = g • x :=
-rfl
 
 theorem finrank_eq_card (G : Type u) (F : Type v) [group G] [field F]
   [fintype G] [mul_semiring_action G F] [has_faithful_scalar G F] :
   finrank (fixed_points.subfield G F) F = fintype.card G :=
 le_antisymm (fixed_points.finrank_le_card G F) $
 calc  fintype.card G
     ≤ fintype.card (F →ₐ[fixed_points.subfield G F] F) :
-        fintype.card_le_of_injective _ (to_alg_hom G F).2
+        fintype.card_le_of_injective _ (mul_semiring_action.to_alg_hom_injective _ F)
 ... ≤ finrank F (F →ₗ[fixed_points.subfield G F] F) : finrank_alg_hom (fixed_points G F) F
 ... = finrank (fixed_points.subfield G F) F : finrank_linear_map' _ _ _
 
+/-- `mul_semiring_action.to_alg_hom` is bijective. -/
 theorem to_alg_hom_bijective (G : Type u) (F : Type v) [group G] [field F]
   [fintype G] [mul_semiring_action G F] [has_faithful_scalar G F] :
-  function.bijective (to_alg_hom G F) :=
+  function.bijective (mul_semiring_action.to_alg_hom _ _ : G → F →ₐ[subfield G F] F) :=
 begin
   rw fintype.bijective_iff_injective_and_card,
   split,
-  { exact (to_alg_hom G F).injective },
+  { exact mul_semiring_action.to_alg_hom_injective _ F },
   { apply le_antisymm,
-    { exact fintype.card_le_of_injective _ (to_alg_hom G F).injective },
+    { exact fintype.card_le_of_injective _ (mul_semiring_action.to_alg_hom_injective _ F) },
     { rw ← finrank_eq_card G F,
       exact has_le.le.trans_eq (finrank_alg_hom _ F) (finrank_linear_map' _ _ _) } },
 end
@@ -332,6 +326,6 @@ end
 def to_alg_hom_equiv (G : Type u) (F : Type v) [group G] [field F]
   [fintype G] [mul_semiring_action G F] [has_faithful_scalar G F] :
     G ≃ (F →ₐ[fixed_points.subfield G F] F) :=
-function.embedding.equiv_of_surjective (to_alg_hom G F) (to_alg_hom_bijective G F).2
+equiv.of_bijective _ (to_alg_hom_bijective G F)
 
 end fixed_points