# mathlibdocumentation

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₁) [semiring A] [ A] [ M] [ M] [ M] :

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

This is a stronger version of distrib_mul_action.to_linear_map, and could also have been called algebra.to_module_End.

Equations
@[simp]
theorem algebra.lsmul_coe (R : Type u) {A : Type w} (M : Type v₁) [semiring A] [ A] [ M] [ M] [ M] (a : A) :
( M) a) =
theorem algebra.lmul_algebra_map (R : Type u) {A : Type w} [semiring A] [ A] (x : R) :
A) ( A) x) = A) x
theorem is_scalar_tower.algebra_map_smul {R : Type u} (A : Type w) {M : Type v₁} [semiring A] [ A] [ M] [ M] [ M] (r : R) (x : M) :
A) r x = r x
theorem is_scalar_tower.of_algebra_map_eq {R : Type u} {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] (h : ∀ (x : R), A) x = A) ( S) x)) :
A
theorem is_scalar_tower.of_algebra_map_eq' {R : Type u} {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] (h : A = A).comp S)) :
A
@[protected, instance]
def is_scalar_tower.subalgebra (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] (S₀ : S) :
S A
theorem is_scalar_tower.algebra_map_eq (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] :
A = A).comp S)
theorem is_scalar_tower.algebra_map_apply (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] (x : R) :
A) x = A) ( S) x)
@[protected, instance]
def is_scalar_tower.subalgebra' (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] (S₀ : S) :
S₀ A
@[ext]
theorem is_scalar_tower.algebra.ext {S : Type u} {A : Type v} [semiring A] (h1 h2 : 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) [semiring A] [ S] [ A] [ A] [ 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) [semiring A] [ S] [ A] [ A] [ A] (y : S) :
A) y = A) y
@[simp]
theorem is_scalar_tower.coe_to_alg_hom (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] :
A) = A
@[simp]
theorem is_scalar_tower.coe_to_alg_hom' (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] :
A) = A)
@[simp]
theorem alg_hom.map_algebra_map {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] (f : A →ₐ[S] B) (r : R) :
f ( A) r) = B) r
@[simp]
theorem alg_hom.comp_algebra_map_of_tower (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] (f : A →ₐ[S] B) :
f.comp A) = B
@[protected, instance]
def is_scalar_tower.subsemiring {S : Type v} {A : Type w} [semiring A] [ A] (U : subsemiring S) :
A
@[protected, nolint, instance]
def is_scalar_tower.of_ring_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [ A] [ B] (f : A →ₐ[R] B) :
B
def alg_hom.restrict_scalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ 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₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] (f : A →ₐ[S] B) (x : A) :
x = f x
@[simp]
theorem alg_hom.coe_restrict_scalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] (f : A →ₐ[S] B) :
= f
@[simp]
theorem alg_hom.coe_restrict_scalars' (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] (f : A →ₐ[S] B) :
= f
theorem alg_hom.restrict_scalars_injective (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] :
def alg_equiv.restrict_scalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ 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₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] (f : A ≃ₐ[S] B) (x : A) :
x = f x
@[simp]
theorem alg_equiv.coe_restrict_scalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] (f : A ≃ₐ[S] B) :
@[simp]
theorem alg_equiv.coe_restrict_scalars' (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] (f : A ≃ₐ[S] B) :
theorem alg_equiv.restrict_scalars_injective (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] :
def subalgebra.restrict_scalars (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] (U : A) :
A

Given a tower A / ↥U / S / R of algebras, where U is an S-subalgebra of A, reinterpret U as an R-subalgebra of A.

Equations
@[simp]
theorem subalgebra.coe_restrict_scalars (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] {U : A} :
@[simp]
theorem subalgebra.restrict_scalars_top (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] :
@[simp]
theorem subalgebra.restrict_scalars_to_submodule (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] {U : A} :
@[simp]
theorem subalgebra.mem_restrict_scalars (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] {U : A} {x : A} :
x U
theorem subalgebra.restrict_scalars_injective (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] :
@[simp]
def subalgebra.of_restrict_scalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ A] [ B] [ B] [ A] [ B] (U : A) (f : U →ₐ[S] B) :

Produces an R-algebra map from U.restrict_scalars R given an S-algebra map from U.

This is a special case of alg_hom.restrict_scalars that can be helpful in elaboration.

Equations
theorem algebra.span_restrict_scalars_eq_span_of_surjective {R : Type u} {A : Type w} {M : Type v₁} [semiring A] [ A] [ M] [ M] [ M] (h : function.surjective A)) (s : set M) :
theorem algebra.coe_span_eq_span_of_surjective {R : Type u} {A : Type w} {M : Type v₁} [semiring A] [ A] [ M] [ M] [ M] (h : function.surjective A)) (s : set M) :
s) = s)
theorem is_scalar_tower.adjoin_range_to_alg_hom (R : Type u) (S : Type v) (A : Type w) [ S] [ A] [ A] [ A] (t : set A) :
theorem submodule.smul_mem_span_smul_of_mem {R : Type u} {S : Type v} {A : Type w} [semiring R] [semiring S] [ S] [ A] [ A] [ A] {s : set S} {t : set A} {k : S} (hks : k ) {x : A} (hx : x t) :
k x (s t)
theorem submodule.smul_mem_span_smul {R : Type u} {S : Type v} {A : Type w} [semiring R] [semiring S] [ S] [ A] [ A] [ A] [ A] {s : set S} (hs : = ) {t : set A} {k : S} {x : A} (hx : x ) :
k x (s t)
theorem submodule.smul_mem_span_smul' {R : Type u} {S : Type v} {A : Type w} [semiring R] [semiring S] [ S] [ A] [ A] [ A] [ A] {s : set S} (hs : = ) {t : set A} {k : S} {x : A} (hx : x (s t)) :
k x (s t)
theorem submodule.span_smul {R : Type u} {S : Type v} {A : Type w} [semiring R] [semiring S] [ S] [ A] [ A] [ A] [ A] {s : set S} (hs : = ) (t : set A) :
(s t) =
theorem submodule.span_algebra_map_image {R : Type u} {S : Type v} [semiring S] [ S] (a : set R) :
( S) '' a) = a)

A variant of submodule.span_image for algebra_map.

theorem submodule.span_algebra_map_image_of_tower {R : Type u} {S : Type u_1} {T : Type u_2} [semiring T] [ S] [ S] [ T] [ T] [ T] (a : set S) :
( T) '' a) = a)
theorem submodule.map_mem_span_algebra_map_image {R : Type u} {S : Type u_1} {T : Type u_2} [semiring T] [ S] [ T] [ T] [ T] (x : S) (a : set S) (hx : x ) :
T) x ( T) '' a)
theorem algebra.lsmul_injective (R : Type u) (A : Type w) (M : Type v₁) [semiring A] [ A] [ M] [ M] [ M] {x : A} (hx : x 0) :