# Documentation

Mathlib.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 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.

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 x_1 => x x_1) a
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_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 : = RingHom.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] [] :
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.

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) :
RingHom.comp (f) () =
instance IsScalarTower.subsemiring {S : Type v} {A : Type w} [] [] [Algebra S A] (U : ) :
IsScalarTower { x // x U } S A
instance IsScalarTower.of_ring_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
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

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

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.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.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.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.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) :
Function.Injective ↑(↑() x)