# Documentation

Mathlib.Algebra.Algebra.Subalgebra.Tower

# 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
theorem Algebra.lmul_algebraMap (R : Type u) {A : Type w} [] [] [Algebra R A] (x : R) :
↑() (↑() x) = ↑() x
instance IsScalarTower.subalgebra (R : Type u) (S : Type v) (A : Type w) [] [] [] [Algebra R S] [Algebra S A] (S₀ : ) :
IsScalarTower { x // x S₀ } S A
instance IsScalarTower.subalgebra' (R : Type u) (S : Type v) (A : Type w) [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] (S₀ : ) :
IsScalarTower R { x // x S₀ } A
def Subalgebra.restrictScalars (R : Type u) {S : Type v} {A : Type w} [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] (U : ) :

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.

Instances For
@[simp]
theorem Subalgebra.coe_restrictScalars (R : Type u) {S : Type v} {A : Type w} [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] {U : } :
↑() = U
@[simp]
theorem Subalgebra.restrictScalars_top (R : Type u) {S : Type v} {A : Type w} [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] :
@[simp]
theorem Subalgebra.restrictScalars_toSubmodule (R : Type u) {S : Type v} {A : Type w} [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] {U : } :
Subalgebra.toSubmodule () = Submodule.restrictScalars R (Subalgebra.toSubmodule U)
@[simp]
theorem Subalgebra.mem_restrictScalars (R : Type u) {S : Type v} {A : Type w} [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] {U : } {x : A} :
x U
theorem Subalgebra.restrictScalars_injective (R : Type u) {S : Type v} {A : Type w} [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] :
def Subalgebra.ofRestrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [Algebra S B] [Algebra R B] [] [] (U : ) (f : { x // x U } →ₐ[S] B) :
{ x // } →ₐ[R] B

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.

Instances For
@[simp]
theorem Subalgebra.range_isScalarTower_toAlgHom (R : Type u) (A : Type w) [] [] [Algebra R A] (S : ) :
LinearMap.range (IsScalarTower.toAlgHom R { x // x S } A) = Subalgebra.toSubmodule S
theorem IsScalarTower.adjoin_range_toAlgHom (R : Type u) (S : Type v) (A : Type w) [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] (t : Set A) :