Mathlib.Algebra.Algebra.Subalgebra.Tower

Module docstring

{"# Subalgebras in towers of algebras

In this file we prove facts about subalgebras in 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).

Main results

IsScalarTower.Subalgebra: if A/S/R is a tower and S₀ is a subalgebra between S and R, then A/S/S₀ is a tower
IsScalarTower.Subalgebra': if A/S/R is a tower and S₀ is a subalgebra between S and R, then A/S₀/R is a tower
Subalgebra.restrictScalars: turn an S-subalgebra of A into an R-subalgebra of A, given that A/S/R is a tower

Algebra.lmul_algebraMap theorem

(x : R) : Algebra.lmul R A (algebraMap R A x) = Algebra.lsmul R R A x

Full source

theorem lmul_algebraMap (x : R) : Algebra.lmul R A (algebraMap R A x) = Algebra.lsmul R R A x :=
  Eq.symm <| LinearMap.ext <| smul_def x

Equality of Left Multiplication and Scalar Multiplication for Algebra Maps

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any element $x \in R$, the left multiplication map $\text{lmul}(x)$ on $A$ (defined by $a \mapsto x \cdot a$) is equal to the left scalar multiplication map $\text{lsmul}(x)$ (defined by $a \mapsto x \cdot a$ when viewing $A$ as an $R$-module). In other words, for any $x \in R$, the following equality holds between linear maps: $$\text{lmul}(\text{algebraMap}_R^A(x)) = \text{lsmul}_R^A(x)$$ where $\text{algebraMap}_R^A$ is the canonical $R$-algebra homomorphism from $R$ to $A$.

IsScalarTower.subalgebra instance

(S₀ : Subalgebra R S) : IsScalarTower S₀ S A

Full source

instance subalgebra (S₀ : Subalgebra R S) : IsScalarTower S₀ S A :=
  of_algebraMap_eq fun _ ↦ rfl

Tower Property for Subalgebras in Algebra Towers

Informal description

For any subalgebra $S₀$ of $S$ over $R$ in an algebra tower $A/S/R$, the scalar multiplication operations satisfy the tower property for $S₀/S/A$. That is, for any $s₀ \in S₀$, $s \in S$, and $a \in A$, we have $(s₀ \cdot s) \cdot a = s₀ \cdot (s \cdot a)$.

IsScalarTower.subalgebra' instance

(S₀ : Subalgebra R S) : IsScalarTower R S₀ A

Full source

instance subalgebra' (S₀ : Subalgebra R S) : IsScalarTower R S₀ A :=
  @IsScalarTower.of_algebraMap_eq R S₀ A _ _ _ _ _ _ fun _ ↦
    (IsScalarTower.algebraMap_apply R S A _ :)

Tower Property for Subalgebras in Algebra Towers (R/S₀/A Variant)

Informal description

For any subalgebra $S_0$ of $S$ over $R$ in an algebra tower $A/S/R$, the scalar multiplication operations satisfy the tower property for $R/S_0/A$. That is, for any $r \in R$, $s_0 \in S_0$, and $a \in A$, we have $(r \cdot s_0) \cdot a = r \cdot (s_0 \cdot a)$.

Subalgebra.restrictScalars definition

(U : Subalgebra S A) : Subalgebra R A

Full source

/-- Given a tower `A / ↥U / S / R` of algebras, where `U` is an `S`-subalgebra of `A`, reinterpret
`U` as an `R`-subalgebra of `A`. -/
def restrictScalars (U : Subalgebra S A) : Subalgebra R A :=
  { U with
    algebraMap_mem' := fun x ↦ by
      rw [algebraMap_apply R S A]
      exact U.algebraMap_mem _ }

Restriction of scalars for subalgebras in a tower of algebras

Informal description

Given a tower of algebras $ A / U / S / R $ where $ U $ is an $ S $-subalgebra of $ A $, the function `Subalgebra.restrictScalars` reinterprets $ U $ as an $ R $-subalgebra of $ A $. This means that the scalar multiplication by elements of $ R $ on $ A $ is compatible with the existing scalar multiplication structure through $ S $.

