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₁) [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

• One or more equations did not get rendered due to their size.

@[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 x_1 => x • x_1) a

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

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

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 = RingHom.comp (algebraMap S A) (algebraMap R S)) : IsScalarTower R S A

See note [partially-applied ext lemmas].

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 = RingHom.comp (algebraMap S A) (algebraMap R S)

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)

theorem IsScalarTower.Algebra.ext {S : Type u} {A : Type v} [CommSemiring S] [Semiring A] (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) [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

• One or more equations did not get rendered due to their size.

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

@[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

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

@[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

@[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) : RingHom.comp (↑f) (algebraMap R A) = algebraMap R B

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

Equations

• @IsScalarTower.subsemiring = @IsScalarTower.subsemiring.proof_1

instance IsScalarTower.of_ring_hom {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

• @IsScalarTower.of_ring_hom = @IsScalarTower.of_ring_hom.proof_1

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

• One or more equations did not get rendered due to their size.

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

@[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

@[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

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)

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

• One or more equations did not get rendered due to their size.

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

@[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

@[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

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)

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.

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)

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)

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] [SMulCommClass 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)

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] [SMulCommClass 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)

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] [SMulCommClass 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)

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.

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] [IsScalarTower R S 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)

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)

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)