doc-next-gen

Mathlib.Algebra.Algebra.Tower

Module docstring

{"# Towers of algebras

In this file we prove basic facts about towers of algebra.

An algebra tower A/S/R is expressed by having instances of Algebra A S, Algebra R S, Algebra R A and IsScalarTower R S A, the later asserting the compatibility condition (r • s) • a = r • (s • a).

An important definition is toAlgHom R S A, the canonical R-algebra homomorphism S →ₐ[R] A.

"}

Algebra.lsmul definition
: A →ₐ[R] Module.End B M
Full source 
/-- The `R`-algebra morphism `A → End (M)` corresponding to the representation of the algebra `A`
on the `B`-module `M`.

This is a stronger version of `DistribMulAction.toLinearMap`, and could also have been
called `Algebra.toModuleEnd`.

The typeclasses correspond to the situation where the types act on each other as
```
R ----→ B
| ⟍     |
|   ⟍   |
↓     ↘ ↓
A ----→ M
```
where the diagram commutes, the action by `R` commutes with everything, and the action by `A` and
`B` on `M` commute.

Typically this is most useful with `B = R` as `Algebra.lsmul R R A : A →ₐ[R] Module.End R M`.
However this can be used to get the fact that left-multiplication by `A` is right `A`-linear, and
vice versa, as
```lean
example : A →ₐ[R] Module.End Aᵐᵒᵖ A := Algebra.lsmul R Aᵐᵒᵖ A
example : Aᵐᵒᵖ →ₐ[R] Module.End A A := Algebra.lsmul R A A
```
respectively; though `LinearMap.mulLeft` and `LinearMap.mulRight` can also be used here.
-/
def lsmul : A →ₐ[R] Module.End B M where
  toFun := DistribMulAction.toLinearMap B M
  map_one' := LinearMap.ext fun _ => one_smul A _
  map_mul' a b := LinearMap.ext <| smul_assoc a b
  map_zero' := LinearMap.ext fun _ => zero_smul A _
  map_add' _a _b := LinearMap.ext fun _ => add_smul _ _ _
  commutes' r := LinearMap.ext <| algebraMap_smul A r
Left multiplication as an algebra homomorphism to endomorphisms
Informal description
Given an $R$-algebra $A$ and a $B$-module $M$ where $B$ is another $R$-algebra, the function `Algebra.lsmul` maps each element $a \in A$ to the linear endomorphism of $M$ given by left scalar multiplication by $a$. This defines an $R$-algebra homomorphism from $A$ to the ring of $B$-linear endomorphisms of $M$. More precisely, for each $a \in A$, the map $\text{lsmul}(a) \colon M \to M$ is defined by $\text{lsmul}(a)(x) = a \cdot x$ for all $x \in M$, and the assignment $a \mapsto \text{lsmul}(a)$ is an $R$-algebra homomorphism. This means: 1. $\text{lsmul}(1) = \text{id}_M$ (preserves multiplicative identity) 2. $\text{lsmul}(a \cdot b) = \text{lsmul}(a) \circ \text{lsmul}(b)$ (preserves multiplication) 3. $\text{lsmul}(a + b) = \text{lsmul}(a) + \text{lsmul}(b)$ (preserves addition) 4. $\text{lsmul}(r \cdot a) = r \cdot \text{lsmul}(a)$ for $r \in R$ (compatibility with $R$-algebra structure)
Algebra.lsmul_coe theorem
(a : A) : (lsmul R B M a : M → M) = (a • ·)
Full source 
@[simp]
theorem lsmul_coe (a : A) : (lsmul R B M a : M → M) = (a • ·) := rfl
Left Scalar Multiplication as Function Application: $\text{lsmul}(a)(x) = a \cdot x$
Informal description
For any element $a$ in an $R$-algebra $A$, the linear endomorphism $\text{lsmul}(a) \colon M \to M$ defined by left scalar multiplication by $a$ coincides with the function $x \mapsto a \cdot x$, where $M$ is a module over another $R$-algebra $B$.
IsScalarTower.algebraMap_smul theorem
[SMul R M] [IsScalarTower R A M] (r : R) (x : M) : algebraMap R A r • x = r • x
Full source 
theorem algebraMap_smul [SMul R M] [IsScalarTower R A M] (r : R) (x : M) :
    algebraMap R A r • x = r • x := by
  rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
Equality of Scalar Actions via Algebra Map in Tower Structure
Informal description
Let $R$, $A$, and $M$ be types with scalar multiplication operations, where $A$ is an $R$-algebra and $M$ is both an $A$-module and an $R$-module. If the scalar multiplication operations satisfy the tower property (i.e., $[IsScalarTower R A M]$), then for any $r \in R$ and $x \in M$, the action of the algebra map $\text{algebraMap}_R^A(r)$ on $x$ equals the action of $r$ on $x$, i.e., $\text{algebraMap}_R^A(r) \cdot x = r \cdot x$.
IsScalarTower.of_algebraMap_smul theorem
[SMul R M] (h : ∀ (r : R) (x : M), algebraMap R A r • x = r • x) : IsScalarTower R A M
Full source 
theorem of_algebraMap_smul [SMul R M] (h : ∀ (r : R) (x : M), algebraMap R A r • x = r • x) :
    IsScalarTower R A M where
  smul_assoc r a x := by rw [Algebra.smul_def, mul_smul, h]
Tower Property from Equality of Scalar Actions via Algebra Map
Informal description
Let $R$, $A$, and $M$ be types equipped with scalar multiplication operations, where $A$ is an $R$-algebra and $M$ is both an $A$-module and an $R$-module. If for every $r \in R$ and $x \in M$, the action of the algebra map $\text{algebraMap}_R^A(r)$ on $x$ equals the action of $r$ on $x$, i.e., $\text{algebraMap}_R^A(r) \cdot x = r \cdot x$, then the scalar multiplication operations satisfy the tower property, i.e., $[IsScalarTower R A M]$.
IsScalarTower.of_compHom theorem
: letI := MulAction.compHom M (algebraMap R A : R →* A); IsScalarTower R A M
Full source 
theorem of_compHom : letI := MulAction.compHom M (algebraMap R A : R →* A); IsScalarTower R A M :=
  letI := MulAction.compHom M (algebraMap R A : R →* A); of_algebraMap_smul fun _ _ ↦ rfl
Tower Property via Algebra Map-Induced Scalar Multiplication
Informal description
Let $R$, $A$, and $M$ be types where $A$ is an $R$-algebra and $M$ is both an $A$-module and an $R$-module. If the multiplicative action of $R$ on $M$ is induced via the algebra map $\text{algebraMap}_R^A \colon R \to A$ (i.e., $r \cdot x = \text{algebraMap}_R^A(r) \cdot x$ for all $r \in R$ and $x \in M$), then the scalar multiplication operations satisfy the tower property, i.e., $[IsScalarTower R A M]$.
IsScalarTower.of_algebraMap_eq theorem
[Algebra R A] (h : ∀ x, algebraMap R A x = algebraMap S A (algebraMap R S x)) : IsScalarTower R S A
Full source 
theorem of_algebraMap_eq [Algebra R A]
    (h : ∀ x, algebraMap R A x = algebraMap S A (algebraMap R S x)) : IsScalarTower R S A :=
  ⟨fun x y z => by simp_rw [Algebra.smul_def, RingHom.map_mul, mul_assoc, h]⟩
Tower Property of Scalar Multiplication via Algebra Map Equality
Informal description
Let $R$, $S$, and $A$ be commutative semirings such that $A$ is an $R$-algebra. If for every $x \in R$, the algebra map $\text{algebraMap}_R^A(x)$ equals the composition $\text{algebraMap}_S^A \circ \text{algebraMap}_R^S(x)$, then the scalar multiplication operations satisfy the tower property, i.e., $(r \cdot s) \cdot a = r \cdot (s \cdot a)$ for all $r \in R$, $s \in S$, and $a \in A$.
IsScalarTower.of_algebraMap_eq' theorem
[Algebra R A] (h : algebraMap R A = (algebraMap S A).comp (algebraMap R S)) : IsScalarTower R S A
Full source 
/-- See note [partially-applied ext lemmas]. -/
theorem of_algebraMap_eq' [Algebra R A]
    (h : algebraMap R A = (algebraMap S A).comp (algebraMap R S)) : IsScalarTower R S A :=
  of_algebraMap_eq <| RingHom.ext_iff.1 h
Tower Property via Composition of Algebra Maps
Informal description
Let $R$, $S$, and $A$ be commutative semirings such that $A$ is an $R$-algebra. If the algebra map $\text{algebraMap}_R^A$ is equal to the composition $\text{algebraMap}_S^A \circ \text{algebraMap}_R^S$, then the scalar multiplication operations satisfy the tower property, i.e., $(r \cdot s) \cdot a = r \cdot (s \cdot a)$ for all $r \in R$, $s \in S$, and $a \in A$.
IsScalarTower.algebraMap_eq theorem
: algebraMap R A = (algebraMap S A).comp (algebraMap R S)
Full source 
theorem algebraMap_eq : algebraMap R A = (algebraMap S A).comp (algebraMap R S) :=
  RingHom.ext fun x => by
    simp_rw [RingHom.comp_apply, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
Compatibility of Algebra Maps in a Tower of Algebras
Informal description
For a tower of algebras $R \to S \to A$, the algebra map from $R$ to $A$ is equal to the composition of the algebra maps from $R$ to $S$ and from $S$ to $A$. In other words, the following diagram commutes: $$\text{algebraMap}_{R \to A} = \text{algebraMap}_{S \to A} \circ \text{algebraMap}_{R \to S}$$
IsScalarTower.algebraMap_apply theorem
(x : R) : algebraMap R A x = algebraMap S A (algebraMap R S x)
Full source 
theorem algebraMap_apply (x : R) : algebraMap R A x = algebraMap S A (algebraMap R S x) := by
  rw [algebraMap_eq R S A, RingHom.comp_apply]
Commutativity of Algebra Maps in a Tower for Each Element
Informal description
For any element $x$ in a commutative semiring $R$, the algebra map from $R$ to $A$ evaluated at $x$ equals the algebra map from $S$ to $A$ evaluated at the image of $x$ under the algebra map from $R$ to $S$. In other words, the following diagram commutes for all $x \in R$: $$\text{algebraMap}_{R \to A}(x) = \text{algebraMap}_{S \to A}(\text{algebraMap}_{R \to S}(x))$$
IsScalarTower.Algebra.ext theorem
{S : Type u} {A : Type v} [CommSemiring S] [Semiring A] (h1 h2 : Algebra S A) (h : ∀ (r : S) (x : A), (by have I := h1; exact r • x) = r • x) : h1 = h2
Full source 
@[ext]
theorem Algebra.ext {S : Type u} {A : Type v} [CommSemiring S] [Semiring A] (h1 h2 : Algebra S A)
    (h : ∀ (r : S) (x : A), (by have I := h1; exact r • x) = r • x) : h1 = h2 :=
  Algebra.algebra_ext _ _ fun r => by
    simpa only [@Algebra.smul_def _ _ _ _ h1, @Algebra.smul_def _ _ _ _ h2, mul_one] using h r 1
Uniqueness of Algebra Structure with Identical Scalar Multiplication
Informal description
Let $S$ be a commutative semiring and $A$ a semiring. Given two $S$-algebra structures $h_1$ and $h_2$ on $A$, if for all $r \in S$ and $x \in A$ the scalar multiplications coincide (i.e., $h_1$'s scalar multiplication $r \cdot x$ equals $h_2$'s $r \cdot x$), then $h_1 = h_2$.
IsScalarTower.toAlgHom definition
: S →ₐ[R] A
Full source 
/-- In a tower, the canonical map from the middle element to the top element is an
algebra homomorphism over the bottom element. -/
def toAlgHom : S →ₐ[R] A :=
  { algebraMap S A with commutes' := fun _ => (algebraMap_apply _ _ _ _).symm }
Canonical algebra homomorphism in a tower of algebras
Informal description
Given a tower of algebras \( R \to S \to A \) with the scalar multiplication tower property, the canonical map \( S \to A \) is an \( R \)-algebra homomorphism. This map sends each element \( y \in S \) to its image under the algebra map \( S \to A \).
IsScalarTower.toAlgHom_apply theorem
(y : S) : toAlgHom R S A y = algebraMap S A y
Full source 
theorem toAlgHom_apply (y : S) : toAlgHom R S A y = algebraMap S A y := rfl
Evaluation of Canonical Algebra Homomorphism in Tower of Algebras
Informal description
For any element $y$ in the algebra $S$, the canonical $R$-algebra homomorphism $\text{toAlgHom}_{R,S,A}$ from $S$ to $A$ satisfies $\text{toAlgHom}_{R,S,A}(y) = \text{algebraMap}_{S,A}(y)$, where $\text{algebraMap}_{S,A}$ is the algebra map from $S$ to $A$.
IsScalarTower.coe_toAlgHom theorem
: ↑(toAlgHom R S A) = algebraMap S A
Full source 
@[simp]
theorem coe_toAlgHom : ↑(toAlgHom R S A) = algebraMap S A :=
  RingHom.ext fun _ => rfl
Canonical Algebra Homomorphism Coincides with Algebra Map in Tower
Informal description
The underlying function of the canonical $R$-algebra homomorphism $\text{toAlgHom}_{R,S,A} : S \to A$ in a tower of algebras $R \to S \to A$ coincides with the algebra map $\text{algebraMap}_{S,A} : S \to A$. In other words, for all $y \in S$, we have $\text{toAlgHom}_{R,S,A}(y) = \text{algebraMap}_{S,A}(y)$.
IsScalarTower.coe_toAlgHom' theorem
: (toAlgHom R S A : S → A) = algebraMap S A
Full source 
@[simp]
theorem coe_toAlgHom' : (toAlgHom R S A : S → A) = algebraMap S A := rfl
Canonical Algebra Homomorphism Coincides with Algebra Map in Tower
Informal description
The underlying function of the canonical $R$-algebra homomorphism $\text{toAlgHom}_{R,S,A} : S \to A$ in a tower of algebras $R \to S \to A$ coincides with the algebra map $\text{algebraMap}_{S,A} : S \to A$. In other words, for all $y \in S$, we have $\text{toAlgHom}_{R,S,A}(y) = \text{algebraMap}_{S,A}(y)$.
AlgHom.map_algebraMap theorem
(f : A →ₐ[S] B) (r : R) : f (algebraMap R A r) = algebraMap R B r
Full source 
@[simp]
theorem _root_.AlgHom.map_algebraMap (f : A →ₐ[S] B) (r : R) :
    f (algebraMap R A r) = algebraMap R B r := by
  rw [algebraMap_apply R S A r, f.commutes, ← algebraMap_apply R S B]
Algebra Homomorphism Commutes with Base Change in Tower
Informal description
Let $R$, $S$, $A$, and $B$ be commutative semirings such that $A$ and $B$ are $S$-algebras, and $S$ is an $R$-algebra, forming a tower of algebras $R \to S \to A$ and $R \to S \to B$. For any $S$-algebra homomorphism $f: A \to B$ and any element $r \in R$, we have: $$f(\text{algebraMap}_{R \to A}(r)) = \text{algebraMap}_{R \to B}(r)$$
AlgHom.comp_algebraMap_of_tower theorem
(f : A →ₐ[S] B) : (f : A →+* B).comp (algebraMap R A) = algebraMap R B
Full source 
@[simp]
theorem _root_.AlgHom.comp_algebraMap_of_tower (f : A →ₐ[S] B) :
    (f : A →+* B).comp (algebraMap R A) = algebraMap R B :=
  RingHom.ext (AlgHom.map_algebraMap f)
Compatibility of Algebra Homomorphism with Base Change in Tower
Informal description
Let $R$, $S$, $A$, and $B$ be commutative semirings such that $A$ and $B$ are $S$-algebras, and $S$ is an $R$-algebra, forming a tower of algebras $R \to S \to A$ and $R \to S \to B$. For any $S$-algebra homomorphism $f: A \to B$, the composition of $f$ (viewed as a ring homomorphism) with the algebra map $\text{algebraMap}_{R \to A}$ equals the algebra map $\text{algebraMap}_{R \to B}$. In other words: $$f \circ \text{algebraMap}_{R \to A} = \text{algebraMap}_{R \to B}$$
IsScalarTower.subsemiring instance
(U : Subsemiring S) : IsScalarTower U S A
Full source 
instance (priority := 999) subsemiring (U : Subsemiring S) : IsScalarTower U S A :=
  of_algebraMap_eq fun _x => rfl
Tower Property of Scalar Multiplication via Subsemiring
Informal description
For any subsemiring $U$ of a commutative semiring $S$, and any $S$-algebra $A$, the scalar multiplication operations satisfy the tower property, i.e., $(u \cdot s) \cdot a = u \cdot (s \cdot a)$ for all $u \in U$, $s \in S$, and $a \in A$.
IsScalarTower.of_algHom instance
{R A B : Type*} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : @IsScalarTower R A B _ f.toRingHom.toAlgebra.toSMul _
Full source 
instance (priority := 999) of_algHom {R A B : Type*} [CommSemiring R] [CommSemiring A]
    [CommSemiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
    @IsScalarTower R A B _ f.toRingHom.toAlgebra.toSMul _ :=
  letI := (f : A →+* B).toAlgebra
  of_algebraMap_eq fun x => (f.commutes x).symm
Tower Property of Scalar Multiplication via Algebra Homomorphism
Informal description
Let $R$, $A$, and $B$ be commutative semirings equipped with $R$-algebra structures. Given an $R$-algebra homomorphism $f \colon A \to B$, the scalar multiplication operations satisfy the tower property, i.e., $(r \cdot a) \cdot b = r \cdot (a \cdot b)$ for all $r \in R$, $a \in A$, and $b \in B$, where the scalar multiplication of $R$ on $B$ is defined via $f$.
AlgHom.restrictScalars definition
(f : A →ₐ[S] B) : A →ₐ[R] B
Full source 
/-- R ⟶ S induces S-Alg ⥤ R-Alg -/
def restrictScalars (f : A →ₐ[S] B) : A →ₐ[R] B :=
  { (f : A →+* B) with
    commutes' := fun r => by
      rw [algebraMap_apply R S A, algebraMap_apply R S B]
      exact f.commutes (algebraMap R S r) }
Restriction of scalars of an algebra homomorphism
Informal description
Given an algebra homomorphism $f: A \to_{\text{Alg}[S]} B$ between $S$-algebras $A$ and $B$, this defines the restriction of scalars of $f$ to an $R$-algebra homomorphism $A \to_{\text{Alg}[R]} B$, where $R$ is a subalgebra of $S$. The restriction preserves the action of $R$ via the composition $R \to S \to A$ and $R \to S \to B$.
AlgHom.restrictScalars_apply theorem
(f : A →ₐ[S] B) (x : A) : f.restrictScalars R x = f x
Full source 
theorem restrictScalars_apply (f : A →ₐ[S] B) (x : A) : f.restrictScalars R x = f x := rfl
Restriction of Scalars Preserves Evaluation: $(f.\text{restrictScalars}\, R)(x) = f(x)$
Informal description
For any $S$-algebra homomorphism $f \colon A \to_{\text{Alg}[S]} B$ and any element $x \in A$, the evaluation of the restricted scalar homomorphism $f.\text{restrictScalars}\, R$ at $x$ equals $f(x)$. That is, $(f.\text{restrictScalars}\, R)(x) = f(x)$.
AlgHom.coe_restrictScalars theorem
(f : A →ₐ[S] B) : (f.restrictScalars R : A →+* B) = f
Full source 
@[simp]
theorem coe_restrictScalars (f : A →ₐ[S] B) : (f.restrictScalars R : A →+* B) = f := rfl
Ring Homomorphism Equality Under Scalar Restriction
Informal description
For any $S$-algebra homomorphism $f: A \to_{\text{Alg}[S]} B$, the underlying ring homomorphism of the scalar-restricted homomorphism $f.\text{restrictScalars}\, R : A \to_{\text{Alg}[R]} B$ is equal to $f$ itself.
AlgHom.coe_restrictScalars' theorem
(f : A →ₐ[S] B) : (restrictScalars R f : A → B) = f
Full source 
@[simp]
theorem coe_restrictScalars' (f : A →ₐ[S] B) : (restrictScalars R f : A → B) = f := rfl
Equality of Underlying Functions in Scalar Restriction of Algebra Homomorphisms
Informal description
For any $S$-algebra homomorphism $f \colon A \to_{\text{Alg}[S]} B$, the underlying function of the scalar-restricted homomorphism $\text{restrictScalars}_R f \colon A \to_{\text{Alg}[R]} B$ is equal to $f$ itself. In other words, the map $\text{restrictScalars}_R f$ and $f$ coincide as functions from $A$ to $B$.
AlgHom.restrictScalars_injective theorem
: Function.Injective (restrictScalars R : (A →ₐ[S] B) → A →ₐ[R] B)
Full source 
theorem restrictScalars_injective :
    Function.Injective (restrictScalars R : (A →ₐ[S] B) → A →ₐ[R] B) := fun _ _ h =>
  AlgHom.ext (AlgHom.congr_fun h :)
Injectivity of Scalar Restriction for Algebra Homomorphisms
Informal description
The restriction of scalars map from $S$-algebra homomorphisms $A \to_{\text{Alg}[S]} B$ to $R$-algebra homomorphisms $A \to_{\text{Alg}[R]} B$ is injective. In other words, if two $S$-algebra homomorphisms $f, g: A \to B$ satisfy $f \circ \iota = g \circ \iota$ when restricted to $R$-algebra homomorphisms (where $\iota: R \to S$ is the algebra map), then $f = g$.
AlgEquiv.restrictScalars definition
(f : A ≃ₐ[S] B) : A ≃ₐ[R] B
Full source 
/-- R ⟶ S induces S-Alg ⥤ R-Alg -/
def restrictScalars (f : A ≃ₐ[S] B) : A ≃ₐ[R] B :=
  { (f : A ≃+* B) with
    commutes' := fun r => by
      rw [algebraMap_apply R S A, algebraMap_apply R S B]
      exact f.commutes (algebraMap R S r) }
Restriction of scalars for algebra equivalences
Informal description
Given an algebra equivalence $f : A \simeq_{\text{Alg}[S]} B$ between two $S$-algebras $A$ and $B$, the function `restrictScalars` constructs an $R$-algebra equivalence $A \simeq_{\text{Alg}[R]} B$ by restricting the scalars from $S$ to $R$. This means that for any $r \in R$, the equivalence $f$ commutes with the algebra maps from $R$ to $A$ and $B$ via the algebra map from $R$ to $S$.
AlgEquiv.restrictScalars_apply theorem
(f : A ≃ₐ[S] B) (x : A) : f.restrictScalars R x = f x
Full source 
theorem restrictScalars_apply (f : A ≃ₐ[S] B) (x : A) : f.restrictScalars R x = f x := rfl
Equality of Restricted Scalar Equivalence Evaluation: $(f.\text{restrictScalars}\, R)(x) = f(x)$
Informal description
For any algebra equivalence $f : A \simeq_{\text{Alg}[S]} B$ between $S$-algebras $A$ and $B$, and for any element $x \in A$, the evaluation of the restricted scalar equivalence $f.\text{restrictScalars}\, R$ at $x$ equals the evaluation of $f$ at $x$, i.e., $(f.\text{restrictScalars}\, R)(x) = f(x)$.
AlgEquiv.coe_restrictScalars theorem
(f : A ≃ₐ[S] B) : (f.restrictScalars R : A ≃+* B) = f
Full source 
@[simp]
theorem coe_restrictScalars (f : A ≃ₐ[S] B) : (f.restrictScalars R : A ≃+* B) = f := rfl
Restriction of Scalars Preserves Underlying Ring Equivalence
Informal description
For any algebra equivalence $f : A \simeq_{\text{Alg}[S]} B$ between $S$-algebras $A$ and $B$, the underlying ring equivalence obtained by restricting scalars from $S$ to $R$ is equal to $f$ itself, i.e., $(f.\text{restrictScalars}\,R : A \simeq+* B) = f$.
AlgEquiv.coe_restrictScalars' theorem
(f : A ≃ₐ[S] B) : (restrictScalars R f : A → B) = f
Full source 
@[simp]
theorem coe_restrictScalars' (f : A ≃ₐ[S] B) : (restrictScalars R f : A → B) = f := rfl
Restriction of Scalars Preserves Underlying Function
Informal description
For any algebra equivalence $f : A \simeq_{\text{Alg}[S]} B$ between $S$-algebras $A$ and $B$, the underlying function obtained by restricting scalars from $S$ to $R$ is equal to $f$ itself, i.e., $(\text{restrictScalars}\, R\, f : A \to B) = f$.
AlgEquiv.restrictScalars_injective theorem
: Function.Injective (restrictScalars R : (A ≃ₐ[S] B) → A ≃ₐ[R] B)
Full source 
theorem restrictScalars_injective :
    Function.Injective (restrictScalars R : (A ≃ₐ[S] B) → A ≃ₐ[R] B) := fun _ _ h =>
  AlgEquiv.ext (AlgEquiv.congr_fun h :)
Injectivity of Scalar Restriction for Algebra Equivalences
Informal description
The function `restrictScalars R` that maps an $S$-algebra equivalence $A \simeq_{\text{Alg}[S]} B$ to an $R$-algebra equivalence $A \simeq_{\text{Alg}[R]} B$ is injective. In other words, if two $S$-algebra equivalences $f$ and $g$ satisfy $\text{restrictScalars}\,R\,f = \text{restrictScalars}\,R\,g$, then $f = g$.
Submodule.restrictScalars_span theorem
(hsur : Function.Surjective (algebraMap R A)) (X : Set M) : restrictScalars R (span A X) = span R X
Full source 
/-- If `A` is an `R`-algebra such that the induced morphism `R →+* A` is surjective, then the
`R`-module generated by a set `X` equals the `A`-module generated by `X`. -/
theorem restrictScalars_span (hsur : Function.Surjective (algebraMap R A)) (X : Set M) :
    restrictScalars R (span A X) = span R X := by
  refine ((span_le_restrictScalars R A X).antisymm fun m hm => ?_).symm
  refine span_induction subset_span (zero_mem _) (fun _ _ _ _ => add_mem) (fun a m _ hm => ?_) hm
  obtain ⟨r, rfl⟩ := hsur a
  simpa [algebraMap_smul] using smul_mem _ r hm
Equality of Restricted Scalar Span and $R$-Span under Surjective Algebra Map
Informal description
Let $R$ be a commutative semiring and $A$ an $R$-algebra such that the canonical $R$-algebra homomorphism $R \to A$ is surjective. For any subset $X$ of an $A$-module $M$, the $R$-submodule obtained by restricting scalars of the $A$-span of $X$ is equal to the $R$-span of $X$, i.e., $$(\operatorname{span}_A X)\big|_R = \operatorname{span}_R X.$$
Submodule.smul_mem_span_smul_of_mem theorem
{s : Set S} {t : Set A} {k : S} (hks : k ∈ span R s) {x : A} (hx : x ∈ t) : k • x ∈ span R (s • t)
Full source 
theorem smul_mem_span_smul_of_mem {s : Set S} {t : Set A} {k : S} (hks : k ∈ span R s) {x : A}
    (hx : x ∈ t) : k • x ∈ span R (s • t) :=
  span_induction (fun _ hc => subset_span <| Set.smul_mem_smul hc hx)
    (by rw [zero_smul]; exact zero_mem _)
    (fun c₁ c₂ _ _ ih₁ ih₂ => by rw [add_smul]; exact add_mem ih₁ ih₂)
    (fun b c _ hc => by rw [IsScalarTower.smul_assoc]; exact smul_mem _ _ hc) hks
Scalar Multiplication Preserves Span in Algebra Tower: $k \in \operatorname{span}_R(s) \land x \in t \implies k \bullet x \in \operatorname{span}_R(s \bullet t)$
Informal description
Let $R$ be a semiring, $S$ an $R$-algebra, and $A$ an $S$-module. For any subsets $s \subseteq S$ and $t \subseteq A$, if $k$ is an element in the $R$-linear span of $s$ and $x$ is an element of $t$, then the scalar product $k \bullet x$ lies in the $R$-linear span of the pointwise scalar product set $s \bullet t$.
Submodule.span_smul_of_span_eq_top theorem
{s : Set S} (hs : span R s = ⊤) (t : Set A) : span R (s • t) = (span S t).restrictScalars R
Full source 
theorem span_smul_of_span_eq_top {s : Set S} (hs : span R s = ⊤) (t : Set A) :
    span R (s • t) = (span S t).restrictScalars R :=
  le_antisymm
    (span_le.2 fun _x ⟨p, _hps, _q, hqt, hpqx⟩ ↦ hpqx ▸ (span S t).smul_mem p (subset_span hqt))
    fun _ hp ↦ closure_induction (hx := hp) (zero_mem _) (fun _ _ _ _ ↦ add_mem) fun s0 y hy ↦ by
      refine span_induction (fun x hx ↦ subset_span <| by exact ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_
        (hs ▸ mem_top : s0 ∈ span R s)
      · rw [zero_smul]; apply zero_mem
      · intro _ _ _ _; rw [add_smul]; apply add_mem
      · intro r s0 _ hy; rw [IsScalarTower.smul_assoc]; exact smul_mem _ r hy
Span of Smul Set Equals Restricted Span When Base Span is Full
Informal description
Let $R$ be a semiring, $S$ an $R$-algebra, and $A$ an $S$-algebra such that the scalar multiplication is compatible (i.e., $(r \cdot s) \cdot a = r \cdot (s \cdot a)$ for $r \in R$, $s \in S$, $a \in A$). Given a subset $s \subseteq S$ whose $R$-linear span is the entire algebra $S$ (i.e., $\operatorname{span}_R s = \top$), and any subset $t \subseteq A$, the $R$-linear span of the pointwise product $s \cdot t$ equals the $S$-linear span of $t$ restricted to $R$-scalars. That is: $$\operatorname{span}_R (s \cdot t) = (\operatorname{span}_S t)_{\text{restrictScalars } R}$$
Submodule.smul_mem_span_smul' theorem
{s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A} (hx : x ∈ span R (s • t)) : k • x ∈ span R (s • t)
Full source 
theorem smul_mem_span_smul' {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A}
    (hx : x ∈ span R (s • t)) : k • x ∈ span R (s • t) := by
  rw [span_smul_of_span_eq_top hs] at hx ⊢; exact (span S t).smul_mem k hx
Closure of Span under Scalar Multiplication in Algebra Tower: $x \in \operatorname{span}_R(s \bullet t) \implies k \bullet x \in \operatorname{span}_R(s \bullet t)$ when $\operatorname{span}_R(s) = S$
Informal description
Let $R$ be a semiring, $S$ an $R$-algebra, and $A$ an $S$-module. Given a subset $s \subseteq S$ whose $R$-linear span is the entire algebra $S$ (i.e., $\operatorname{span}_R s = \top$), and any subset $t \subseteq A$, if $x$ is in the $R$-linear span of $s \bullet t$ and $k \in S$, then the scalar product $k \bullet x$ lies in the $R$-linear span of $s \bullet t$.
Submodule.smul_mem_span_smul theorem
{s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A} (hx : x ∈ span R t) : k • x ∈ span R (s • t)
Full source 
theorem smul_mem_span_smul {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A}
    (hx : x ∈ span R t) : k • x ∈ span R (s • t) := by
  rw [span_smul_of_span_eq_top hs]
  exact (span S t).smul_mem k (span_le_restrictScalars R S t hx)
Scalar Multiplication Preserves Span Inclusion in Algebra Tower
Informal description
Let $R$ be a semiring, $S$ an $R$-algebra, and $A$ an $S$-algebra with compatible scalar multiplication (i.e., $(r \cdot s) \cdot a = r \cdot (s \cdot a)$ for $r \in R$, $s \in S$, $a \in A$). Given a subset $s \subseteq S$ whose $R$-linear span is the entire algebra $S$ (i.e., $\operatorname{span}_R s = \top$), and any subset $t \subseteq A$, if $x$ is in the $R$-linear span of $t$, then for any $k \in S$, the element $k \cdot x$ is in the $R$-linear span of the pointwise product $s \cdot t$.
Submodule.span_algebraMap_image theorem
(a : Set R) : Submodule.span R (algebraMap R S '' a) = (Submodule.span R a).map (Algebra.linearMap R S)
Full source 
/-- A variant of `Submodule.span_image` for `algebraMap`. -/
theorem span_algebraMap_image (a : Set R) :
    Submodule.span R (algebraMapalgebraMap R S '' a) = (Submodule.span R a).map (Algebra.linearMap R S) :=
  (Submodule.span_image <| Algebra.linearMap R S).trans rfl
Span-Image Commutation for Algebra Maps
Informal description
Let $R$ be a commutative semiring and $S$ an $R$-algebra. For any subset $a \subseteq R$, the $R$-linear span of the image of $a$ under the algebra map $\text{algebraMap} \colon R \to S$ is equal to the image under $\text{Algebra.linearMap} \colon R \to S$ of the $R$-linear span of $a$. In symbols: \[ \operatorname{span}_R (\text{algebraMap}(a)) = (\operatorname{span}_R a).\text{map} (\text{Algebra.linearMap}). \]
Submodule.span_algebraMap_image_of_tower theorem
{S T : Type*} [CommSemiring S] [Semiring T] [Module R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (a : Set S) : Submodule.span R (algebraMap S T '' a) = (Submodule.span R a).map ((Algebra.linearMap S T).restrictScalars R)
Full source 
theorem span_algebraMap_image_of_tower {S T : Type*} [CommSemiring S] [Semiring T] [Module R S]
    [Algebra R T] [Algebra S T] [IsScalarTower R S T] (a : Set S) :
    Submodule.span R (algebraMapalgebraMap S T '' a) =
      (Submodule.span R a).map ((Algebra.linearMap S T).restrictScalars R) :=
  (Submodule.span_image <| (Algebra.linearMap S T).restrictScalars R).trans rfl
Compatibility of Span with Algebra Homomorphism in Scalar Tower
Informal description
Let $R$ be a commutative semiring, $S$ a commutative semiring that is an $R$-algebra, and $T$ a semiring that is both an $R$-algebra and an $S$-algebra, with the scalar multiplication operations forming a tower (i.e., $(r \cdot s) \cdot t = r \cdot (s \cdot t)$ for all $r \in R$, $s \in S$, $t \in T$). For any subset $a \subseteq S$, the $R$-linear span of the image of $a$ under the algebra homomorphism $S \to T$ equals the image under the $R$-linear map $S \to T$ (restricted to $R$-scalars) of the $R$-linear span of $a$. In symbols: \[ \operatorname{span}_R (\phi(a)) = \phi(\operatorname{span}_R a) \] where $\phi \colon S \to T$ is the algebra homomorphism.
Submodule.map_mem_span_algebraMap_image theorem
{S T : Type*} [CommSemiring S] [Semiring T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (x : S) (a : Set S) (hx : x ∈ Submodule.span R a) : algebraMap S T x ∈ Submodule.span R (algebraMap S T '' a)
Full source 
theorem map_mem_span_algebraMap_image {S T : Type*} [CommSemiring S] [Semiring T] [Algebra R S]
    [Algebra R T] [Algebra S T] [IsScalarTower R S T] (x : S) (a : Set S)
    (hx : x ∈ Submodule.span R a) : algebraMapalgebraMap S T x ∈ Submodule.span R (algebraMap S T '' a) := by
  rw [span_algebraMap_image_of_tower, mem_map]
  exact ⟨x, hx, rfl⟩
Image of algebra element under span-preserving homomorphism
Informal description
Let $R$ be a commutative semiring, $S$ a commutative semiring that is an $R$-algebra, and $T$ a semiring that is both an $R$-algebra and an $S$-algebra, with the scalar multiplication operations forming a tower (i.e., $(r \cdot s) \cdot t = r \cdot (s \cdot t)$ for all $r \in R$, $s \in S$, $t \in T$). For any subset $a \subseteq S$ and any element $x \in \operatorname{span}_R(a)$, the image of $x$ under the algebra homomorphism $\phi \colon S \to T$ belongs to the $R$-linear span of $\phi(a)$. In symbols: \[ x \in \operatorname{span}_R(a) \implies \phi(x) \in \operatorname{span}_R(\phi(a)) \]
Algebra.lsmul_injective theorem
[NoZeroSMulDivisors A M] {x : A} (hx : x ≠ 0) : Function.Injective (lsmul R B M x)
Full source 
theorem lsmul_injective [NoZeroSMulDivisors A M] {x : A} (hx : x ≠ 0) :
    Function.Injective (lsmul R B M x) :=
  smul_right_injective M hx
Injectivity of Left Multiplication by Nonzero Elements in Modules without Zero Divisors
Informal description
Let $A$ be an $R$-algebra and $M$ be a $B$-module, where $B$ is another $R$-algebra, such that $A$ and $M$ have no zero scalar divisors. For any nonzero element $x \in A$, the left scalar multiplication map $y \mapsto x \cdot y$ is injective on $M$.