mathlib documentation

algebra.algebra.tower

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

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

source
def algebra.lsmul (R : Type u) {A : Type w} (M : Type v₁) [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] :
A →ₐ[R] module.End R M

The R-algebra morphism A → End (M) corresponding to the representation of the algebra A on the R-module M.

This is a stronger version of distrib_mul_action.to_linear_map, and could also have been called algebra.to_module_End.

Equations
source
@[simp]
theorem algebra.lsmul_coe (R : Type u) {A : Type w} (M : Type v₁) [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] (a : A) :
⇑(⇑(algebra.lsmul R M) a) = has_smul.smul a
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
theorem is_scalar_tower.algebra_map_smul {R : Type u} (A : Type w) {M : Type v₁} [comm_semiring R] [semiring A] [algebra R A] [has_smul R M] [mul_action A M] [is_scalar_tower R A M] (r : R) (x : M) :
⇑(algebra_map R A) r • x = r • x
source
theorem is_scalar_tower.of_algebra_map_eq {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] (h : ∀ (x : R), ⇑(algebra_map R A) x = ⇑(algebra_map S A) (⇑(algebra_map R S) x)) :
is_scalar_tower R S A
source
theorem is_scalar_tower.of_algebra_map_eq' {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] (h : algebra_map R A = (algebra_map S A).comp (algebra_map R S)) :
is_scalar_tower R S A

See note [partially-applied ext lemmas].

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
theorem is_scalar_tower.algebra_map_eq (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] :
algebra_map R A = (algebra_map S A).comp (algebra_map R S)
source
theorem is_scalar_tower.algebra_map_apply (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] (x : R) :
⇑(algebra_map R A) x = ⇑(algebra_map S A) (⇑(algebra_map R S) 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] [algebra R A] [is_scalar_tower R S A] (S₀ : subalgebra R S) :
is_scalar_tower R ↥S₀ A
source
@[ext]
theorem is_scalar_tower.algebra.ext {S : Type u} {A : Type v} [comm_semiring S] [semiring A] (h1 h2 : algebra S A) (h : ∀ (r : S) (x : A), r • x = r • x) :
h1 = h2
source
def is_scalar_tower.to_alg_hom (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 →ₐ[R] A

In a tower, the canonical map from the middle element to the top element is an algebra homomorphism over the bottom element.

Equations
source
theorem is_scalar_tower.to_alg_hom_apply (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] (y : S) :
⇑(is_scalar_tower.to_alg_hom R S A) y = ⇑(algebra_map S A) y
source
@[simp]
theorem is_scalar_tower.coe_to_alg_hom (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] :
↑(is_scalar_tower.to_alg_hom R S A) = algebra_map S A
source
@[simp]
theorem is_scalar_tower.coe_to_alg_hom' (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] :
⇑(is_scalar_tower.to_alg_hom R S A) = ⇑(algebra_map S A)
source
@[simp]
theorem alg_hom.map_algebra_map {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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A →ₐ[S] B) (r : R) :
⇑f (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
source
@[simp]
theorem alg_hom.comp_algebra_map_of_tower (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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A →ₐ[S] B) :
↑f.comp (algebra_map R A) = algebra_map R B
source
@[protected, instance]
def is_scalar_tower.subsemiring {S : Type v} {A : Type w} [comm_semiring S] [semiring A] [algebra S A] (U : subsemiring S) :
is_scalar_tower ↥U S A
source
@[protected, nolint, instance]
def is_scalar_tower.of_ring_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
is_scalar_tower R A B
source
def alg_hom.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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A →ₐ[S] B) :
A →ₐ[R] B

R ⟶ S induces S-Alg ⥤ R-Alg

Equations
source
theorem alg_hom.restrict_scalars_apply (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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A →ₐ[S] B) (x : A) :
⇑(alg_hom.restrict_scalars R f) x = ⇑f x
source
@[simp]
theorem alg_hom.coe_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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A →ₐ[S] B) :
↑(alg_hom.restrict_scalars R f) = ↑f
source
@[simp]
theorem alg_hom.coe_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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A →ₐ[S] B) :
⇑(alg_hom.restrict_scalars R f) = ⇑f
source
theorem alg_hom.restrict_scalars_injective (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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] :
function.injective (alg_hom.restrict_scalars R)
source
def alg_equiv.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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A ≃ₐ[S] B) :
A ≃ₐ[R] B

R ⟶ S induces S-Alg ⥤ R-Alg

