# 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.
• restrict_scalars.linear_equiv : restrict_scalars R S M ≃ₗ[S] M: the equivalence as an S-module between the restricted and origianl space.
• restrict_scalars.alg_equiv : restrict_scalars R S A ≃ₐ[S] A: the equivalence as an S-algebra between the restricted and original space.

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
@[instance]
def restrict_scalars.inhabited (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : inhabited M] :
Equations
• = I
@[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
@[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
@[instance]
def restrict_scalars.module_orig (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [I : M] :
S M)
Equations
def restrict_scalars.linear_equiv (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [ M] :
M ≃ₗ[S] M

restrict_scalars.linear_equiv is an equivalence of modules over the semiring S.

Equations
@[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)
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.linear_equiv_map_smul (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [ S] [ M] (t : R) (x : M) :
(t x) = S) t x
@[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)
@[instance]
def restrict_scalars.semiring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : semiring A] :
Equations
• = I
@[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
@[instance]
def restrict_scalars.comm_semiring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : comm_semiring A] :
Equations
@[instance]
def restrict_scalars.comm_ring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : comm_ring A] :
Equations
• = I
@[instance]
def restrict_scalars.algebra_orig (R : Type u_1) (S : Type u_2) (A : Type u_4) [semiring A] [I : A] :
S A)
Equations
def restrict_scalars.alg_equiv (R : Type u_1) (S : Type u_2) (A : Type u_4) [semiring A] [ A] :
A ≃ₐ[S] A

Tautological S-algebra isomorphism restrict_scalars R S A ≃ₐ[S] A.

Equations
@[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