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.
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) _
A natural number that is invertible when coerced to R
is also invertible
when coerced to any R
-algebra.
Equations
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.
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)
Extend the scalars of an alg_hom
.
alg_hom
s from the top of a tower are equivalent to a pair of alg_hom
s.
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 := _}