Towers of algebras
We set up the basic theory of algebra towers.
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).
In field_theory/tower.lean we use this to prove the tower law for finite extensions,
that if R and S are both fields, then [A:R] = [A:S] [S:A].
In this file we prepare the main lemma:
if {bi | i ∈ I} is an R-basis of S and {cj | j ∈ J} is a S-basis
of A, then {bi cj | i ∈ I, j ∈ J} is an R-basis of A. This statement does not require the
base rings to be a field, so we also generalize the lemma to rings in this file.
theorem
is_scalar_tower.algebra_map_smul
{R : Type u}
(S : Type v)
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower R S A]
(r : R)
(x : A) :
⇑(algebra_map R S) r • x = r • x
theorem
is_scalar_tower.smul_left_comm
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower R S A]
(r : R)
(s : S)
(x : 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] :
(∀ (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.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) :
theorem
is_scalar_tower.algebra_comap_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.comap.algebra R S A = _inst_7
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.
@[simp]
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
def
is_scalar_tower.restrict_base
(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 R A]
[algebra S B]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B] :
R ⟶ S induces S-Alg ⥤ R-Alg
@[simp]
theorem
is_scalar_tower.restrict_base_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 R A]
[algebra S B]
[algebra R B]
[is_scalar_tower R S A]
[is_scalar_tower R S B]
(f : A →ₐ[S] B)
(x : A) :
⇑(is_scalar_tower.restrict_base R f) x = ⇑f x
@[instance]
def
is_scalar_tower.right
(R : Type u)
{S : Type v}
[comm_semiring R]
[comm_semiring S]
[algebra R S] :
is_scalar_tower R S S
Equations
- _ = _
@[instance]
def
is_scalar_tower.nat
{S : Type v}
{A : Type w}
[comm_semiring S]
[semiring A]
[algebra S A] :
is_scalar_tower ℕ S A
Equations
@[instance]
def
is_scalar_tower.comap
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A] :
is_scalar_tower R S (algebra.comap R S A)
Equations
@[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
Equations
- _ = _
@[instance]
def
is_scalar_tower.subring
{S : Type u_1}
{A : Type u_2}
[comm_ring S]
[ring A]
[algebra S A]
(U : set S)
[is_subring U] :
is_scalar_tower ↥U S A
Equations
- _ = _
@[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
Equations
- _ = _
@[instance]
def
is_scalar_tower.subalgebra
(R : Type u)
(A : Type w)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(S : subalgebra R A) :
is_scalar_tower R ↥S A
Equations
- _ = _
@[instance]
def
is_scalar_tower.polynomial
(R : Type u)
(A : Type w)
(B : Type u₁)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[comm_semiring B]
[algebra A B]
[algebra R B]
[is_scalar_tower R A B] :
is_scalar_tower R A (polynomial B)
Equations
- _ = _
theorem
is_scalar_tower.aeval_apply
(R : Type u)
(A : Type w)
(B : Type u₁)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[comm_semiring B]
[algebra A B]
[algebra R B]
[is_scalar_tower R A B]
(x : B)
(p : polynomial R) :
⇑(polynomial.aeval x) p = ⇑(polynomial.aeval x) (polynomial.map (algebra_map R A) p)
@[instance]
def
is_scalar_tower.int
(S : Type v)
(A : Type w)
[comm_ring S]
[comm_ring A]
[algebra S A] :
is_scalar_tower ℤ S A
Equations
- _ = _
@[instance]
def
is_scalar_tower.rat
(R : Type u)
(S : Type v)
[field R]
[division_ring S]
[algebra R S]
[char_zero R]
[char_zero S] :
is_scalar_tower ℚ R S
Equations
- _ = _
theorem
algebra.adjoin_algebra_map'
{R : Type u}
{S : Type v}
{A : Type w}
[comm_ring R]
[comm_ring S]
[comm_ring A]
[algebra R S]
[algebra S A]
(s : set S) :
algebra.adjoin R (⇑(algebra_map S (algebra.comap R S A)) '' s) = (algebra.adjoin R s).map (algebra.to_comap R S A)
theorem
algebra.adjoin_algebra_map
(R : Type u)
(S : Type v)
(A : Type w)
[comm_ring R]
[comm_ring S]
[comm_ring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A]
(s : set S) :
algebra.adjoin R (⇑(algebra_map S A) '' s) = (algebra.adjoin R s).map (is_scalar_tower.to_alg_hom R S A)
def
subalgebra.res
(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] :
subalgebra S A → subalgebra R A
If A/S/R is a tower of algebras then the restriction of a S-subalgebra of A is an R-subalgebra of A.
Equations
- subalgebra.res R U = {carrier := ↑U, algebra_map_mem' := _}
@[simp]
theorem
subalgebra.res_top
(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] :
subalgebra.res R ⊤ = ⊤
@[simp]
theorem
subalgebra.mem_res
(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]
{U : subalgebra S A}
{x : A} :
x ∈ subalgebra.res R U ↔ x ∈ U
theorem
subalgebra.res_inj
(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]
{U V : subalgebra S A} :
subalgebra.res R U = subalgebra.res R V → U = V
def
subalgebra.of_under
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[comm_semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(S : subalgebra R A)
(U : subalgebra ↥S A)
[algebra ↥S B]
[is_scalar_tower R ↥S B] :
Produces a map from subalgebra.under.
theorem
is_scalar_tower.range_under_adjoin
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[comm_semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A]
(t : set A) :
(is_scalar_tower.to_alg_hom R S A).range.under (algebra.adjoin ↥((is_scalar_tower.to_alg_hom R S A).range) t) = subalgebra.res R (algebra.adjoin S t)
def
submodule.restrict_scalars'
(R : Type u)
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower R S A] :
Restricting the scalars of submodules in an algebra tower.
theorem
submodule.restrict_scalars'_top
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower R S A] :
theorem
submodule.restrict_scalars'_injective
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower R S A]
(U₁ U₂ : submodule S A) :
submodule.restrict_scalars' R U₁ = submodule.restrict_scalars' R U₂ → U₁ = U₂
theorem
submodule.restrict_scalars'_inj
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower R S A]
{U₁ U₂ : submodule S A} :
submodule.restrict_scalars' R U₁ = submodule.restrict_scalars' R U₂ ↔ U₁ = U₂
theorem
submodule.smul_mem_span_smul_of_mem
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower R S A]
{s : set S}
{t : set A}
{k : S}
(hks : k ∈ submodule.span R s)
{x : A} :
x ∈ t → k • x ∈ submodule.span R (s • t)
theorem
submodule.smul_mem_span_smul
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower R S A]
{s : set S}
(hs : submodule.span R s = ⊤)
{t : set A}
{k : S}
{x : A} :
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}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower R S A]
{s : set S}
(hs : submodule.span R s = ⊤)
{t : set A}
{k : S}
{x : A} :
x ∈ submodule.span R (s • t) → k • x ∈ submodule.span R (s • t)
theorem
submodule.span_smul
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[semimodule S A]
[semimodule R A]
[is_scalar_tower 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
linear_independent_smul
{R : Type u}
{S : Type v}
{A : Type w}
[comm_ring R]
[ring S]
[add_comm_group A]
[algebra R S]
[module S A]
[module R A]
[is_scalar_tower R S A]
{ι : Type v₁}
{b : ι → S}
{κ : Type w₁}
{c : κ → A} :
linear_independent R b → linear_independent S c → linear_independent R (λ (p : ι × κ), b p.fst • c p.snd)
theorem
is_basis.smul
{R : Type u}
{S : Type v}
{A : Type w}
[comm_ring R]
[ring S]
[add_comm_group A]
[algebra R S]
[module S A]
[module R A]
[is_scalar_tower R S A]
{ι : Type v₁}
{b : ι → S}
{κ : Type w₁}
{c : κ → A} :