feat(algebra/{module/linear_map, algebra/basic}): Add `distrib_mul_ac…

…tion.to_linear_(map|equiv)` and `mul_semiring_action.to_alg_(hom|equiv)` (#8936)

This adds the following stronger versions of `distrib_mul_action.to_add_monoid_hom`:

* `distrib_mul_action.to_linear_map`
* `distrib_mul_action.to_linear_equiv`
* `mul_semiring_action.to_alg_hom`
* `mul_semiring_action.to_alg_equiv`

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/group.20acting.20on.20algebra/near/251372497)

src/algebra/algebra/basic.lean

@@ -1085,6 +1085,39 @@ end division_ring
 
 end alg_equiv
 
+namespace mul_semiring_action
+
+variables {M G : Type*} (R A : Type*) [comm_semiring R] [semiring A] [algebra R A]
+
+section
+variables [monoid M] [mul_semiring_action M A] [smul_comm_class M R A]
+
+/-- Each element of the monoid defines a algebra homomorphism.
+
+This is a stronger version of `mul_semiring_action.to_ring_hom` and
+`distrib_mul_action.to_linear_map`. -/
+@[simps]
+def to_alg_hom (m : M) : A →ₐ[R] A :=
+alg_hom.mk' (mul_semiring_action.to_ring_hom _ _ m) (smul_comm _)
+
+end
+
+section
+variables [group G] [mul_semiring_action G A] [smul_comm_class G R A]
+
+/-- Each element of the group defines a algebra equivalence.
+
+This is a stronger version of `mul_semiring_action.to_ring_equiv` and
+`distrib_mul_action.to_linear_equiv`. -/
+@[simps]
+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 }
+
+end
+
+end mul_semiring_action
+
 section nat
 
 variables {R : Type*} [semiring R]

src/algebra/group_ring_action.lean

@@ -51,12 +51,14 @@ mul_semiring_action.smul_mul g x y
 variables (M R)
 
 /-- Each element of the monoid defines a additive monoid homomorphism. -/
+@[simps]
 def distrib_mul_action.to_add_monoid_hom [distrib_mul_action M A] (x : M) : A →+ A :=
 { to_fun   := (•) x,
   map_zero' := smul_zero x,
   map_add' := smul_add x }
 
 /-- 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 G A x,
   .. mul_action.to_perm_hom G A x }
@@ -68,6 +70,7 @@ def distrib_mul_action.hom_add_monoid_hom [distrib_mul_action M A] : M →* add_
   map_mul' := λ x y, add_monoid_hom.ext $ λ z, mul_smul x y z }
 
 /-- 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 :=
 { map_one' := smul_one x,
   map_mul' := smul_mul' x,
@@ -78,7 +81,8 @@ theorem to_ring_hom_injective [mul_semiring_action M R] [has_faithful_scalar M R
 λ m₁ m₂ h, eq_of_smul_eq_smul $ λ r, ring_hom.ext_iff.1 h r
 
 /-- Each element of the group defines a semiring isomorphism. -/
-def mul_semiring_action.to_semiring_equiv [mul_semiring_action G R] (x : G) : R ≃+* R :=
+@[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,
   .. mul_semiring_action.to_ring_hom G R x }
 

src/algebra/module/linear_map.lean

@@ -662,3 +662,36 @@ by exact {
   ..g }
 
 end module
+
+namespace distrib_mul_action
+
+variables (R M) [semiring R] [add_comm_monoid M] [module R M]
+
+section
+variables [monoid S] [distrib_mul_action S M] [smul_comm_class S R M]
+
+/-- Each element of the monoid defines a linear map.
+
+This is a stronger version of `distrib_mul_action.to_add_monoid_hom`. -/
+@[simps]
+def to_linear_map (s : S) : M →ₗ[R] M :=
+{ to_fun := has_scalar.smul s,
+  map_add' := smul_add s,
+  map_smul' := λ a b, smul_comm _ _ _ }
+
+end
+
+section
+variables [group S] [distrib_mul_action S M] [smul_comm_class S R M]
+
+/-- Each element of the group defines a linear equivalence.
+
+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_linear_map R M s }
+
+end
+
+end distrib_mul_action