Subalgebra.coe_restrictScalars theorem

{U : Subalgebra S A} : (restrictScalars R U : Set A) = (U : Set A)

Full source

@[simp]
theorem coe_restrictScalars {U : Subalgebra S A} : (restrictScalars R U : Set A) = (U : Set A) :=
  rfl

Equality of Underlying Sets in Scalar Restriction for Subalgebras

Informal description

For any $S$-subalgebra $U$ of $A$ in a tower of algebras $A/S/R$, the underlying set of the $R$-subalgebra obtained by restricting scalars from $S$ to $R$ is equal to the underlying set of $U$ itself. In other words, the set of elements in $\text{restrictScalars}_R(U)$ is the same as the set of elements in $U$.

Subalgebra.restrictScalars_top theorem

: restrictScalars R (⊤ : Subalgebra S A) = ⊤

Full source

@[simp]
theorem restrictScalars_top : restrictScalars R (⊤ : Subalgebra S A) = ⊤ :=
  SetLike.coe_injective <| by dsimp

Restriction of Scalars Preserves Top Subalgebra

Informal description

For any algebra tower $A/S/R$, the restriction of scalars from $S$ to $R$ applied to the top subalgebra of $A$ over $S$ yields the top subalgebra of $A$ over $R$. In other words, $\text{restrictScalars}_R(\top : \text{Subalgebra}\, S\, A) = \top$.

Subalgebra.restrictScalars_toSubmodule theorem

{U : Subalgebra S A} : Subalgebra.toSubmodule (U.restrictScalars R) = U.toSubmodule.restrictScalars R

Full source

@[simp]
theorem restrictScalars_toSubmodule {U : Subalgebra S A} :
    Subalgebra.toSubmodule (U.restrictScalars R) = U.toSubmodule.restrictScalars R :=
  SetLike.coe_injective rfl

Compatibility of Subalgebra and Submodule Scalar Restriction

Informal description

For any $S$-subalgebra $U$ of $A$ in an algebra tower $A/S/R$, the underlying $R$-submodule obtained by restricting scalars from $S$ to $R$ is equal to the restriction of scalars applied to the underlying $S$-submodule of $U$. In other words, the following diagram commutes: $$\text{toSubmodule} \circ \text{restrictScalars}_R = \text{restrictScalars}_R \circ \text{toSubmodule}$$

Subalgebra.mem_restrictScalars theorem

{U : Subalgebra S A} {x : A} : x ∈ restrictScalars R U ↔ x ∈ U

Full source

@[simp]
theorem mem_restrictScalars {U : Subalgebra S A} {x : A} : x ∈ restrictScalars R Ux ∈ restrictScalars R U ↔ x ∈ U :=
  Iff.rfl

Membership in Restricted Scalar Subalgebra is Equivalent to Original Membership

Informal description

For any $S$-subalgebra $U$ of $A$ in an algebra tower $A/S/R$, and any element $x \in A$, we have $x \in \text{restrictScalars}_R(U)$ if and only if $x \in U$.

Subalgebra.restrictScalars_injective theorem

: Function.Injective (restrictScalars R : Subalgebra S A → Subalgebra R A)

Full source

theorem restrictScalars_injective :
    Function.Injective (restrictScalars R : Subalgebra S A → Subalgebra R A) := fun U V H ↦
  ext fun x ↦ by rw [← mem_restrictScalars R, H, mem_restrictScalars]

Injectivity of Scalar Restriction for Subalgebras in a Tower

Informal description

The function `restrictScalars R` from the set of $S$-subalgebras of $A$ to the set of $R$-subalgebras of $A$ is injective. That is, for any two $S$-subalgebras $U_1$ and $U_2$ of $A$, if their restrictions to $R$-subalgebras are equal, then $U_1 = U_2$.

Subalgebra.ofRestrictScalars definition

