Mathlib.Algebra.Algebra.RestrictScalars

Module docstring

{"# 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.

/-- 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:
```lean
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:
```lean
-- 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:
```lean
-- 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. -/
@[nolint unusedArguments]
def RestrictScalars (_R _S M : Type*) : Type _ := M

Restriction of scalars from $S$ to $R$ for module $M$

Informal description

Given a commutative semiring $R$, a semiring $S$ with an $R$-algebra structure, and an $S$-module $M$, the type synonym `RestrictScalars R S M` represents $M$ viewed as an $R$-module by restricting the scalar multiplication from $S$ to $R$ via the algebra map $R \to S$.

instInhabitedRestrictScalars instance

[I : Inhabited M] : Inhabited (RestrictScalars R S M)

Full source

instance [I : Inhabited M] : Inhabited (RestrictScalars R S M) := I

Inhabitedness of Restricted Scalar Modules

Informal description

For any inhabited $S$-module $M$, the restricted scalar module $\operatorname{RestrictScalars}_R^S M$ is also inhabited.

instAddCommMonoidRestrictScalars instance

[I : AddCommMonoid M] : AddCommMonoid (RestrictScalars R S M)

Full source

instance [I : AddCommMonoid M] : AddCommMonoid (RestrictScalars R S M) := I

Additive Commutative Monoid Structure on Restricted Scalars

Informal description

For any commutative semiring $R$, semiring $S$ with an $R$-algebra structure, and additive commutative monoid $M$, the restriction of scalars $\operatorname{RestrictScalars}_R^S M$ is also an additive commutative monoid.

instAddCommGroupRestrictScalars instance

[I : AddCommGroup M] : AddCommGroup (RestrictScalars R S M)

Full source

instance [I : AddCommGroup M] : AddCommGroup (RestrictScalars R S M) := I

Additive Commutative Group Structure on Restriction of Scalars

Informal description

For any commutative additive group $M$ over a semiring $S$ with an $R$-algebra structure, the restriction of scalars $\operatorname{RestrictScalars}_R^S M$ is also a commutative additive group.

RestrictScalars.moduleOrig definition

[I : Module S M] : Module S (RestrictScalars R S M)

Full source

/-- We temporarily install an action of the original ring on `RestrictScalars R S M`. -/
def RestrictScalars.moduleOrig [I : Module S M] : Module S (RestrictScalars R S M) := I

Original module structure under scalar restriction

Informal description

Given a commutative semiring $R$, a semiring $S$ with an $R$-algebra structure, and an $S$-module $M$, the original $S$-module structure on $M$ is preserved when viewed as a module over the restricted scalars $\operatorname{RestrictScalars}_R^S M$.

RestrictScalars.module instance

[Module S M] : Module R (RestrictScalars R S M)

Full source

/-- 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.module [Module S M] : Module R (RestrictScalars R S M) :=
  Module.compHom M (algebraMap R S)

Module Structure via Restriction of Scalars

Informal description

Given a commutative semiring $R$, a semiring $S$ with an $R$-algebra structure, and an $S$-module $M$, the restriction of scalars $\operatorname{RestrictScalars}_R^S M$ inherits a canonical $R$-module structure. This is obtained by composing the original scalar multiplication with the algebra map $R \to S$.

RestrictScalars.isScalarTower instance

[Module S M] : IsScalarTower R S (RestrictScalars R S M)

Full source

/-- This instance is only relevant when `RestrictScalars.moduleOrig` is available as an instance.
-/
instance RestrictScalars.isScalarTower [Module S M] : IsScalarTower R S (RestrictScalars R S M) :=
  ⟨fun r S M ↦ by
    rw [Algebra.smul_def, mul_smul]
    rfl⟩

Scalar Tower Property for Restricted Scalars

Informal description

For any commutative semiring $R$, semiring $S$ with an $R$-algebra structure, and $S$-module $M$, the scalar multiplication operations on $\operatorname{RestrictScalars}_R^S M$ satisfy the tower property: for any $r \in R$, $s \in S$, and $m \in M$, we have $(r \cdot s) \cdot m = r \cdot (s \cdot m)$.

RestrictScalars.opModule instance

[Module Sᵐᵒᵖ M] : Module Rᵐᵒᵖ (RestrictScalars R S M)

Full source

/-- 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]`.
-/
instance RestrictScalars.opModule [Module Sᵐᵒᵖ M] : Module Rᵐᵒᵖ (RestrictScalars R S M) :=
  letI : Module Sᵐᵒᵖ (RestrictScalars R S M) := ‹Module Sᵐᵒᵖ M›
  Module.compHom M (RingHom.op <| algebraMap R S)

Right Module Structure via Restriction of Scalars in Opposite Semiring

Informal description

For any commutative semiring $R$, semiring $S$ with an $R$-algebra structure, and right $S$-module $M$, the restriction of scalars $\operatorname{RestrictScalars}_R^S M$ inherits a canonical right $R$-module structure. This is obtained by composing the original right scalar multiplication with the algebra map $R \to S$ (viewed in the opposite semiring).

RestrictScalars.isCentralScalar instance

[Module S M] [Module Sᵐᵒᵖ M] [IsCentralScalar S M] : IsCentralScalar R (RestrictScalars R S M)

Full source

instance RestrictScalars.isCentralScalar [Module S M] [Module Sᵐᵒᵖ M] [IsCentralScalar S M] :
    IsCentralScalar R (RestrictScalars R S M) where
  op_smul_eq_smul r _x := (op_smul_eq_smul (algebraMap R S r) (_ : M) :)

Central Scalar Multiplication for Restricted Scalars

Informal description

For any commutative semiring $R$, semiring $S$ with an $R$-algebra structure, and $S$-module $M$ with both left and right $S$-module structures that are central (i.e., the left and right scalar multiplications coincide), the restriction of scalars $\operatorname{RestrictScalars}_R^S M$ inherits a central scalar multiplication structure over $R$.

RestrictScalars.lsmul definition

[Module S M] : S →ₐ[R] Module.End R (RestrictScalars R S M)

Full source

/-- The `R`-algebra homomorphism from the original coefficient algebra `S` to endomorphisms
of `RestrictScalars R S M`.
-/
def RestrictScalars.lsmul [Module S M] : S →ₐ[R] Module.End R (RestrictScalars R S M) :=
  -- We use `RestrictScalars.moduleOrig` in the implementation,
  -- but not in the type.
  letI : Module S (RestrictScalars R S M) := RestrictScalars.moduleOrig R S M
  Algebra.lsmul R R (RestrictScalars R S M)

Left multiplication algebra homomorphism for restricted scalars

Informal description

Given a commutative semiring $R$, a semiring $S$ with an $R$-algebra structure, and an $S$-module $M$, the map $\text{lsmul} : S \to \text{End}_R(\text{RestrictScalars}_R^S M)$ is the $R$-algebra homomorphism that sends each element $s \in S$ to the $R$-linear endomorphism given by left multiplication by $s$ on $\text{RestrictScalars}_R^S M$.

RestrictScalars.addEquiv definition

: RestrictScalars R S M ≃+ M

Full source

/-- `RestrictScalars.addEquiv` is the additive equivalence with the original module. -/
def RestrictScalars.addEquiv : RestrictScalarsRestrictScalars R S M ≃+ M :=
  AddEquiv.refl M

Additive equivalence between restricted scalars and original module

Informal description

The additive equivalence $\operatorname{RestrictScalars}_R^S M \simeq^+ M$ between the module with restricted scalars and the original module, which is the identity map since they are definitionally equal.

RestrictScalars.smul_def theorem

 (c : R) (x : RestrictScalars R S M) :
  c • x = (RestrictScalars.addEquiv R S M).symm (algebraMap R S c • RestrictScalars.addEquiv R S M x)

Full source

theorem RestrictScalars.smul_def (c : R) (x : RestrictScalars R S M) :
    c • x = (RestrictScalars.addEquiv R S M).symm
      (algebraMap R S c • RestrictScalars.addEquiv R S M x) :=
  rfl

Definition of Scalar Multiplication in Restricted Scalar Module

Informal description

For any element $c \in R$ and any element $x \in \operatorname{RestrictScalars}_R^S M$, the scalar multiplication $c \bullet x$ in the restricted scalar module is equal to the inverse image under the additive equivalence $\operatorname{RestrictScalars}_R^S M \simeq^+ M$ of the scalar multiplication $\phi(c) \bullet f(x)$, where $\phi: R \to S$ is the algebra map and $f$ is the additive equivalence.

RestrictScalars.addEquiv_map_smul theorem

 (c : R) (x : RestrictScalars R S M) :
  RestrictScalars.addEquiv R S M (c • x) = algebraMap R S c • RestrictScalars.addEquiv R S M x

Full source

@[simp]
theorem RestrictScalars.addEquiv_map_smul (c : R) (x : RestrictScalars R S M) :
    RestrictScalars.addEquiv R S M (c • x) = algebraMap R S c • RestrictScalars.addEquiv R S M x :=
  rfl

Compatibility of scalar multiplication with additive equivalence under restriction of scalars

Informal description

Let $R$ be a commutative semiring, $S$ a semiring with an $R$-algebra structure, and $M$ an $S$-module. For any $c \in R$ and $x \in \operatorname{RestrictScalars}_R^S M$, the additive equivalence $f : \operatorname{RestrictScalars}_R^S M \simeq^+ M$ satisfies $$ f(c \cdot x) = \phi(c) \cdot f(x), $$ where $\phi : R \to S$ is the algebra map and $\cdot$ denotes scalar multiplication.

RestrictScalars.addEquiv_symm_map_algebraMap_smul theorem

 (r : R) (x : M) :
  (RestrictScalars.addEquiv R S M).symm (algebraMap R S r • x) = r • (RestrictScalars.addEquiv R S M).symm x

Full source

theorem RestrictScalars.addEquiv_symm_map_algebraMap_smul (r : R) (x : M) :
    (RestrictScalars.addEquiv R S M).symm (algebraMap R S r • x) =
      r • (RestrictScalars.addEquiv R S M).symm x :=
  rfl

Compatibility of scalar multiplication with additive equivalence inverse under restriction of scalars

Informal description

For any element $r \in R$ and $x \in M$, the inverse of the additive equivalence $\operatorname{RestrictScalars}_R^S M \simeq^+ M$ maps the scalar multiplication $\phi(r) \bullet x$ in $M$ (where $\phi: R \to S$ is the algebra map) to the scalar multiplication $r \bullet f^{-1}(x)$ in $\operatorname{RestrictScalars}_R^S M$, where $f$ is the additive equivalence. In other words, $f^{-1}(\phi(r) \bullet x) = r \bullet f^{-1}(x)$.

RestrictScalars.addEquiv_symm_map_smul_smul theorem

 (r : R) (s : S) (x : M) :
  (RestrictScalars.addEquiv R S M).symm ((r • s) • x) = r • (RestrictScalars.addEquiv R S M).symm (s • x)

Full source

theorem RestrictScalars.addEquiv_symm_map_smul_smul (r : R) (s : S) (x : M) :
    (RestrictScalars.addEquiv R S M).symm ((r • s) • x) =
      r • (RestrictScalars.addEquiv R S M).symm (s • x) := by
  rw [Algebra.smul_def, mul_smul]
  rfl

Inverse of Additive Equivalence Preserves Scalar Multiplication under Restriction of Scalars

Informal description

For any element $r$ in a commutative semiring $R$, any element $s$ in a semiring $S$ with an $R$-algebra structure, and any element $x$ in an $S$-module $M$, the inverse of the additive equivalence $\operatorname{RestrictScalars}_R^S M \simeq^+ M$ maps the scalar multiplication $(r \cdot s) \bullet x$ to $r \bullet$ the inverse image of $s \bullet x$ under the additive equivalence.

RestrictScalars.lsmul_apply_apply theorem

 (s : S) (x : RestrictScalars R S M) :
  RestrictScalars.lsmul R S M s x = (RestrictScalars.addEquiv R S M).symm (s • RestrictScalars.addEquiv R S M x)

Full source

theorem RestrictScalars.lsmul_apply_apply (s : S) (x : RestrictScalars R S M) :
    RestrictScalars.lsmul R S M s x =
      (RestrictScalars.addEquiv R S M).symm (s • RestrictScalars.addEquiv R S M x) :=
  rfl

Left Multiplication via Additive Equivalence in Restricted Scalars

Informal description

For any element $s \in S$ and any element $x \in \operatorname{RestrictScalars}_R^S M$, the left multiplication map $\text{lsmul}(s)$ applied to $x$ is equal to the inverse of the additive equivalence applied to $s$ multiplied by the image of $x$ under the additive equivalence. That is, $\text{lsmul}(s)(x) = f^{-1}(s \cdot f(x))$, where $f : \operatorname{RestrictScalars}_R^S M \simeq^+ M$ is the additive equivalence.

instSemiringRestrictScalars instance

[I : Semiring A] : Semiring (RestrictScalars R S A)

Full source

instance [I : Semiring A] : Semiring (RestrictScalars R S A) := I

Semiring Structure on Restricted Scalars

Informal description

For any semiring $A$, the type `RestrictScalars R S A` obtained by restricting scalars from $S$ to $R$ inherits a semiring structure from $A$.

instRingRestrictScalars instance

[I : Ring A] : Ring (RestrictScalars R S A)

Full source

instance [I : Ring A] : Ring (RestrictScalars R S A) := I

Ring Structure under Restriction of Scalars

Informal description

For any ring $A$ and any restriction of scalars from $S$ to $R$, the restricted scalar structure $\text{RestrictScalars}\, R\, S\, A$ is also a ring.

instCommSemiringRestrictScalars instance

[I : CommSemiring A] : CommSemiring (RestrictScalars R S A)

Full source

instance [I : CommSemiring A] : CommSemiring (RestrictScalars R S A) := I

Commutative Semiring Structure on Restricted Scalars

Informal description

For any commutative semiring $A$, the type `RestrictScalars R S A` (which represents $A$ viewed as an $R$-module by restricting the scalar multiplication from $S$ to $R$) is also a commutative semiring.

instCommRingRestrictScalars instance

[I : CommRing A] : CommRing (RestrictScalars R S A)

Full source

instance [I : CommRing A] : CommRing (RestrictScalars R S A) := I

Commutative Ring Structure on Restriction of Scalars

Informal description

For any commutative ring $A$ and any $R$-algebra $S$, the restriction of scalars $\mathrm{RestrictScalars}\, R\, S\, A$ is again a commutative ring.

RestrictScalars.ringEquiv definition

: RestrictScalars R S A ≃+* A

Full source

/-- Tautological ring isomorphism `RestrictScalars R S A ≃+* A`. -/
def RestrictScalars.ringEquiv : RestrictScalarsRestrictScalars R S A ≃+* A :=
  RingEquiv.refl _

Tautological ring isomorphism for restricted scalars

Informal description

The tautological ring isomorphism between `RestrictScalars R S A` and `A`, where `A` is viewed as an `R`-module by restricting the scalar multiplication from `S` to `R` via the algebra map `R → S`. This isomorphism preserves both the additive and multiplicative structures.

RestrictScalars.ringEquiv_map_smul theorem

 (r : R) (x : RestrictScalars R S A) :
  RestrictScalars.ringEquiv R S A (r • x) = algebraMap R S r • RestrictScalars.ringEquiv R S A x

Full source

@[simp]
theorem RestrictScalars.ringEquiv_map_smul (r : R) (x : RestrictScalars R S A) :
    RestrictScalars.ringEquiv R S A (r • x) =
      algebraMap R S r • RestrictScalars.ringEquiv R S A x :=
  rfl

Ring Equivalence Preserves Scalar Multiplication under Restriction of Scalars

Informal description

For any element $r \in R$ and any element $x \in \operatorname{RestrictScalars}_R^S A$, the ring equivalence $\operatorname{RestrictScalars}_R^S A \simeq+* A$ maps the scalar multiplication $r \cdot x$ to the scalar multiplication $\phi(r) \cdot \operatorname{RestrictScalars.ringEquiv}(x)$, where $\phi : R \to S$ is the algebra map.

RestrictScalars.algebra instance

: Algebra R (RestrictScalars R S A)

Full source

/-- `R ⟶ S` induces `S-Alg ⥤ R-Alg` -/
instance RestrictScalars.algebra : Algebra R (RestrictScalars R S A) where
  algebraMap := (algebraMap S A).comp (algebraMap R S)
  smul := (· • ·)
  commutes' := fun _ _ ↦ Algebra.commutes' (A := A) _ _
  smul_def' := fun _ _ ↦ Algebra.smul_def' (A := A) _ _

Algebra Structure via Restriction of Scalars

Informal description

Given a commutative semiring $R$, a semiring $S$ with an $R$-algebra structure, and an $S$-algebra $A$, the restriction of scalars $\operatorname{RestrictScalars}_R^S A$ inherits a canonical $R$-algebra structure. This is obtained by composing the original algebra structure with the algebra map $R \to S$.

RestrictScalars.ringEquiv_algebraMap theorem

(r : R) : RestrictScalars.ringEquiv R S A (algebraMap R (RestrictScalars R S A) r) = algebraMap S A (algebraMap R S r)

Full source

@[simp]
theorem RestrictScalars.ringEquiv_algebraMap (r : R) :
    RestrictScalars.ringEquiv R S A (algebraMap R (RestrictScalars R S A) r) =
      algebraMap S A (algebraMap R S r) :=
  rfl

Compatibility of algebra maps with restriction of scalars equivalence

Informal description

For any element $r \in R$, the ring equivalence $\operatorname{RestrictScalars}_R^S A \simeq+* A$ maps the algebra map $\phi_R : R \to \operatorname{RestrictScalars}_R^S A$ applied to $r$ to the composition of algebra maps $\phi_S \circ \phi_R : R \to S \to A$ applied to $r$, where $\phi_R : R \to S$ is the given algebra map and $\phi_S : S \to A$ is the algebra structure on $A$. In symbols: $$\text{RestrictScalars.ringEquiv}_{R,S,A}(\phi_R(r)) = \phi_S(\phi_R(r))$$ where: - $\phi_R : R \to \operatorname{RestrictScalars}_R^S A$ is the restricted algebra map - $\phi_R : R \to S$ is the original algebra map - $\phi_S : S \to A$ is the algebra structure on $A$

Main definitions

See also