The RestrictScalars type alias

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

Main definitions

• RestrictScalars 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 (RestrictScalars R S M) instance for the original action. This is available as a def RestrictScalars.moduleOrig if really needed.
• RestrictScalars.addEquiv : RestrictScalars 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).
• RestrictScalars.ringEquiv : RestrictScalars R S A ≃+* A: the ring equivalence between the restricted and original space when the module is an algebra.

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:

• LinearMap.restrictScalars
• LinearEquiv.restrictScalars
• AlgHom.restrictScalars
• AlgEquiv.restrictScalars
• Submodule.restrictScalars
• Subalgebra.restrictScalars

def RestrictScalars (_R : Type u_5) (_S : Type u_6) (M : Type u_7) : Type u_7

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 RestrictScalars 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:

variable (R S M : Type*)
variable [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module S M]

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

-- an `R`-module structure on `M` is provided by `RestrictScalars` which is compatible
example : RestrictScalars 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] [IsScalarTower 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] [IsScalarTower R S M]. If some concrete M naturally carries these (as is often the case) then we have avoided RestrictScalars entirely. If not, we can pass RestrictScalars 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 IsScalarTower rather than RestrictScalars.

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

Equations

• RestrictScalars _R _S M = M

instance instInhabitedRestrictScalars (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : Inhabited M] : Inhabited (RestrictScalars R S M)

Equations

• instInhabitedRestrictScalars R S M = I

instance instAddCommMonoidRestrictScalars (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : AddCommMonoid M] : AddCommMonoid (RestrictScalars R S M)

Equations

• instAddCommMonoidRestrictScalars R S M = I

instance instAddCommGroupRestrictScalars (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : AddCommGroup M] : AddCommGroup (RestrictScalars R S M)

Equations

• instAddCommGroupRestrictScalars R S M = I

def RestrictScalars.moduleOrig (R : Type u_1) (S : Type u_2) (M : Type u_3) [Semiring S] [AddCommMonoid M] [I : Module S M] : Module S (RestrictScalars R S M)

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

Equations

• RestrictScalars.moduleOrig R S M = I

instance RestrictScalars.module (R : Type u_1) (S : Type u_2) (M : Type u_3) [Semiring S] [AddCommMonoid M] [CommSemiring R] [Algebra R S] [Module S M] : Module R (RestrictScalars R 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] [IsScalarTower R S M].

Equations

• RestrictScalars.module R S M = Module.compHom M (algebraMap R S)

instance RestrictScalars.isScalarTower (R : Type u_1) (S : Type u_2) (M : Type u_3) [Semiring S] [AddCommMonoid M] [CommSemiring R] [Algebra R S] [Module S M] : IsScalarTower R S (RestrictScalars R S M)

This instance is only relevant when RestrictScalars.moduleOrig is available as an instance.

Equations

• ⋯ = ⋯

instance RestrictScalars.opModule (R : Type u_1) (S : Type u_2) (M : Type u_3) [Semiring S] [AddCommMonoid M] [CommSemiring R] [Algebra R S] [Module Sᵐᵒᵖ M] : Module Rᵐᵒᵖ (RestrictScalars R 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] [IsScalarTower Rᵐᵒᵖ Sᵐᵒᵖ M].

Equations

• RestrictScalars.opModule R S M = Module.compHom M (RingHom.op (algebraMap R S))

instance RestrictScalars.isCentralScalar (R : Type u_1) (S : Type u_2) (M : Type u_3) [Semiring S] [AddCommMonoid M] [CommSemiring R] [Algebra R S] [Module S M] [Module Sᵐᵒᵖ M] [IsCentralScalar S M] : IsCentralScalar R (RestrictScalars R S M)

Equations

• ⋯ = ⋯

def RestrictScalars.lsmul (R : Type u_1) (S : Type u_2) (M : Type u_3) [Semiring S] [AddCommMonoid M] [CommSemiring R] [Algebra R S] [Module S M] : S →ₐ[R] Module.End R (RestrictScalars R S M)

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

Equations

• RestrictScalars.lsmul R S M = Algebra.lsmul R R (RestrictScalars R S M)

def RestrictScalars.addEquiv (R : Type u_1) (S : Type u_2) (M : Type u_3) [AddCommMonoid M] : RestrictScalars R S M ≃+ M

RestrictScalars.addEquiv is the additive equivalence with the original module.

Equations

• RestrictScalars.addEquiv R S M = AddEquiv.refl M

