# mathlibdocumentation

algebra.algebra.restrict_scalars

# The restrict_scalars type alias #

See the documentation attached to the restrict_scalars definition for advice on how and when to use this type alias. As described there, it is often a better choice to use the is_scalar_tower typeclass instead.

## Main definitions #

• restrict_scalars R S M: the S-module M viewed as an R module when S is an R-algebra. Note that by default we do not have a module S (restrict_scalars R S M) instance for the original action. This is available as a def restrict_scalars.module_orig if really needed.
• restrict_scalars.add_equiv : restrict_scalars R S M ≃+ M: the additive equivalence between the restricted and original space (in fact, they are definitionally equal, but sometimes it is helpful to avoid using this fact, to keep instances from leaking).
• restrict_scalars.ring_equiv : restrict_scalars R S A ≃+* A: the ring equivalence between the restricted and original space when the module is an algebra.

There are many similarly-named definitions elsewhere which do not refer to this type alias. These refer to restricting the scalar type in a bundled type, such as from A →ₗ[R] B to A →ₗ[S] B:

• linear_map.restrict_scalars
• linear_equiv.restrict_scalars
• alg_hom.restrict_scalars
• alg_equiv.restrict_scalars
• submodule.restrict_scalars
• subalgebra.restrict_scalars
@[nolint]
def restrict_scalars (R : Type u_1) (S : Type u_2) (M : Type u_3) :
Type u_3

If we put an R-algebra structure on a semiring S, we get a natural equivalence from the category of S-modules to the category of representations of the algebra S (over R). The type synonym restrict_scalars is essentially this equivalence.

Warning: use this type synonym judiciously! Consider an example where we want to construct an R-linear map from M to S, given:

variables (R S M : Type*)
variables [comm_semiring R] [semiring S] [algebra R S] [add_comm_monoid M] [module S M]


With the assumptions above we can't directly state our map as we have no module R M structure, but restrict_scalars permits it to be written as:

-- an R-module structure on M is provided by restrict_scalars which is compatible
example : restrict_scalars R S M →ₗ[R] S := sorry


However, it is usually better just to add this extra structure as an argument:

-- an R-module structure on M and proof of its compatibility is provided by the user
example [module R M] [is_scalar_tower R S M] : M →ₗ[R] S := sorry


The advantage of the second approach is that it defers the duty of providing the missing typeclasses [module R M] [is_scalar_tower R S M]. If some concrete M naturally carries these (as is often the case) then we have avoided restrict_scalars entirely. If not, we can pass restrict_scalars R S M later on instead of M.

Note that this means we almost always want to state definitions and lemmas in the language of is_scalar_tower rather than restrict_scalars.

An example of when one might want to use restrict_scalars would be if one has a vector space over a field of characteristic zero and wishes to make use of the ℚ-algebra structure.

Equations
• M = M
Instances for restrict_scalars
@[protected, instance]
def restrict_scalars.inhabited (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : inhabited M] :
Equations
• = I
@[protected, instance]
def restrict_scalars.add_comm_monoid (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : add_comm_monoid M] :
Equations
@[protected, instance]
def restrict_scalars.add_comm_group (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : add_comm_group M] :
Equations
def restrict_scalars.module_orig (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [I : M] :
S M)

We temporarily install an action of the original ring on restrict_sclars R S M.

Equations
@[protected, instance]
def restrict_scalars.module (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [ S] [ M] :
S M)

When M is a module over a ring S, and S is an algebra over R, then M inherits a module structure over R.

The preferred way of setting this up is [module R M] [module S M] [is_scalar_tower R S M].

Equations
• = S)
@[protected, instance]
def restrict_scalars.is_scalar_tower (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [ S] [ M] :
S M)

This instance is only relevant when restrict_scalars.module_orig is available as an instance.

@[protected, instance]
def restrict_scalars.op_module (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [ S] [ M] :
S M)

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].

Equations
@[protected, instance]
def restrict_scalars.is_central_scalar (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [ S] [ M] [ M] [ M] :
S M)
def restrict_scalars.lsmul (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [ S] [ M] :
S →ₐ[R] S M)

The R-algebra homomorphism from the original coefficient algebra S to endomorphisms of restrict_scalars R S M.

Equations
• = let _inst : S M) := in S M)
@[simp]
theorem restrict_scalars.add_equiv_symm_apply (R : Type u_1) (S : Type u_2) (M : Type u_3) (ᾰ : M) :
M).symm) =
@[simp]
theorem restrict_scalars.add_equiv_apply (R : Type u_1) (S : Type u_2) (M : Type u_3) (ᾰ : M) :
M) =
def restrict_scalars.add_equiv (R : Type u_1) (S : Type u_2) (M : Type u_3)  :
M ≃+ M

restrict_scalars.add_equiv is the additive equivalence with the original module.

Equations
theorem restrict_scalars_smul_def (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [ S] [ M] (c : R) (x : M) :
c x = S) c x
@[simp]
theorem restrict_scalars.add_equiv_map_smul (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [ S] [ M] (t : R) (x : M) :
M) (t x) = S) t M) x
@[protected, instance]
def restrict_scalars.semiring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : semiring A] :
Equations
• = I
@[protected, instance]
def restrict_scalars.ring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : ring A] :
ring S A)
Equations
• = I
@[protected, instance]
def restrict_scalars.comm_semiring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : comm_semiring A] :
Equations
@[protected, instance]
def restrict_scalars.comm_ring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : comm_ring A] :
Equations
• = I
def restrict_scalars.ring_equiv (R : Type u_1) (S : Type u_2) (A : Type u_4) [semiring A] :
A ≃+* A

Tautological ring isomorphism restrict_scalars R S A ≃+* A.

Equations
@[simp]
theorem restrict_scalars.ring_equiv_map_smul (R : Type u_1) (S : Type u_2) (A : Type u_4) [semiring A] [ A] [ S] (r : R) (x : A) :
A) (r x) = S) r A) x
@[protected, instance]
def restrict_scalars.algebra (R : Type u_1) (S : Type u_2) (A : Type u_4) [semiring A] [ A] [ S] :
S A)

R ⟶ S induces S-Alg ⥤ R-Alg

Equations
@[simp]
theorem restrict_scalars.ring_equiv_algebra_map (R : Type u_1) (S : Type u_2) (A : Type u_4) [semiring A] [ A] [ S] (r : R) :
A) ( S A)) r) = A) ( S) r)