mathlib3 documentation

algebra.algebra.restrict_scalars

The restrict_scalars type alias #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
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
@[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] [add_comm_monoid M] [I : module 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] [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
@[protected, 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] :

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

@[protected, instance]

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.lsmul (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] :

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

Equations
def restrict_scalars.add_equiv (R : Type u_1) (S : Type u_2) (M : Type u_3) [add_comm_monoid M] :

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

Equations
@[simp]
theorem restrict_scalars.add_equiv_map_smul (R : Type u_1) (S : Type u_2) (M : Type u_3) [add_comm_monoid M] [comm_semiring R] [semiring S] [algebra R S] [module S M] (c : R) (x : restrict_scalars R S M) :
theorem restrict_scalars.smul_def (R : Type u_1) (S : Type u_2) (M : Type u_3) [add_comm_monoid M] [comm_semiring R] [semiring S] [algebra R S] [module S M] (c : R) (x : restrict_scalars R S M) :
theorem restrict_scalars.add_equiv_symm_map_smul_smul (R : Type u_1) (S : Type u_2) (M : Type u_3) [add_comm_monoid M] [comm_semiring R] [semiring S] [algebra R S] [module S M] (r : R) (s : S) (x : M) :
theorem restrict_scalars.lsmul_apply_apply (R : Type u_1) (S : Type u_2) (M : Type u_3) [add_comm_monoid M] [comm_semiring R] [semiring S] [algebra R S] [module S M] (s : S) (x : restrict_scalars R S M) :
@[protected, instance]
def restrict_scalars.semiring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : semiring A] :
Equations
@[protected, instance]
def restrict_scalars.ring (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : ring A] :
Equations
@[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
def restrict_scalars.ring_equiv (R : Type u_1) (S : Type u_2) (A : Type u_4) [semiring 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] [comm_semiring S] [algebra S A] [comm_semiring R] [algebra R S] (r : R) (x : restrict_scalars R S A) :
@[protected, instance]
def restrict_scalars.algebra (R : Type u_1) (S : Type u_2) (A : Type u_4) [semiring A] [comm_semiring S] [algebra S A] [comm_semiring R] [algebra R S] :

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] [comm_semiring S] [algebra S A] [comm_semiring R] [algebra R S] (r : R) :