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.

source

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

A →ₐ[R] Module.End 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

Algebra.lsmul R B M = { toFun := DistribMulAction.toLinearMap B M, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

@[simp]

theorem Algebra.lsmul_coe (R : Type u) {A : Type w} (B : Type u₁) (M : Type v₁) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (a : A) :

⇑((Algebra.lsmul R B M) a) = fun (x : M) => a • x

source

theorem IsScalarTower.algebraMap_smul {R : Type u} (A : Type w) {M : Type v₁} [CommSemiring R] [Semiring A] [Algebra R A] [MulAction A M] [SMul R M] [IsScalarTower R A M] (r : R) (x : M) :

(algebraMap R A) r • x = r • x

source

theorem IsScalarTower.of_algebraMap_smul {R : Type u} {A : Type w} {M : Type v₁} [CommSemiring R] [Semiring A] [Algebra R A] [MulAction A M] [SMul R M] (h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x) :

IsScalarTower R A M

source

theorem IsScalarTower.of_compHom (R : Type u) (A : Type w) (M : Type v₁) [CommSemiring R] [Semiring A] [Algebra R A] [MulAction A M] :

IsScalarTower R A M

source

theorem IsScalarTower.of_algebraMap_eq {R : Type u} {S : Type v} {A : Type w} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] (h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)) :

IsScalarTower R S A

source

theorem IsScalarTower.of_algebraMap_eq' {R : Type u} {S : Type v} {A : Type w} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] (h : algebraMap R A = (algebraMap S A).comp (algebraMap R S)) :

IsScalarTower R S A

See note [partially-applied ext lemmas].

source

theorem IsScalarTower.algebraMap_eq (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] :

algebraMap R A = (algebraMap S A).comp (algebraMap R S)

source

theorem IsScalarTower.algebraMap_apply (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (x : R) :

(algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)

source

theorem IsScalarTower.Algebra.ext {S : Type u} {A : Type v} [CommSemiring S] [Semiring A] (h1 h2 : Algebra S A) (h : ∀ (r : S) (x : A), (let_fun I := h1; r • x) = r • x) :

h1 = h2

source

def IsScalarTower.toAlgHom (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower 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

IsScalarTower.toAlgHom R S A = { toRingHom := algebraMap S A, commutes' := ⋯ }

Instances For

source

theorem IsScalarTower.toAlgHom_apply (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (y : S) :

(IsScalarTower.toAlgHom R S A) y = (algebraMap S A) y

source

@[simp]

theorem IsScalarTower.coe_toAlgHom (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] :

↑(IsScalarTower.toAlgHom R S A) = algebraMap S A

source

@[simp]

theorem IsScalarTower.coe_toAlgHom' (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] :

⇑(IsScalarTower.toAlgHom R S A) = ⇑(algebraMap S A)

source

@[simp]

theorem AlgHom.map_algebraMap {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) (r : R) :

f ((algebraMap R A) r) = (algebraMap R B) r

source

@[simp]

theorem AlgHom.comp_algebraMap_of_tower (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) :

(↑f).comp (algebraMap R A) = algebraMap R B

source

@[instance 999]

instance IsScalarTower.subsemiring {S : Type v} {A : Type w} [CommSemiring S] [Semiring A] [Algebra S A] (U : Subsemiring S) :

IsScalarTower (↥U) S A

Equations

⋯ = ⋯

source

@[instance 999]

instance IsScalarTower.of_algHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

IsScalarTower R A B

Equations

⋯ = ⋯

source

def AlgHom.restrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) :

A →ₐ[R] B

R ⟶ S induces S-Alg ⥤ R-Alg

Equations

AlgHom.restrictScalars R f = { toRingHom := ↑f, commutes' := ⋯ }

Instances For

source

theorem AlgHom.restrictScalars_apply (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) (x : A) :

(AlgHom.restrictScalars R f) x = f x

source

@[simp]

theorem AlgHom.coe_restrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) :

↑(AlgHom.restrictScalars R f) = ↑f

source

@[simp]

theorem AlgHom.coe_restrictScalars' (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) :

⇑(AlgHom.restrictScalars R f) = ⇑f

source

theorem AlgHom.restrictScalars_injective (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] :

Function.Injective (AlgHom.restrictScalars R)

source

def AlgEquiv.restrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A ≃ₐ[S] B) :

A ≃ₐ[R] B

R ⟶ S induces S-Alg ⥤ R-Alg

Equations

AlgEquiv.restrictScalars R f = { toEquiv := (↑f).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

theorem AlgEquiv.restrictScalars_apply (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A ≃ₐ[S] B) (x : A) :

(AlgEquiv.restrictScalars R f) x = f x

source

@[simp]

theorem AlgEquiv.coe_restrictScalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A ≃ₐ[S] B) :

↑(AlgEquiv.restrictScalars R f) = ↑f

source

@[simp]

theorem AlgEquiv.coe_restrictScalars' (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A ≃ₐ[S] B) :

⇑(AlgEquiv.restrictScalars R f) = ⇑f

source

theorem AlgEquiv.restrictScalars_injective (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] :

Function.Injective (AlgEquiv.restrictScalars R)

source

theorem Submodule.restrictScalars_span (R : Type u) (A : Type w) {M : Type v₁} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (hsur : Function.Surjective ⇑(algebraMap R A)) (X : Set M) :

Submodule.restrictScalars R (Submodule.span A X) = Submodule.span R X

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.

source

theorem Submodule.coe_span_eq_span_of_surjective (R : Type u) (A : Type w) {M : Type v₁} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (h : Function.Surjective ⇑(algebraMap R A)) (s : Set M) :

↑(Submodule.span A s) = ↑(Submodule.span R s)

source

theorem Submodule.smul_mem_span_smul_of_mem {R : Type u} {S : Type v} {A : Type w} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower 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.span_smul_of_span_eq_top {R : Type u} {S : Type v} {A : Type w} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {s : Set S} (hs : Submodule.span R s = ⊤) (t : Set A) :

Submodule.span R (s • t) = Submodule.restrictScalars R (Submodule.span S t)

source

theorem Submodule.smul_mem_span_smul' {R : Type u} {S : Type v} {A : Type w} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower 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.smul_mem_span_smul {R : Type u} {S : Type v} {A : Type w} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower 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.span_algebraMap_image {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (a : Set R) :

Submodule.span R (⇑(algebraMap R S) '' a) = Submodule.map (Algebra.linearMap R S) (Submodule.span R a)

A variant of Submodule.span_image for algebraMap.

source

theorem Submodule.span_algebraMap_image_of_tower {R : Type u} [CommSemiring R] {S : Type u_1} {T : Type u_2} [CommSemiring S] [Semiring T] [Module R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (a : Set S) :

Submodule.span R (⇑(algebraMap S T) '' a) = Submodule.map (↑R (Algebra.linearMap S T)) (Submodule.span R a)

source

theorem Submodule.map_mem_span_algebraMap_image {R : Type u} [CommSemiring R] {S : Type u_1} {T : Type u_2} [CommSemiring S] [Semiring T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (x : S) (a : Set S) (hx : x ∈ Submodule.span R a) :

(algebraMap S T) x ∈ Submodule.span R (⇑(algebraMap S T) '' a)

source

theorem Algebra.lsmul_injective (R : Type u) (A : Type w) (B : Type u₁) (M : Type v₁) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommGroup M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [NoZeroSMulDivisors A M] {x : A} (hx : x ≠ 0) :

Function.Injective ⇑((Algebra.lsmul R B M) x)

Documentation

Mathlib.Algebra.Algebra.Tower

Towers of algebras #