Equations
source
theorem alg_equiv.restrict_scalars_apply (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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A ≃ₐ[S] B) (x : A) :
⇑(alg_equiv.restrict_scalars R f) x = ⇑f x
source
@[simp]
theorem alg_equiv.coe_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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A ≃ₐ[S] B) :
↑(alg_equiv.restrict_scalars R f) = ↑f
source
@[simp]
theorem alg_equiv.coe_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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (f : A ≃ₐ[S] B) :
⇑(alg_equiv.restrict_scalars R f) = ⇑f
source
theorem alg_equiv.restrict_scalars_injective (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 S B] [algebra R A] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] :
function.injective (alg_equiv.restrict_scalars R)
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
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.restrict_scalars R U).to_submodule = submodule.restrict_scalars R U.to_submodule
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
source
theorem algebra.span_restrict_scalars_eq_span_of_surjective {R : Type u} {A : Type w} {M : Type v₁} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] (h : function.surjective ⇑(algebra_map R A)) (s : set M) :
submodule.restrict_scalars R (submodule.span A s) = submodule.span R s
source
theorem algebra.coe_span_eq_span_of_surjective {R : Type u} {A : Type w} {M : Type v₁} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] (h : function.surjective ⇑(algebra_map R A)) (s : set M) :
↑(submodule.span A s) = ↑(submodule.span R s)
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)
source
theorem submodule.smul_mem_span_smul_of_mem {R : Type u} {S : Type v} {A : Type w} [semiring R] [semiring S] [add_comm_monoid A] [module R S] [module S A] [module R A] [is_scalar_tower R S A] {s : set S} {t : set A} {k : S} (hks : k ∈ submodule.span R s) {x : A} (hx : x ∈ t) :
k • x ∈ submodule.span R (s • t)
source
theorem submodule.smul_mem_span_smul {R : Type u} {S : Type v} {A : Type w} [semiring R] [semiring S] [add_comm_monoid A] [module R S] [module S A] [module R A] [is_scalar_tower R S A] [smul_comm_class R S A] {s : set S} (hs : submodule.span R s = ⊤) {t : set A} {k : S} {x : A} (hx : x ∈ submodule.span R t) :
k • x ∈ submodule.span R (s • t)
source
theorem submodule.smul_mem_span_smul' {R : Type u} {S : Type v} {A : Type w} [semiring R] [semiring S] [add_comm_monoid A] [module R S] [module S A] [module R A] [is_scalar_tower R S A] [smul_comm_class R S A] {s : set S} (hs : submodule.span R s = ⊤) {t : set A} {k : S} {x : A} (hx : x ∈ submodule.span R (s • t)) :
k • x ∈ submodule.span R (s • t)
source
theorem submodule.span_smul {R : Type u} {S : Type v} {A : Type w} [semiring R] [semiring S] [add_comm_monoid A] [module R S] [module S A] [module R A] [is_scalar_tower R S A] [smul_comm_class R S A] {s : set S} (hs : submodule.span R s = ⊤) (t : set A) :
submodule.span R (s • t) = submodule.restrict_scalars R (submodule.span S t)
source
theorem submodule.span_algebra_map_image {R : Type u} {S : Type v} [comm_semiring R] [semiring S] [algebra R S] (a : set R) :
submodule.span R (⇑(algebra_map R S) '' a) = submodule.map (algebra.linear_map R S) (submodule.span R a)

A variant of submodule.span_image for algebra_map.

source
theorem submodule.span_algebra_map_image_of_tower {R : Type u} [comm_semiring R] {S : Type u_1} {T : Type u_2} [comm_semiring S] [semiring T] [module R S] [is_scalar_tower R S S] [algebra R T] [algebra S T] [is_scalar_tower R S T] (a : set S) :
submodule.span R (⇑(algebra_map S T) '' a) = submodule.map (linear_map.restrict_scalars R (algebra.linear_map S T)) (submodule.span R a)
source
theorem submodule.map_mem_span_algebra_map_image {R : Type u} [comm_semiring R] {S : Type u_1} {T : Type u_2} [comm_semiring S] [semiring T] [algebra R S] [algebra R T] [algebra S T] [is_scalar_tower R S T] (x : S) (a : set S) (hx : x ∈ submodule.span R a) :
⇑(algebra_map S T) x ∈ submodule.span R (⇑(algebra_map S T) '' a)
source
theorem algebra.lsmul_injective (R : Type u) (A : Type w) (M : Type v₁) [comm_semiring R] [semiring A] [algebra R A] [add_comm_group M] [module A M] [module R M] [is_scalar_tower R A M] [no_zero_smul_divisors A M] {x : A} (hx : x ≠ 0) :
function.injective ⇑(⇑(algebra.lsmul R M) x)