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.
@[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}
(h : function.injective ⇑(algebra_map A B))
(hp : ⇑(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}
(h : ⇑(polynomial.aeval (⇑(algebra_map A B) x)) p = 0) :
⇑(polynomial.aeval x) p = 0
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)
theorem
algebra.adjoin_res
(C : Type u_1)
(D : Type u_2)
(E : Type u_3)
[comm_semiring C]
[comm_semiring D]
[comm_semiring E]
[algebra C D]
[algebra C E]
[algebra D E]
[is_scalar_tower C D E]
(S : set E) :
subalgebra.res C (algebra.adjoin D S) = (⊤.map (is_scalar_tower.to_alg_hom C D E)).under (algebra.adjoin ↥(⊤.map (is_scalar_tower.to_alg_hom C D E)) S)
theorem
algebra.adjoin_res_eq_adjoin_res
(C : Type u_1)
(D : Type u_2)
(E : Type u_3)
(F : Type u_4)
[comm_semiring C]
[comm_semiring D]
[comm_semiring E]
[comm_semiring F]
[algebra C D]
[algebra C E]
[algebra C F]
[algebra D F]
[algebra E F]
[is_scalar_tower C D F]
[is_scalar_tower C E F]
{S : set D}
{T : set E}
(hS : algebra.adjoin C S = ⊤)
(hT : algebra.adjoin C T = ⊤) :
subalgebra.res C (algebra.adjoin E (⇑(algebra_map D F) '' S)) = subalgebra.res C (algebra.adjoin D (⇑(algebra_map E F) '' T))
@[simp]
theorem
subalgebra.aeval_coe
(R : Type u)
{A : Type w}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
{S : subalgebra R A}
{x : ↥S}
{p : polynomial R} :
⇑(polynomial.aeval ↑x) p = ↑(⇑(polynomial.aeval x) p)
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}
(hb : linear_independent R b)
(hc : 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}
(hb : is_basis R b)
(hc : is_basis S c) :
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]
(hAC : ⊤.fg)
(hBC : ⊤.fg)
(hBCi : function.injective ⇑(algebra_map B C)) :
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.
def
alg_hom.restrict_domain
{A : Type w}
(B : Type u₁)
{C : Type u_1}
{D : Type u_2}
[comm_semiring A]
[comm_semiring C]
[comm_semiring D]
[algebra A C]
[algebra A D]
(f : C →ₐ[A] D)
[comm_semiring B]
[algebra A B]
[algebra B C]
[is_scalar_tower A B C] :
Restrict the domain of an alg_hom.
Equations
- alg_hom.restrict_domain B f = f.comp (is_scalar_tower.to_alg_hom A B C)
def
alg_hom.extend_scalars
{A : Type w}
(B : Type u₁)
{C : Type u_1}
{D : Type u_2}
[comm_semiring A]
[comm_semiring C]
[comm_semiring D]
[algebra A C]
[algebra A D]
(f : C →ₐ[A] D)
[comm_semiring B]
[algebra A B]
[algebra B C]
[is_scalar_tower A B C] :
Extend the scalars of an alg_hom.
def
alg_hom_equiv_sigma
{A : Type w}
{B : Type u₁}
{C : Type u_1}
{D : Type u_2}
[comm_semiring A]
[comm_semiring C]
[comm_semiring D]
[algebra A C]
[algebra A D]
[comm_semiring B]
[algebra A B]
[algebra B C]
[is_scalar_tower A B C] :
alg_homs from the top of a tower are equivalent to a pair of alg_homs.
Equations
- alg_hom_equiv_sigma = {to_fun := λ (f : C →ₐ[A] D), ⟨alg_hom.restrict_domain B f _inst_9, alg_hom.extend_scalars B f _inst_9⟩, inv_fun := λ (fg : Σ (f : B →ₐ[A] D), C →ₐ[B] D), is_scalar_tower.restrict_base A fg.snd, left_inv := _, right_inv := _}