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 #
restrict_scalars R S M
: theS
-moduleM
viewed as anR
module whenS
is anR
-algebra. Note that by default we do not have amodule S (restrict_scalars R S M)
instance for the original action. This is available as a defrestrict_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.
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
:
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
- restrict_scalars R S M = M
Instances for restrict_scalars
- restrict_scalars.inhabited
- restrict_scalars.add_comm_monoid
- restrict_scalars.add_comm_group
- restrict_scalars.module
- restrict_scalars.is_scalar_tower
- restrict_scalars.op_module
- restrict_scalars.is_central_scalar
- restrict_scalars.semiring
- restrict_scalars.ring
- restrict_scalars.comm_semiring
- restrict_scalars.comm_ring
- restrict_scalars.algebra
- restrict_scalars.seminormed_add_comm_group
- restrict_scalars.normed_add_comm_group
- restrict_scalars.normed_space
- lie_algebra.restrict_scalars.restrict_scalars.lie_ring
- lie_algebra.restrict_scalars.lie_algebra
Equations
- restrict_scalars.inhabited R S M = I
Equations
- restrict_scalars.add_comm_monoid R S M = I
Equations
- restrict_scalars.add_comm_group R S M = I
We temporarily install an action of the original ring on restrict_sclars R S M
.
Equations
- restrict_scalars.module_orig R S M = I
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
- restrict_scalars.module R S M = module.comp_hom M (algebra_map R S)
This instance is only relevant when restrict_scalars.module_orig
is available as an 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
- restrict_scalars.op_module R S M = let _inst : module Sᵐᵒᵖ (restrict_scalars R S M) := _inst_5 in module.comp_hom M (⇑ring_hom.op (algebra_map R S))
The R
-algebra homomorphism from the original coefficient algebra S
to endomorphisms
of restrict_scalars R S M
.
Equations
- restrict_scalars.lsmul R S M = let _inst : module S (restrict_scalars R S M) := restrict_scalars.module_orig R S M in algebra.lsmul R (restrict_scalars R S M)
restrict_scalars.add_equiv
is the additive equivalence with the original module.
Equations
Equations
- restrict_scalars.semiring R S A = I
Equations
- restrict_scalars.ring R S A = I
Equations
- restrict_scalars.comm_semiring R S A = I
Equations
- restrict_scalars.comm_ring R S A = I
Tautological ring isomorphism restrict_scalars R S A ≃+* A
.
Equations
- restrict_scalars.ring_equiv R S A = ring_equiv.refl (restrict_scalars R S A)
R ⟶ S
induces S-Alg ⥤ R-Alg
Equations
- restrict_scalars.algebra R S A = {to_has_smul := {smul := has_smul.smul smul_zero_class.to_has_smul}, to_ring_hom := {to_fun := ((algebra_map S A).comp (algebra_map R S)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}