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
@[instance]
def
is_scalar_tower.subalgebra
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
(S₀ : subalgebra R S) :
is_scalar_tower ↥S₀ 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)
@[instance]
def
is_scalar_tower.subalgebra'
(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]
(S₀ : subalgebra R S) :
is_scalar_tower R ↥S₀ A
@[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_8
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 S B]
[algebra R A]
[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 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) :
⇑(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
@[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
@[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)
@[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
@[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
@[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
@[instance]
def
is_scalar_tower.polynomial
(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 R S (polynomial A)
theorem
is_scalar_tower.aeval_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 : A)
(p : polynomial R) :
⇑(polynomial.aeval x) p = ⇑(polynomial.aeval x) (polynomial.map (algebra_map R S) p)
def
is_scalar_tower.invertible.algebra_tower
(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]
(r : R)
[invertible (⇑(algebra_map R S) r)] :
invertible (⇑(algebra_map R A) r)
Suppose that R -> S -> A is a tower of algebras.
If an element r : R is invertible in S, then it is invertible in A.
Equations
- is_scalar_tower.invertible.algebra_tower R S A r = (invertible.map ↑(algebra_map S A) (⇑(algebra_map R S) r)).copy (⇑(algebra_map R A) r) _
def
is_scalar_tower.invertible_algebra_coe_nat
(R : Type u)
(A : Type w)
[comm_semiring R]
[semiring A]
[algebra R A]
(n : ℕ)
[inv : invertible ↑n] :
A natural number that is invertible when coerced to R is also invertible
when coerced to any R-algebra.
Equations
theorem
is_scalar_tower.algebra_map_aeval
(R : Type u)
(A : Type w)
(B : Type u₁)
[comm_semiring R]
[comm_semiring A]
[comm_semiring B]
[algebra R A]
[algebra A B]
[algebra R B]
[is_scalar_tower R A B]
(x : A)
(p : polynomial R) :
⇑(algebra_map A B) (⇑(polynomial.aeval x) p) = ⇑(polynomial.aeval (⇑(algebra_map A B) x)) p
theorem
is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero
(R : Type u)
(A : Type w)
(B : Type u₁)
[comm_semiring R]
[comm_semiring A]
[comm_semiring B]
[algebra R A]
[algebra A B]
[algebra R B]
[is_scalar_tower R A B]
{x : A}
{p : polynomial R} :
function.injective ⇑(algebra_map A B) → ⇑(polynomial.aeval (⇑(algebra_map A B) x)) p = 0 → ⇑(polynomial.aeval x) p = 0
theorem
is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero_field
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[field A]
[comm_semiring B]
[nontrivial B]
[algebra R A]
[algebra R B]
[algebra A B]
[is_scalar_tower R A B]
{x : A}
{p : polynomial R} :
⇑(polynomial.aeval (⇑(algebra_map A B) x)) p = 0 → ⇑(polynomial.aeval x) p = 0
@[instance]
def
is_scalar_tower.linear_map
(R : Type u)
(A : Type v)
(V : Type w)
[comm_semiring R]
[comm_semiring A]
[add_comm_monoid V]
[semimodule R V]
[algebra R A] :
is_scalar_tower R A (V →ₗ[R] A)
@[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
@[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
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.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, 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)
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} :
theorem
is_basis.smul_repr
{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 u_1}
{ι' : Type u_2}
{b : ι → S}
{c : ι' → A}
(hb : is_basis R b)
(hc : is_basis S c)
(x : A)
(ij : ι × ι') :
theorem
is_basis.smul_repr_mk
{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 u_1}
{ι' : Type u_2}
{b : ι → S}
{c : ι' → A}
(hb : is_basis R b)
(hc : is_basis S c)
(x : A)
(i : ι)
(j : ι') :
theorem
fg_of_fg_of_fg
(A : Type w)
(B : Type u₁)
(C : Type u_1)
[comm_ring A]
[comm_ring B]
[comm_ring C]
[algebra A B]
[algebra B C]
[algebra A C]
[is_scalar_tower A B C]
[is_noetherian_ring A] :
⊤.fg → ⊤.fg → function.injective ⇑(algebra_map B C) → ⊤.fg
Artin--Tate lemma: if A ⊆ B ⊆ C is a chain of subrings of commutative rings, and A is noetherian, and C is algebra-finite over A, and C is module-finite over B, then B is algebra-finite over A.
References: Atiyah--Macdonald Proposition 7.8; Stacks 00IS; Altman--Kleiman 16.17.