feat(group_theory/group_action): add distrib_mul_action.to_add_aut and mul_distrib_mul_action.to_mul_aut (#9224)

These can be used to golf the existing `mul_aut_arrow`.

This also moves some definitions out of `algebra/group_ring_action.lean` into a more appropriate file.

Author: eric-wieser

src/algebra/group_ring_action.lean

@@ -50,18 +50,6 @@ instance mul_semiring_action.to_mul_distrib_mul_action [h : mul_semiring_action
   mul_distrib_mul_action M R :=
 { ..h }
 
-/-- Each element of the group defines an additive monoid isomorphism. -/
-@[simps]
-def distrib_mul_action.to_add_equiv [distrib_mul_action G A] (x : G) : A ≃+ A :=
-{ .. distrib_mul_action.to_add_monoid_hom A x,
-  .. mul_action.to_perm_hom G A x }
-
-/-- Each element of the group defines a multiplicative monoid isomorphism. -/
-@[simps]
-def mul_distrib_mul_action.to_mul_equiv [mul_distrib_mul_action G M] (x : G) : M ≃* M :=
-{ .. mul_distrib_mul_action.to_monoid_hom M x,
-  .. mul_action.to_perm_hom G M x }
-
 /-- Each element of the monoid defines a semiring homomorphism. -/
 @[simps]
 def mul_semiring_action.to_ring_hom [mul_semiring_action M R] (x : M) : R →+* R :=
@@ -75,7 +63,7 @@ theorem to_ring_hom_injective [mul_semiring_action M R] [has_faithful_scalar M R
 /-- Each element of the group defines a semiring isomorphism. -/
 @[simps]
 def mul_semiring_action.to_ring_equiv [mul_semiring_action G R] (x : G) : R ≃+* R :=
-{ .. distrib_mul_action.to_add_equiv G R x,
+{ .. distrib_mul_action.to_add_equiv R x,
   .. mul_semiring_action.to_ring_hom G R x }
 
 section

src/algebra/module/linear_map.lean

@@ -693,7 +693,7 @@ variables [group S] [distrib_mul_action S M] [smul_comm_class S R M]
 This is a stronger version of `distrib_mul_action.to_add_equiv`. -/
 @[simps]
 def to_linear_equiv (s : S) : M ≃ₗ[R] M :=
-{ ..to_add_equiv _ _ s,
+{ ..to_add_equiv M s,
   ..to_linear_map R M s }
 
 end

src/group_theory/group_action/group.lean

@@ -47,13 +47,15 @@ add_decl_doc add_action.to_perm
 variables (α) (β)
 
 /-- Given an action of a group `α` on a set `β`, each `g : α` defines a permutation of `β`. -/
+@[simps]
 def mul_action.to_perm_hom : α →* equiv.perm β :=
 { to_fun := mul_action.to_perm,
   map_one' := equiv.ext $ one_smul α,
   map_mul' := λ u₁ u₂, equiv.ext $ mul_smul (u₁:α) u₂ }
 
 /-- Given an action of a additive group `α` on a set `β`, each `g : α` defines a permutation of
 `β`. -/
+@[simps]
 def add_action.to_perm_hom (α : Type*) [add_group α] [add_action α β] :
   α →+ additive (equiv.perm β) :=
 { to_fun := λ a, additive.of_mul $ add_action.to_perm a,
@@ -136,6 +138,29 @@ section distrib_mul_action
 section group
 variables [group α] [add_monoid β] [distrib_mul_action α β]
 
+variables (β)
+
+/-- Each element of the group defines an additive monoid isomorphism.
+
+This is a stronger version of `mul_action.to_perm`. -/
+@[simps {simp_rhs := tt}]
+def distrib_mul_action.to_add_equiv (x : α) : β ≃+ β :=
+{ .. distrib_mul_action.to_add_monoid_hom β x,
+  .. mul_action.to_perm_hom α β x }
+
+variables (α β)
+
+/-- Each element of the group defines an additive monoid isomorphism.
+
+This is a stronger version of `mul_action.to_perm_hom`. -/
+@[simps]
+def distrib_mul_action.to_add_aut : α →* add_aut β :=
+{ to_fun := distrib_mul_action.to_add_equiv β,
+  map_one' := add_equiv.ext (one_smul _),
+  map_mul' := λ a₁ a₂, add_equiv.ext (mul_smul _ _) }
+
+variables {α β}
+
 theorem smul_eq_zero_iff_eq (a : α) {x : β} : a • x = 0 ↔ x = 0 :=
 ⟨λ h, by rw [← inv_smul_smul a x, h, smul_zero], λ h, h.symm ▸ smul_zero _⟩
 
@@ -157,6 +182,34 @@ end gwz
 
 end distrib_mul_action
 
+section mul_distrib_mul_action
+variables [group α] [monoid β] [mul_distrib_mul_action α β]
+
+variables (β)
+
+/-- Each element of the group defines a multiplicative monoid isomorphism.
+
+This is a stronger version of `mul_action.to_perm`. -/
+@[simps {simp_rhs := tt}]
+def mul_distrib_mul_action.to_mul_equiv (x : α) : β ≃* β :=
+{ .. mul_distrib_mul_action.to_monoid_hom β x,
+  .. mul_action.to_perm_hom α β x }
+
+variables (α β)
+
+/-- Each element of the group defines an multiplicative monoid isomorphism.
+
+This is a stronger version of `mul_action.to_perm_hom`. -/
+@[simps]
+def mul_distrib_mul_action.to_mul_aut : α →* mul_aut β :=
+{ to_fun := mul_distrib_mul_action.to_mul_equiv β,
+  map_one' := mul_equiv.ext (one_smul _),
+  map_mul' := λ a₁ a₂, mul_equiv.ext (mul_smul _ _) }
+
+variables {α β}
+
+end mul_distrib_mul_action
+
 section arrow
 
 /-- If `G` acts on `A`, then it acts also on `A → B`, by `(g • F) a = F (g⁻¹ • a)`. -/
@@ -167,17 +220,18 @@ section arrow
 
 local attribute [instance] arrow_action
 
+/-- When `B` is a monoid, `arrow_action` is additionally a `mul_distrib_mul_action`. -/
+def arrow_mul_distrib_mul_action {G A B : Type*} [group G] [mul_action G A] [monoid B] :
+  mul_distrib_mul_action G (A → B) :=
+{ smul_one := λ g, rfl,
+  smul_mul := λ g f₁ f₂, rfl }
+
+local attribute [instance] arrow_mul_distrib_mul_action
+
 /-- Given groups `G H` with `G` acting on `A`, `G` acts by
   multiplicative automorphisms on `A → H`. -/
-@[simps] def mul_aut_arrow {G A H} [group G] [mul_action G A] [group H] : G →* mul_aut (A → H) :=
-{ to_fun := λ g,
-  { to_fun := λ F, g • F,
-    inv_fun := λ F, g⁻¹ • F,
-    left_inv := λ F, inv_smul_smul g F,
-    right_inv := λ F, smul_inv_smul g F,
-    map_mul' := by { intros, ext, simp only [arrow_action_to_has_scalar_smul, pi.mul_apply] } },
-  map_one' := by { ext, simp only [mul_aut.one_apply, mul_equiv.coe_mk, one_smul] },
-  map_mul' := by { intros, ext, simp only [mul_smul, mul_equiv.coe_mk, mul_aut.mul_apply] } }
+@[simps] def mul_aut_arrow {G A H} [group G] [mul_action G A] [monoid H] : G →* mul_aut (A → H) :=
+mul_distrib_mul_action.to_mul_aut _ _
 
 end arrow