mathlib documentation

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 #

See also #

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:

@[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
@[instance]
def restrict_scalars.inhabited (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : inhabited M] :
Equations
@[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] [add_comm_monoid M] [I : module S M] :
Equations
def restrict_scalars.linear_equiv (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [add_comm_monoid M] [module 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] [add_comm_monoid M] [comm_semiring R] [algebra R S] [module 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
theorem restrict_scalars_smul_def (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [add_comm_monoid M] [comm_semiring R] [algebra R S] [module S M] (c : R) (x : restrict_scalars R S M) :
c x = (algebra_map R 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] [add_comm_monoid M] [comm_semiring R] [algebra R S] [module S M] (t : R) (x : restrict_scalars R S M) :
@[instance]
def restrict_scalars.is_scalar_tower (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring S] [add_comm_monoid M] [comm_semiring R] [algebra R S] [module S M] :
@[instance]
def restrict_scalars.semiring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : semiring A] :
Equations
@[instance]
def restrict_scalars.ring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : ring A] :
Equations
@[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
@[instance]
def restrict_scalars.algebra_orig (R : Type u_1) (S : Type u_2) (A : Type u_4) [comm_semiring S] [semiring A] [I : algebra S A] :
Equations
def restrict_scalars.alg_equiv (R : Type u_1) (S : Type u_2) (A : Type u_4) [comm_semiring S] [semiring A] [algebra 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) [comm_semiring S] [semiring A] [algebra S A] [comm_semiring R] [algebra R S] :

R ⟶ S induces S-Alg ⥤ R-Alg

Equations