feat(group_theory/group_action): generalize mul_action.function_End to other endomorphisms (#8724)

The main aim of this PR is to remove [`intermediate_field.subgroup_action`](https://leanprover-community.github.io/mathlib_docs/field_theory/galois.html#intermediate_field.subgroup_action) which is a weird special case of the much more general instance `f • a = f a`, added in this PR as `alg_equiv.apply_mul_semiring_action`. We add the same actions for all the other hom types for consistency.

These generalizations are in line with the `mul_action.function_End` (renamed to `function.End.apply_mul_action`) and `mul_action.perm` (renamed to `equiv.perm.apply_mul_action`) instances introduced by @dwarn, providing any endomorphism that has a monoid structure with a faithful `mul_action` corresponding to function application.
Note that there is no monoid structure on `ring_equiv`, or `alg_hom`, so this PR does not bother with the corresponding action.

Author: eric-wieser

src/algebra/algebra/basic.lean

@@ -1008,6 +1008,29 @@ by { ext, refl }
 @[simp] lemma aut_congr_trans (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) :
   (aut_congr ϕ).trans (aut_congr ψ) = aut_congr (ϕ.trans ψ) := rfl
 
+/-- The tautological action by `A₁ ≃ₐ[R] A₁` on `A₁`.
+
+This generalizes `function.End.apply_mul_action`. -/
+instance apply_mul_semiring_action : mul_semiring_action (A₁ ≃ₐ[R] A₁) A₁ :=
+{ smul := ($),
+  smul_zero := alg_equiv.map_zero,
+  smul_add := alg_equiv.map_add,
+  smul_one := alg_equiv.map_one,
+  smul_mul := alg_equiv.map_mul,
+  one_smul := λ _, rfl,
+  mul_smul := λ _ _ _, rfl }
+
+@[simp] protected lemma smul_def (f : A₁ ≃ₐ[R] A₁) (a : A₁) : f • a = f a := rfl
+
+instance apply_has_faithful_scalar : has_faithful_scalar (A₁ ≃ₐ[R] A₁) A₁ :=
+⟨λ _ _, alg_equiv.ext⟩
+
+instance apply_smul_comm_class : smul_comm_class R (A₁ ≃ₐ[R] A₁) A₁ :=
+{ smul_comm := λ r e a, (e.to_linear_equiv.map_smul r a).symm }
+
+instance apply_smul_comm_class' : smul_comm_class (A₁ ≃ₐ[R] A₁) R A₁ :=
+{ smul_comm := λ e r a, (e.to_linear_equiv.map_smul r a) }
+
 end semiring
 
 section comm_semiring

src/algebra/module/basic.lean

@@ -251,6 +251,23 @@ instance semiring.to_opposite_module [semiring R] : module Rᵒᵖ R :=
 def ring_hom.to_module [semiring R] [semiring S] (f : R →+* S) : module R S :=
 module.comp_hom S f
 
+/-- The tautological action by `R →+* R` on `R`.
+
+This generalizes `function.End.apply_mul_action`. -/
+instance ring_hom.apply_distrib_mul_action [semiring R] : distrib_mul_action (R →+* R) R :=
+{ smul := ($),
+  smul_zero := ring_hom.map_zero,
+  smul_add := ring_hom.map_add,
+  one_smul := λ _, rfl,
+  mul_smul := λ _ _ _, rfl }
+
+@[simp] protected lemma ring_hom.smul_def [semiring R] (f : R →+* R) (a : R) :
+  f • a = f a := rfl
+
+/-- `ring_hom.apply_distrib_mul_action` is faithful. -/
+instance ring_hom.apply_has_faithful_scalar [semiring R] : has_faithful_scalar (R →+* R) R :=
+⟨ring_hom.ext⟩
+
 section add_comm_monoid
 
 variables [semiring R] [add_comm_monoid M] [module R M]

src/data/equiv/mul_add_aut.lean

@@ -72,6 +72,23 @@ mul_equiv.apply_symm_apply _ _
 def to_perm : mul_aut M →* equiv.perm M :=
 by refine_struct { to_fun := mul_equiv.to_equiv }; intros; refl
 
+/-- The tautological action by `mul_aut M` on `M`.
+
+Note this also satisfies the axioms of `mul_semiring_action` that aren't inherited from
+`distrib_mul_action`.
+
+This generalizes `function.End.apply_mul_action`. -/
+instance apply_mul_action {M} [monoid M] : mul_action (mul_aut M) M :=
+{ smul := ($),
+  one_smul := λ _, rfl,
+  mul_smul := λ _ _ _, rfl }
+
+@[simp] protected lemma smul_def {M} [monoid M] (f : mul_aut M) (a : M) : f • a = f a := rfl
+
+/-- `mul_aut.apply_mul_action` is faithful. -/
+instance apply_has_faithful_scalar {M} [monoid M] : has_faithful_scalar (mul_aut M) M :=
+⟨λ _ _, mul_equiv.ext⟩
+
 /-- Group conjugation, `mul_aut.conj g h = g * h * g⁻¹`, as a monoid homomorphism
 mapping multiplication in `G` into multiplication in the automorphism group `mul_aut G`. -/
 def conj [group G] : G →* mul_aut G :=
@@ -130,6 +147,22 @@ add_equiv.apply_symm_apply _ _
 def to_perm : add_aut A →* equiv.perm A :=
 by refine_struct { to_fun := add_equiv.to_equiv }; intros; refl
 
+/-- The tautological action by `add_aut A` on `A`.
+
+This generalizes `function.End.apply_mul_action`. -/
+instance apply_distrib_mul_action {A} [add_monoid A] : distrib_mul_action (add_aut A) A :=
+{ smul := ($),
+  smul_zero := add_equiv.map_zero,
+  smul_add := add_equiv.map_add,
+  one_smul := λ _, rfl,
+  mul_smul := λ _ _ _, rfl }
+
+@[simp] protected lemma smul_def {A} [add_monoid A] (f : add_aut A) (a : A) : f • a = f a := rfl
+
+/-- `add_aut.apply_distrib_mul_action` is faithful. -/
+instance apply_has_faithful_scalar {A} [add_monoid A] : has_faithful_scalar (add_aut A) A :=
+⟨λ _ _, add_equiv.ext⟩
+
 /-- Additive group conjugation, `add_aut.conj g h = g + h - g`, as an additive monoid
 homomorphism mapping addition in `G` into multiplication in the automorphism group `add_aut G`
 (written additively in order to define the map). -/

src/field_theory/galois.lean

@@ -162,18 +162,6 @@ variables (H : subgroup (E ≃ₐ[F] E)) (K : intermediate_field F E)
 
 namespace intermediate_field
 
-instance subgroup_action : mul_semiring_action H E :=
-{ smul := λ h x, h x,
-  smul_zero := λ _, map_zero _,
-  smul_add := λ _, map_add _,
-  one_smul := λ _, rfl,
-  smul_one := λ _, map_one _,
-  mul_smul := λ _ _ _, rfl,
-  smul_mul := λ _, map_mul _ }
-
-instance : has_faithful_scalar H E :=
-{ eq_of_smul_eq_smul := λ x y z, subtype.ext (alg_equiv.ext z) }
-
 /-- The intermediate_field fixed by a subgroup -/
 def fixed_field : intermediate_field F E :=
 { carrier := mul_action.fixed_points H E,

src/group_theory/group_action/defs.lean

@@ -424,14 +424,48 @@ instance : inhabited (function.End α) := ⟨1⟩
 
 variable {α}
 
-/-- The tautological action by `function.End α` on `α`. -/
-instance mul_action.function_End : mul_action (function.End α) α :=
+/-- The tautological action by `function.End α` on `α`.
+
+This is generalized to bundled endomorphisms by:
+* `equiv.perm.apply_mul_action`
+* `add_monoid.End.apply_distrib_mul_action`
+* `add_aut.apply_distrib_mul_action`
+* `ring_hom.apply_distrib_mul_action`
+* `linear_equiv.apply_distrib_mul_action`
+* `linear_map.apply_module`
+* `ring_hom.apply_mul_semiring_action`
+* `alg_equiv.apply_mul_semiring_action`
+-/
+instance function.End.apply_mul_action : mul_action (function.End α) α :=
 { smul := ($),
   one_smul := λ _, rfl,
   mul_smul := λ _ _ _, rfl }
 
 @[simp] lemma function.End.smul_def (f : function.End α) (a : α) : f • a = f a := rfl
 
+/-- `function.End.apply_mul_action` is faithful. -/
+instance function.End.apply_has_faithful_scalar : has_faithful_scalar (function.End α) α :=
+⟨λ x y, funext⟩
+
+/-- The tautological action by `add_monoid.End α` on `α`.
+
+This generalizes `function.End.apply_mul_action`. -/
+instance add_monoid.End.apply_distrib_mul_action [add_monoid α] :
+  distrib_mul_action (add_monoid.End α) α :=
+{ smul := ($),
+  smul_zero := add_monoid_hom.map_zero,
+  smul_add := add_monoid_hom.map_add,
+  one_smul := λ _, rfl,
+  mul_smul := λ _ _ _, rfl }
+
+@[simp] lemma add_monoid.End.smul_def [add_monoid α] (f : add_monoid.End α) (a : α) :
+  f • a = f a := rfl
+
+/-- `add_monoid.End.apply_distrib_mul_action` is faithful. -/
+instance add_monoid.End.apply_has_faithful_scalar [add_monoid α] :
+  has_faithful_scalar (add_monoid.End α) α :=
+⟨add_monoid_hom.ext⟩
+
 /-- The monoid hom representing a monoid action.
 
 When `M` is a group, see `mul_action.to_perm_hom`. -/

src/group_theory/group_action/group.lean

@@ -60,16 +60,19 @@ def add_action.to_perm_hom (α : Type*) [add_group α] [add_action α β] :
   map_zero' := equiv.ext $ zero_vadd α,
   map_add' := λ a₁ a₂, equiv.ext $ add_vadd a₁ a₂ }
 
-/-- The tautological action by `equiv.perm α` on `α`. -/
-instance mul_action.perm (α : Type*) : mul_action (equiv.perm α) α :=
+/-- The tautological action by `equiv.perm α` on `α`.
+
+This generalizes `function.End.apply_mul_action`.-/
+instance equiv.perm.apply_mul_action (α : Type*) : mul_action (equiv.perm α) α :=
 { smul := λ f a, f a,
   one_smul := λ _, rfl,
   mul_smul := λ _ _ _, rfl }
 
-@[simp] lemma equiv.perm.smul_def {α : Type*} (f : equiv.perm α) (a : α) : f • a = f a := rfl
+@[simp] protected lemma equiv.perm.smul_def {α : Type*} (f : equiv.perm α) (a : α) : f • a = f a :=
+rfl
 
-/-- `mul_action.perm` is faithful. -/
-instance equiv.perm.has_faithful_scalar (α : Type*) : has_faithful_scalar (equiv.perm α) α :=
+/-- `equiv.perm.apply_mul_action` is faithful. -/
+instance equiv.perm.apply_has_faithful_scalar (α : Type*) : has_faithful_scalar (equiv.perm α) α :=
 ⟨λ x y, equiv.ext⟩
 
 variables {α} {β}

src/linear_algebra/basic.lean

@@ -569,6 +569,30 @@ by refine_struct
     .. linear_map.add_comm_monoid, .. };
 intros; try { refl }; apply linear_map.ext; simp {proj := ff}
 
+/-- The tautological action by `M →ₗ[R] M` on `M`.
+
+This generalizes `function.End.apply_mul_action`. -/
+instance apply_module : module (M →ₗ[R] M) M :=
+{ smul := ($),
+  smul_zero := linear_map.map_zero,
+  smul_add := linear_map.map_add,
+  add_smul := linear_map.add_apply,
+  zero_smul := (linear_map.zero_apply : ∀ m, (0 : M →ₗ[R] M) m = 0),
+  one_smul := λ _, rfl,
+  mul_smul := λ _ _ _, rfl }
+
+@[simp] protected lemma smul_def (f : M →ₗ[R] M) (a : M) : f • a = f a := rfl
+
+/-- `linear_map.apply_module` is faithful. -/
+instance apply_has_faithful_scalar : has_faithful_scalar (M →ₗ[R] M) M :=
+⟨λ _ _, linear_map.ext⟩
+
+instance apply_smul_comm_class : smul_comm_class R (M →ₗ[R] M) M :=
+{ smul_comm := λ r e m, (e.map_smul r m).symm }
+
+instance apply_smul_comm_class' : smul_comm_class (M →ₗ[R] M) R M :=
+{ smul_comm := linear_map.map_smul }
+
 end semiring
 
 section ring
@@ -2866,6 +2890,29 @@ def automorphism_group.to_linear_map_monoid_hom :
   map_one' := rfl,
   map_mul' := λ _ _, rfl }
 
+/-- The tautological action by `M ≃ₗ[R] M` on `M`.
+
+This generalizes `function.End.apply_mul_action`. -/
+instance apply_distrib_mul_action : distrib_mul_action (M ≃ₗ[R] M) M :=
+{ smul := ($),
+  smul_zero := linear_equiv.map_zero,
+  smul_add := linear_equiv.map_add,
+  one_smul := λ _, rfl,
+  mul_smul := λ _ _ _, rfl }
+
+@[simp] protected lemma smul_def (f : M ≃ₗ[R] M) (a : M) :
+  f • a = f a := rfl
+
+/-- `linear_equiv.apply_distrib_mul_action` is faithful. -/
+instance apply_has_faithful_scalar : has_faithful_scalar (M ≃ₗ[R] M) M :=
+⟨λ _ _, linear_equiv.ext⟩
+
+instance apply_smul_comm_class : smul_comm_class R (M ≃ₗ[R] M) M :=
+{ smul_comm := λ r e m, (e.map_smul r m).symm }
+
+instance apply_smul_comm_class' : smul_comm_class (M ≃ₗ[R] M) R M :=
+{ smul_comm := linear_equiv.map_smul }
+
 end linear_equiv
 
 namespace linear_map

src/ring_theory/derivation.lean

@@ -24,7 +24,7 @@ non-commutative case. Any development on the theory of derivations is discourage
 definitive definition of derivation will be implemented.
 -/
 
-open algebra ring_hom
+open algebra
 
 -- to match `linear_map`
 set_option old_structure_cmd true
@@ -87,7 +87,8 @@ begin
 end
 
 @[simp] lemma map_algebra_map : D (algebra_map R A r) = 0 :=
-by rw [←mul_one r, ring_hom.map_mul, map_one, ←smul_def, map_smul, map_one_eq_zero, smul_zero]
+by rw [←mul_one r, ring_hom.map_mul, ring_hom.map_one, ←smul_def, map_smul, map_one_eq_zero,
+  smul_zero]
 
 /- Data typeclasses -/