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.

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] :

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

Equations
@[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) :
@[simp]
theorem algebra.lmul_algebra_map (R : Type u) {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (x : R) :
theorem is_scalar_tower.algebra_map_smul {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] (r : R) (x : M) :
(algebra_map R A) r x = r x
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)) :
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)) :

See note [partially-applied ext lemmas].

@[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) :
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] :
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) :
@[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) :
@[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
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] :

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

Equations
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) :
@[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] :
@[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] :
@[instance]
def is_scalar_tower.subsemiring {S : Type v} {A : Type w} [comm_semiring S] [semiring A] [algebra S A] (U : subsemiring S) :
@[instance]
def is_scalar_tower.subring {S : Type u_1} {A : Type u_2} [comm_ring S] [ring A] [algebra S A] (U : set S) [is_subring U] :
@[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) :
@[instance]
def is_scalar_tower.rat (R : Type u) (S : Type v) [field R] [division_ring S] [algebra R S] [char_zero R] [char_zero S] :
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] (iSB : subalgebra S A) :

Given a scalar tower R, S, A of algebras, reinterpret an S-subalgebra of A an as an R-subalgebra.

Equations
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) :

R ⟶ S induces S-Alg ⥤ R-Alg

Equations
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) :
@[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) :
@[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) :
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) :

R ⟶ S induces S-Alg ⥤ R-Alg

Equations
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) :
@[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) :
@[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) :
def subalgebra.res (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) :

If A/S/R is a tower of algebras then the restriction of a S-subalgebra of A is an R-subalgebra of A.

Equations
@[simp]
theorem subalgebra.res_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] :
@[simp]
theorem subalgebra.mem_res (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} :
theorem subalgebra.res_inj (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 V : subalgebra S A} (H : subalgebra.res R U = subalgebra.res R V) :
U = V
def subalgebra.of_under {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [comm_semiring A] [semiring B] [algebra R A] [algebra R B] (S : subalgebra R A) (U : subalgebra S A) [algebra S B] [is_scalar_tower R S B] (f : U →ₐ[S] B) :

Produces a map from subalgebra.under.

Equations
theorem submodule.smul_mem_span_smul_of_mem {R : Type u} {S : Type v} {A : Type w} [comm_semiring R] [semiring S] [add_comm_monoid A] [algebra 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) :
theorem submodule.smul_mem_span_smul {R : Type u} {S : Type v} {A : Type w} [comm_semiring R] [semiring S] [add_comm_monoid A] [algebra R S] [module S A] [module R A] [is_scalar_tower R S A] {s : set S} (hs : submodule.span R s = ) {t : set A} {k : S} {x : A} (hx : x submodule.span R t) :
theorem submodule.smul_mem_span_smul' {R : Type u} {S : Type v} {A : Type w} [comm_semiring R] [semiring S] [add_comm_monoid A] [algebra R S] [module S A] [module R A] [is_scalar_tower 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)) :
theorem submodule.span_smul {R : Type u} {S : Type v} {A : Type w} [comm_semiring R] [semiring S] [add_comm_monoid A] [algebra R S] [module S A] [module R A] [is_scalar_tower R S A] {s : set S} (hs : submodule.span R s = ) (t : set A) :
theorem algebra.lsmul_injective (R : Type u) (A : Type w) (M : Type v₁) [comm_semiring R] [ring 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) :