Subalgebras in towers of algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 is_scalar_tower R S A, the later asserting the compatibility condition (r • s) • a = r • (s • a).

Main results #

is_scalar_tower.subalgebra: if A/S/R is a tower and S₀ is a subalgebra between S and R, then A/S/S₀ is a tower
is_scalar_tower.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.restrict_scalars: turn an S-subalgebra of A into an R-subalgebra of A, given that A/S/R is a tower

source

theorem algebra.lmul_algebra_map (R : Type u) {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (x : R) :

⇑(algebra.lmul R A) (⇑(algebra_map R A) x) = ⇑(algebra.lsmul R A) x

source

@[protected, instance]

def is_scalar_tower.subalgebra (R : Type u) (S : Type v) (A : Type w) [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] (S₀ : subalgebra R S) :

is_scalar_tower ↥S₀ S A

source

@[protected, instance]

def is_scalar_tower.subalgebra' (R : Type u) (S : Type v) (A : Type w) [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (S₀ : subalgebra R S) :

is_scalar_tower R ↥S₀ A

source

def subalgebra.restrict_scalars (R : Type u) {S : Type v} {A : Type w} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower 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.restrict_scalars R U = {carrier := U.carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}

source

@[simp]

theorem subalgebra.coe_restrict_scalars (R : Type u) {S : Type v} {A : Type w} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] {U : subalgebra S A} :

↑(subalgebra.restrict_scalars R U) = ↑U

source

@[simp]

theorem subalgebra.restrict_scalars_top (R : Type u) {S : Type v} {A : Type w} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] :

subalgebra.restrict_scalars R ⊤ = ⊤

source

@[simp]

theorem subalgebra.restrict_scalars_to_submodule (R : Type u) {S : Type v} {A : Type w} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] {U : subalgebra S A} :

⇑subalgebra.to_submodule (subalgebra.restrict_scalars R U) = submodule.restrict_scalars R (⇑subalgebra.to_submodule U)

source

@[simp]

theorem subalgebra.mem_restrict_scalars (R : Type u) {S : Type v} {A : Type w} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] {U : subalgebra S A} {x : A} :

x ∈ subalgebra.restrict_scalars R U ↔ x ∈ U

source

theorem subalgebra.restrict_scalars_injective (R : Type u) {S : Type v} {A : Type w} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] :

function.injective (subalgebra.restrict_scalars R)

source

@[simp]

def subalgebra.of_restrict_scalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] [algebra R S] [algebra S A] [algebra R A] [algebra S B] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (U : subalgebra S A) (f : ↥U →ₐ[S] B) :

↥(subalgebra.restrict_scalars R U) →ₐ[R] B

Produces an R-algebra map from U.restrict_scalars R given an S-algebra map from U.

This is a special case of alg_hom.restrict_scalars that can be helpful in elaboration.

Equations

subalgebra.of_restrict_scalars R U f = alg_hom.restrict_scalars R f

source

theorem is_scalar_tower.adjoin_range_to_alg_hom (R : Type u) (S : Type v) (A : Type w) [comm_semiring R] [comm_semiring S] [comm_semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (t : set A) :

subalgebra.restrict_scalars R (algebra.adjoin ↥((is_scalar_tower.to_alg_hom R S A).range) t) = subalgebra.restrict_scalars R (algebra.adjoin S t)