Documentation

Mathlib.Algebra.Algebra.RestrictScalars

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 #

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:

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.

Instances For
    instance instInhabitedRestrictScalars (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : Inhabited M] :
    instance instAddCommMonoidRestrictScalars (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : AddCommMonoid M] :
    instance instAddCommGroupRestrictScalars (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : AddCommGroup M] :
    def RestrictScalars.moduleOrig (R : Type u_1) (S : Type u_2) (M : Type u_3) [Semiring S] [AddCommMonoid M] [I : Module S M] :

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

    Instances For
      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] :

      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].

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

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

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

      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].

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

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

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

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

        Instances For
          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) :
          @[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) :
          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) :
          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) :
          instance instSemiringRestrictScalars (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : Semiring A] :
          instance instRingRestrictScalars (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : Ring A] :
          instance instCommSemiringRestrictScalars (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : CommSemiring A] :
          instance instCommRingRestrictScalars (R : Type u_1) (S : Type u_2) (A : Type u_4) [I : CommRing A] :
          def RestrictScalars.ringEquiv (R : Type u_1) (S : Type u_2) (A : Type u_4) [Semiring A] :

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

          Instances For
            @[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

            R ⟶ S induces S-Alg ⥤ R-Alg

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