(U : Subalgebra S A) (f : U →ₐ[S] B) : U.restrictScalars R →ₐ[R] B

Full source

/-- Produces an `R`-algebra map from `U.restrictScalars R` given an `S`-algebra map from `U`.

This is a special case of `AlgHom.restrictScalars` that can be helpful in elaboration. -/
@[simp]
def ofRestrictScalars (U : Subalgebra S A) (f : U →ₐ[S] B) : U.restrictScalars R →ₐ[R] B :=
  f.restrictScalars R

Restriction of scalars for algebra homomorphisms on subalgebras

Informal description

Given an $S$-subalgebra $U$ of $A$ and an $S$-algebra homomorphism $f: U \to_{\text{Alg}[S]} B$, this constructs the corresponding $R$-algebra homomorphism $U_{\text{restrictScalars } R} \to_{\text{Alg}[R]} B$ by restricting the scalars of $f$ from $S$ to $R$.

Subalgebra.range_isScalarTower_toAlgHom theorem

 [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) :
  LinearMap.range (IsScalarTower.toAlgHom R S A) = Subalgebra.toSubmodule S

Full source

@[simp]
lemma range_isScalarTower_toAlgHom [CommSemiring R] [CommSemiring A]
    [Algebra R A] (S : Subalgebra R A) :
    LinearMap.range (IsScalarTower.toAlgHom R S A) = Subalgebra.toSubmodule S := by
  ext
  simp only [← Submodule.range_subtype (Subalgebra.toSubmodule S), LinearMap.mem_range,
    IsScalarTower.coe_toAlgHom', Subalgebra.mem_toSubmodule]
  rfl

Range of Tower Algebra Homomorphism Equals Submodule

Informal description

Let $R$ be a commutative semiring and $A$ a commutative semiring with an $R$-algebra structure. For any $R$-subalgebra $S$ of $A$, the range of the canonical $R$-algebra homomorphism $\text{IsScalarTower.toAlgHom} \colon R \to S \to A$ is equal to the underlying $R$-submodule of $S$.

IsScalarTower.adjoin_range_toAlgHom theorem

(t : Set A) : (Algebra.adjoin (toAlgHom R S A).range t).restrictScalars R = (Algebra.adjoin S t).restrictScalars R

Full source

theorem adjoin_range_toAlgHom (t : Set A) :
    (Algebra.adjoin (toAlgHom R S A).range t).restrictScalars R =
      (Algebra.adjoin S t).restrictScalars R :=
  Subalgebra.ext fun z ↦
    show z ∈ Subsemiring.closure (Set.range (algebraMap (toAlgHom R S A).range A) ∪ t : Set A)z ∈ Subsemiring.closure (Set.range (algebraMap (toAlgHom R S A).range A) ∪ t : Set A) ↔
         z ∈ Subsemiring.closure (Set.range (algebraMap S A) ∪ t : Set A) by
      suffices Set.range (algebraMap (toAlgHom R S A).range A) = Set.range (algebraMap S A) by
        rw [this]
      ext z
      exact ⟨fun ⟨⟨_, y, h1⟩, h2⟩ ↦ ⟨y, h2 ▸ h1⟩, fun ⟨y, hy⟩ ↦ ⟨⟨z, y, hy⟩, rfl⟩⟩

Equality of Restricted Scalar Adjoints in Algebra Tower

Informal description

Let $R$, $S$, and $A$ be commutative semirings forming an algebra tower $A/S/R$ (with compatible scalar multiplications). For any subset $t \subseteq A$, the $R$-subalgebra obtained by restricting scalars from $S$ to $R$ in the algebra generated by $t$ over the range of the canonical algebra homomorphism $S \to A$ is equal to the $R$-subalgebra obtained by restricting scalars from $S$ to $R$ in the algebra generated by $t$ over $S$. In symbols: $$(\text{Algebra.adjoin } (\text{toAlgHom } R S A).\text{range } t).\text{restrictScalars } R = (\text{Algebra.adjoin } S t).\text{restrictScalars } R$$