theorem RestrictScalars.smul_def (R : Type u_1) (S : Type u_2) (M : Type u_3) [AddCommMonoid M] [CommSemiring R] [Semiring S] [Algebra R S] [Module S M] (c : R) (x : RestrictScalars R S M) : c • x = (AddEquiv.symm (RestrictScalars.addEquiv R S M)) ((algebraMap R S) c • (RestrictScalars.addEquiv R S M) x)

@[simp]

theorem RestrictScalars.addEquiv_map_smul (R : Type u_1) (S : Type u_2) (M : Type u_3) [AddCommMonoid M] [CommSemiring R] [Semiring S] [Algebra R S] [Module S M] (c : R) (x : RestrictScalars R S M) : (RestrictScalars.addEquiv R S M) (c • x) = (algebraMap R S) c • (RestrictScalars.addEquiv R S M) x

theorem RestrictScalars.addEquiv_symm_map_algebraMap_smul (R : Type u_1) (S : Type u_2) (M : Type u_3) [AddCommMonoid M] [CommSemiring R] [Semiring S] [Algebra R S] [Module S M] (r : R) (x : M) : (AddEquiv.symm (RestrictScalars.addEquiv R S M)) ((algebraMap R S) r • x) = r • (AddEquiv.symm (RestrictScalars.addEquiv R S M)) x

theorem RestrictScalars.addEquiv_symm_map_smul_smul (R : Type u_1) (S : Type u_2) (M : Type u_3) [AddCommMonoid M] [CommSemiring R] [Semiring S] [Algebra R S] [Module S M] (r : R) (s : S) (x : M) : (AddEquiv.symm (RestrictScalars.addEquiv R S M)) ((r • s) • x) = r • (AddEquiv.symm (RestrictScalars.addEquiv R S M)) (s • x)

theorem RestrictScalars.lsmul_apply_apply (R : Type u_1) (S : Type u_2) (M : Type u_3) [AddCommMonoid M] [CommSemiring R] [Semiring S] [Algebra R S] [Module S M] (s : S) (x : RestrictScalars R S M) : ((RestrictScalars.lsmul R S M) s) x = (AddEquiv.symm (RestrictScalars.addEquiv R S M)) (s • (RestrictScalars.addEquiv R S M) x)

instance instSemiringRestrictScalars (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : Semiring A] : Semiring (RestrictScalars R S A)

Equations

• instSemiringRestrictScalars R S A = I

instance instRingRestrictScalars (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : Ring A] : Ring (RestrictScalars R S A)

Equations

• instRingRestrictScalars R S A = I

instance instCommSemiringRestrictScalars (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : CommSemiring A] : CommSemiring (RestrictScalars R S A)

Equations

• instCommSemiringRestrictScalars R S A = I

instance instCommRingRestrictScalars (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : CommRing A] : CommRing (RestrictScalars R S A)

Equations

• instCommRingRestrictScalars R S A = I

def RestrictScalars.ringEquiv (R : Type u_1) (S : Type u_2) (A : Type u_4) [Semiring A] : RestrictScalars R S A ≃+* A

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

Equations

• RestrictScalars.ringEquiv R S A = RingEquiv.refl (RestrictScalars R S A)

@[simp]

theorem RestrictScalars.ringEquiv_map_smul (R : Type u_1) (S : Type u_2) (A : Type u_4) [Semiring A] [CommSemiring S] [Algebra S A] [CommSemiring R] [Algebra R S] (r : R) (x : RestrictScalars R S A) : (RestrictScalars.ringEquiv R S A) (r • x) = (algebraMap R S) r • (RestrictScalars.ringEquiv R S A) x

instance RestrictScalars.algebra (R : Type u_1) (S : Type u_2) (A : Type u_4) [Semiring A] [CommSemiring S] [Algebra S A] [CommSemiring R] [Algebra R S] : Algebra R (RestrictScalars R S A)

R ⟶ S induces S-Alg ⥤ R-Alg

Equations

• RestrictScalars.algebra R S A = let __src := RingHom.comp (algebraMap S A) (algebraMap R S); Algebra.mk __src ⋯ ⋯

@[simp]

theorem RestrictScalars.ringEquiv_algebraMap (R : Type u_1) (S : Type u_2) (A : Type u_4) [Semiring A] [CommSemiring S] [Algebra S A] [CommSemiring R] [Algebra R S] (r : R) : (RestrictScalars.ringEquiv R S A) ((algebraMap R (RestrictScalars R S A)) r) = (algebraMap S A) ((algebraMap R S) r)