Subalgebras in towers of algebras

In this file we prove facts about subalgebras in towers of algebras.

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 latter 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} [CommSemiring R] [Semiring A] [Algebra R A] (x : R) : (lmul R A) ((algebraMap R A) x) = (lsmul R R A) x

instance IsScalarTower.subalgebra (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] (S₀ : Subalgebra R S) : IsScalarTower (↥S₀) S A

instance IsScalarTower.subalgebra' (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (S₀ : Subalgebra R S) : IsScalarTower R (↥S₀) A

def Subalgebra.restrictScalars (R : Type u) {S : Type v} {A : Type w} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (U : Subalgebra S A) : Subalgebra R A

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.

Equations

• Subalgebra.restrictScalars R U = { toSubsemiring := U.toSubsemiring, algebraMap_mem' := ⋯ }

@[simp]

theorem Subalgebra.coe_restrictScalars (R : Type u) {S : Type v} {A : Type w} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] {U : Subalgebra S A} : ↑(restrictScalars R U) = ↑U

@[simp]

theorem Subalgebra.restrictScalars_top (R : Type u) {S : Type v} {A : Type w} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] : restrictScalars R ⊤ = ⊤

@[simp]

theorem Subalgebra.restrictScalars_toSubmodule (R : Type u) {S : Type v} {A : Type w} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] {U : Subalgebra S A} : toSubmodule (restrictScalars R U) = Submodule.restrictScalars R (toSubmodule U)

@[simp]

theorem Subalgebra.mem_restrictScalars (R : Type u) {S : Type v} {A : Type w} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] {U : Subalgebra S A} {x : A} : x ∈ restrictScalars R U ↔ x ∈ U

theorem Subalgebra.restrictScalars_injective (R : Type u) {S : Type v} {A : Type w} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] : Function.Injective (restrictScalars R)

def Subalgebra.ofRestrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra R A] [Algebra S B] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (U : Subalgebra S A) (f : ↥U →ₐ[S] B) : ↥(restrictScalars R U) →ₐ[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.

Equations

• Subalgebra.ofRestrictScalars R U f = AlgHom.restrictScalars R f

@[simp]

theorem Subalgebra.restrictScalars_one (R : Type u) (A : Type w) [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) : Submodule.restrictScalars R 1 = toSubmodule S

theorem Subalgebra.codisjoint_one_iff (R : Type u) (A : Type w) [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) (I : Ideal A) : Codisjoint 1 (Submodule.restrictScalars (↥S) I) ↔ Codisjoint (toSubmodule S) (Submodule.restrictScalars R I)

theorem Subalgebra.disjoint_one_iff (R : Type u) (A : Type w) [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) (I : Ideal A) : Disjoint 1 (Submodule.restrictScalars (↥S) I) ↔ Disjoint (toSubmodule S) (Submodule.restrictScalars R I)

@[simp]

theorem Subalgebra.range_isScalarTower_toAlgHom (R : Type u) (A : Type w) [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) : (↑(IsScalarTower.toAlgHom R (↥S) A)).range = toSubmodule S

theorem IsScalarTower.adjoin_range_toAlgHom (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (t : Set A) : Subalgebra.restrictScalars R (Algebra.adjoin (↥(toAlgHom R S A).range) t) = Subalgebra.restrictScalars R (Algebra.adjoin S t)