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

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

def Algebra.lsmul (R : Type u) {A : Type w} (B : Type u₁) (M : Type v₁) [] [] [] [Algebra R A] [Algebra R B] [] [Module R M] [Module A M] [Module B M] [] [] [] :

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

This is a stronger version of DistribMulAction.toLinearMap, and could also have been called Algebra.toModuleEnd.

The typeclasses correspond to the situation where the types act on each other as

R ----→ B
| ⟍     |
|   ⟍   |
↓     ↘ ↓
A ----→ M


where the diagram commutes, the action by R commutes with everything, and the action by A and B on M commute.

Typically this is most useful with B = R as Algebra.lsmul R R A : A →ₐ[R] Module.End R M. However this can be used to get the fact that left-multiplication by A is right A-linear, and vice versa, as

example : A →ₐ[R] Module.End Aᵐᵒᵖ A := Algebra.lsmul R Aᵐᵒᵖ A
example : Aᵐᵒᵖ →ₐ[R] Module.End A A := Algebra.lsmul R A A


respectively; though LinearMap.mulLeft and LinearMap.mulRight can also be used here.

Equations
• = { toFun := , map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem Algebra.lsmul_coe (R : Type u) {A : Type w} (B : Type u₁) (M : Type v₁) [] [] [] [Algebra R A] [Algebra R B] [] [Module R M] [Module A M] [Module B M] [] [] [] (a : A) :
(() a) = fun (x : M) => a x
theorem IsScalarTower.algebraMap_smul {R : Type u} (A : Type w) {M : Type v₁} [] [] [Algebra R A] [] [SMul R M] [] (r : R) (x : M) :
() r x = r x
theorem IsScalarTower.of_algebraMap_smul {R : Type u} {A : Type w} {M : Type v₁} [] [] [Algebra R A] [] [SMul R M] (h : ∀ (r : R) (x : M), () r x = r x) :
theorem IsScalarTower.of_compHom (R : Type u) (A : Type w) (M : Type v₁) [] [] [Algebra R A] [] :
theorem IsScalarTower.of_algebraMap_eq {R : Type u} {S : Type v} {A : Type w} [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] (h : ∀ (x : R), () x = () (() x)) :
theorem IsScalarTower.of_algebraMap_eq' {R : Type u} {S : Type v} {A : Type w} [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] (h : = ().comp ()) :

See note [partially-applied ext lemmas].

theorem IsScalarTower.algebraMap_eq (R : Type u) (S : Type v) (A : Type w) [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] :
= ().comp ()
theorem IsScalarTower.algebraMap_apply (R : Type u) (S : Type v) (A : Type w) [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] (x : R) :
() x = () (() x)
theorem IsScalarTower.Algebra.ext {S : Type u} {A : Type v} [] [] (h1 : Algebra S A) (h2 : Algebra S A) (h : ∀ (r : S) (x : A), (let_fun I := h1; r x) = r x) :
h1 = h2
def IsScalarTower.toAlgHom (R : Type u) (S : Type v) (A : Type w) [] [] [] [Algebra R S] [Algebra S A] [Algebra 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
• = let __src := ; { toRingHom := __src, commutes' := }
Instances For
theorem IsScalarTower.toAlgHom_apply (R : Type u) (S : Type v) (A : Type w) [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] (y : S) :
() y = () y
@[simp]
theorem IsScalarTower.coe_toAlgHom (R : Type u) (S : Type v) (A : Type w) [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] :
() =
@[simp]
theorem IsScalarTower.coe_toAlgHom' (R : Type u) (S : Type v) (A : Type w) [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] :
() = ()
@[simp]
theorem AlgHom.map_algebraMap {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A →ₐ[S] B) (r : R) :
f (() r) = () r
@[simp]
theorem AlgHom.comp_algebraMap_of_tower (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A →ₐ[S] B) :
(f).comp () =
@[instance 999]
instance IsScalarTower.subsemiring {S : Type v} {A : Type w} [] [] [Algebra S A] (U : ) :
IsScalarTower (U) S A
Equations
• =
@[instance 999]
instance IsScalarTower.of_algHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
Equations
• =
def AlgHom.restrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A →ₐ[S] B) :

R ⟶ S induces S-Alg ⥤ R-Alg

Equations
• = let __src := f; { toRingHom := __src, commutes' := }
Instances For
theorem AlgHom.restrictScalars_apply (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A →ₐ[S] B) (x : A) :
() x = f x
@[simp]
theorem AlgHom.coe_restrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A →ₐ[S] B) :
() = f
@[simp]
theorem AlgHom.coe_restrictScalars' (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A →ₐ[S] B) :
() = f
theorem AlgHom.restrictScalars_injective (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] :
def AlgEquiv.restrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A ≃ₐ[S] B) :

R ⟶ S induces S-Alg ⥤ R-Alg

Equations
• = let __src := f; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
theorem AlgEquiv.restrictScalars_apply (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A ≃ₐ[S] B) (x : A) :
() x = f x
@[simp]
theorem AlgEquiv.coe_restrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A ≃ₐ[S] B) :
() = f
@[simp]
theorem AlgEquiv.coe_restrictScalars' (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] (f : A ≃ₐ[S] B) :
() = f
theorem AlgEquiv.restrictScalars_injective (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [] [] [] [] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [] [] :
theorem Submodule.restrictScalars_span (R : Type u) (A : Type w) {M : Type v₁} [] [] [Algebra R A] [] [Module R M] [Module A M] [] (hsur : ) (X : Set M) :

If A is an R-algebra such that the induced morphism R →+* A is surjective, then the R-module generated by a set X equals the A-module generated by X.

theorem Submodule.coe_span_eq_span_of_surjective (R : Type u) (A : Type w) {M : Type v₁} [] [] [Algebra R A] [] [Module R M] [Module A M] [] (h : ) (s : Set M) :
() = ()
theorem Submodule.smul_mem_span_smul_of_mem {R : Type u} {S : Type v} {A : Type w} [] [] [] [Module R S] [Module S A] [Module R A] [] {s : Set S} {t : Set A} {k : S} (hks : k ) {x : A} (hx : x t) :
theorem Submodule.span_smul_of_span_eq_top {R : Type u} {S : Type v} {A : Type w} [] [] [] [Module R S] [Module S A] [Module R A] [] {s : Set S} (hs : = ) (t : Set A) :
theorem Submodule.smul_mem_span_smul' {R : Type u} {S : Type v} {A : Type w} [] [] [] [Module R S] [Module S A] [Module R A] [] {s : Set S} (hs : = ) {t : Set A} {k : S} {x : A} (hx : x Submodule.span R (s t)) :
theorem Submodule.smul_mem_span_smul {R : Type u} {S : Type v} {A : Type w} [] [] [] [Module R S] [Module S A] [Module R A] [] {s : Set S} (hs : = ) {t : Set A} {k : S} {x : A} (hx : x ) :
theorem Submodule.span_algebraMap_image {R : Type u} {S : Type v} [] [] [Algebra R S] (a : Set R) :
Submodule.span R (() '' a) = Submodule.map () ()

A variant of Submodule.span_image for algebraMap.

theorem Submodule.span_algebraMap_image_of_tower {R : Type u} [] {S : Type u_1} {T : Type u_2} [] [] [Module R S] [Algebra R T] [Algebra S T] [] (a : Set S) :
Submodule.span R (() '' a) = Submodule.map (R ()) ()
theorem Submodule.map_mem_span_algebraMap_image {R : Type u} [] {S : Type u_1} {T : Type u_2} [] [] [Algebra R S] [Algebra R T] [Algebra S T] [] (x : S) (a : Set S) (hx : x ) :
() x Submodule.span R (() '' a)
theorem Algebra.lsmul_injective (R : Type u) (A : Type w) (B : Type u₁) (M : Type v₁) [] [] [] [Algebra R A] [Algebra R B] [] [Module R M] [Module A M] [Module B M] [] [] [] [] {x : A} (hx : x 0) :