Towers of algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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₁)
[comm_semiring R]
[semiring A]
[algebra R A]
[add_comm_monoid M]
[module R M]
[module A M]
[is_scalar_tower R A M] :
A →ₐ[R] module.End R 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
- algebra.lsmul R M = {to_fun := distrib_mul_action.to_linear_map R M is_scalar_tower.to_smul_comm_class', map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
@[simp]
theorem
algebra.lsmul_coe
(R : Type u)
{A : Type w}
(M : Type v₁)
[comm_semiring R]
[semiring A]
[algebra R A]
[add_comm_monoid M]
[module R M]
[module A M]
[is_scalar_tower R A M]
(a : A) :
⇑(⇑(algebra.lsmul R M) a) = has_smul.smul a
theorem
is_scalar_tower.algebra_map_smul
{R : Type u}
(A : Type w)
{M : Type v₁}
[comm_semiring R]
[semiring A]
[algebra R A]
[has_smul R M]
[mul_action A M]
[is_scalar_tower R A M]
(r : R)
(x : M) :
⇑(algebra_map R A) r • x = r • x
theorem
is_scalar_tower.of_algebra_map_eq
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
(h : ∀ (x : R), ⇑(algebra_map R A) x = ⇑(algebra_map S A) (⇑(algebra_map R S) x)) :
is_scalar_tower R S A
theorem
is_scalar_tower.of_algebra_map_eq'
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
(h : algebra_map R A = (algebra_map S A).comp (algebra_map R S)) :
is_scalar_tower R S A
theorem
is_scalar_tower.algebra_map_eq
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A] :
algebra_map R A = (algebra_map S A).comp (algebra_map R S)
theorem
is_scalar_tower.algebra_map_apply
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A]
(x : R) :
⇑(algebra_map R A) x = ⇑(algebra_map S A) (⇑(algebra_map R S) x)
@[ext]
theorem
is_scalar_tower.algebra.ext
{S : Type u}
{A : Type v}
[comm_semiring S]
[semiring A]
(h1 h2 : algebra S 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)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A] :
In a tower, the canonical map from the middle element to the top element is an algebra homomorphism over the bottom element.
theorem
is_scalar_tower.to_alg_hom_apply
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A]
(y : S) :
⇑(is_scalar_tower.to_alg_hom R S A) y = ⇑(algebra_map S A) y
@[simp]
theorem
is_scalar_tower.coe_to_alg_hom
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A] :
↑(is_scalar_tower.to_alg_hom R S A) = algebra_map S A
@[simp]
theorem
is_scalar_tower.coe_to_alg_hom'
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A] :
⇑(is_scalar_tower.to_alg_hom R S A) = ⇑(algebra_map S A)
@[simp]
theorem
alg_hom.map_algebra_map
{R : Type u}
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A →ₐ[S] B)
(r : R) :
⇑f (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
@[simp]
theorem
alg_hom.comp_algebra_map_of_tower
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A →ₐ[S] B) :
↑f.comp (algebra_map R A) = algebra_map R B
@[protected, instance]
def
is_scalar_tower.subsemiring
{S : Type v}
{A : Type w}
[comm_semiring S]
[semiring A]
[algebra S A]
(U : subsemiring S) :
is_scalar_tower ↥U S A
@[protected, nolint, instance]
def
is_scalar_tower.of_ring_hom
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[comm_semiring A]
[comm_semiring B]
[algebra R A]
[algebra R B]
(f : A →ₐ[R] B) :
is_scalar_tower R A B
def
alg_hom.restrict_scalars
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A →ₐ[S] B) :
R ⟶ S induces S-Alg ⥤ R-Alg
theorem
alg_hom.restrict_scalars_apply
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A →ₐ[S] B)
(x : A) :
⇑(alg_hom.restrict_scalars R f) x = ⇑f x
@[simp]
theorem
alg_hom.coe_restrict_scalars
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A →ₐ[S] B) :
↑(alg_hom.restrict_scalars R f) = ↑f
@[simp]
theorem
alg_hom.coe_restrict_scalars'
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A →ₐ[S] B) :
⇑(alg_hom.restrict_scalars R f) = ⇑f
theorem
alg_hom.restrict_scalars_injective
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B] :
def
alg_equiv.restrict_scalars
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A ≃ₐ[S] B) :
R ⟶ S induces S-Alg ⥤ R-Alg
theorem
alg_equiv.restrict_scalars_apply
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A ≃ₐ[S] B)
(x : A) :
⇑(alg_equiv.restrict_scalars R f) x = ⇑f x
@[simp]
theorem
alg_equiv.coe_restrict_scalars
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A ≃ₐ[S] B) :
↑(alg_equiv.restrict_scalars R f) = ↑f
@[simp]
theorem
alg_equiv.coe_restrict_scalars'
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A ≃ₐ[S] B) :
⇑(alg_equiv.restrict_scalars R f) = ⇑f
theorem
alg_equiv.restrict_scalars_injective
(R : Type u)
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B]
[algebra R A]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B] :
theorem
submodule.restrict_scalars_span
(R : Type u)
(A : Type w)
{M : Type v₁}
[comm_semiring R]
[semiring A]
[algebra R A]
[add_comm_monoid M]
[module R M]
[module A M]
[is_scalar_tower R A M]
(hsur : function.surjective ⇑(algebra_map R A))
(X : set M) :
submodule.restrict_scalars 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₁}
[comm_semiring R]
[semiring A]
[algebra R A]
[add_comm_monoid M]
[module R M]
[module A M]
[is_scalar_tower R A M]
(h : function.surjective ⇑(algebra_map 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]
[add_comm_monoid A]
[module R S]
[module S A]
[module R A]
[is_scalar_tower 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]
[add_comm_monoid A]
[module R S]
[module S A]
[module R A]
[is_scalar_tower R S A]
[smul_comm_class 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]
[add_comm_monoid A]
[module R S]
[module S A]
[module R A]
[is_scalar_tower R S A]
[smul_comm_class 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]
[add_comm_monoid A]
[module R S]
[module S A]
[module R A]
[is_scalar_tower R S A]
[smul_comm_class R S A]
{s : set S}
(hs : submodule.span R s = ⊤)
(t : set A) :
submodule.span R (s • t) = submodule.restrict_scalars R (submodule.span S t)
theorem
submodule.span_algebra_map_image
{R : Type u}
{S : Type v}
[comm_semiring R]
[semiring S]
[algebra R S]
(a : set R) :
submodule.span R (⇑(algebra_map R S) '' a) = submodule.map (algebra.linear_map R S) (submodule.span R a)
A variant of submodule.span_image for algebra_map.
theorem
submodule.span_algebra_map_image_of_tower
{R : Type u}
[comm_semiring R]
{S : Type u_1}
{T : Type u_2}
[comm_semiring S]
[semiring T]
[module R S]
[is_scalar_tower R S S]
[algebra R T]
[algebra S T]
[is_scalar_tower R S T]
(a : set S) :
submodule.span R (⇑(algebra_map S T) '' a) = submodule.map (linear_map.restrict_scalars R (algebra.linear_map S T)) (submodule.span R a)
theorem
submodule.map_mem_span_algebra_map_image
{R : Type u}
[comm_semiring R]
{S : Type u_1}
{T : Type u_2}
[comm_semiring S]
[semiring T]
[algebra R S]
[algebra R T]
[algebra S T]
[is_scalar_tower R S T]
(x : S)
(a : set S)
(hx : x ∈ submodule.span R a) :
⇑(algebra_map S T) x ∈ submodule.span R (⇑(algebra_map S T) '' a)
theorem
algebra.lsmul_injective
(R : Type u)
(A : Type w)
(M : Type v₁)
[comm_semiring R]
[semiring A]
[algebra R A]
[add_comm_group M]
[module A M]
[module R M]
[is_scalar_tower R A M]
[no_zero_smul_divisors A M]
{x : A}
(hx : x ≠ 0) :
function.injective ⇑(⇑(algebra.lsmul R M) x)