chore(algebra/algebra/restrict_scalars): put a right action on restri…

…cted scalars (#13996)

This provides `module Rᵐᵒᵖ (restrict_scalars R S M)` in terms of a `module Sᵐᵒᵖ M` action, by sending `Rᵐᵒᵖ` to `Sᵐᵒᵖ` through `algebra_map R S`.

This means that `restrict_scalars R S M` now works for right-modules and bi-modules in addition to left-modules.

This will become important if we change `algebra R A` to require `A` to be an `R`-bimodule, as otherwise `restrict_scalars R S A` would no longer be an algebra.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2313996.20right.20actions.20on.20restrict_scalars/near/282045994)

src/algebra/algebra/restrict_scalars.lean

@@ -89,8 +89,7 @@ variables [semiring S] [add_comm_monoid M]
 def restrict_scalars.module_orig [I : module S M] :
   module S (restrict_scalars R S M) := I
 
-variables [comm_semiring R] [algebra R S] [module S M]
-
+variables [comm_semiring R] [algebra R S]
 section
 local attribute [instance] restrict_scalars.module_orig
 
@@ -100,22 +99,38 @@ module structure over `R`.
 
 The preferred way of setting this up is `[module R M] [module S M] [is_scalar_tower R S M]`.
 -/
-instance : module R (restrict_scalars R S M) :=
+instance [module S M] : module R (restrict_scalars R S M) :=
 module.comp_hom M (algebra_map R S)
 
 /--
 This instance is only relevant when `restrict_scalars.module_orig` is available as an instance.
 -/
-instance : is_scalar_tower R S (restrict_scalars R S M) :=
+instance [module S M] : is_scalar_tower R S (restrict_scalars R S M) :=
 ⟨λ r S M, by { rw [algebra.smul_def, mul_smul], refl }⟩
 
 end
 
+/--
+When `M` is a right-module over a ring `S`, and `S` is an algebra over `R`, then `M` inherits a
+right-module structure over `R`.
+The preferred way of setting this up is
+`[module Rᵐᵒᵖ M] [module Sᵐᵒᵖ M] [is_scalar_tower Rᵐᵒᵖ Sᵐᵒᵖ M]`.
+-/
+instance restrict_scalars.op_module [module Sᵐᵒᵖ M] : module Rᵐᵒᵖ (restrict_scalars R S M) :=
+begin
+  letI : module Sᵐᵒᵖ (restrict_scalars R S M) := ‹module Sᵐᵒᵖ M›,
+  exact module.comp_hom M (algebra_map R S).op
+end
+
+instance restrict_scalars.is_central_scalar [module S M] [module Sᵐᵒᵖ M] [is_central_scalar S M] :
+  is_central_scalar R (restrict_scalars R S M) :=
+{ op_smul_eq_smul := λ r x, (op_smul_eq_smul (algebra_map R S r) (_ : M) : _)}
+
 /--
 The `R`-algebra homomorphism from the original coefficient algebra `S` to endomorphisms
 of `restrict_scalars R S M`.
 -/
-def restrict_scalars.lsmul : S →ₐ[R] module.End R (restrict_scalars R S M) :=
+def restrict_scalars.lsmul [module S M] : S →ₐ[R] module.End R (restrict_scalars R S M) :=
 begin
   -- We use `restrict_scalars.module_orig` in the implementation,
   -- but not in the type.