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.
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
algebra.adjoin_algebra_map
(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 : 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_restrict_scalars
(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.restrict_scalars C (algebra.adjoin D S) = subalgebra.restrict_scalars C (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.restrict_scalars C (algebra.adjoin E (⇑(algebra_map D F) '' S)) = subalgebra.restrict_scalars C (algebra.adjoin D (⇑(algebra_map E F) '' T))
theorem
algebra.fg_trans'
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[comm_semiring R]
[comm_semiring S]
[comm_semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A]
(hRS : ⊤.fg)
(hSA : ⊤.fg) :
@[simp]
theorem
basis.algebra_map_coeffs_repr_apply_support_val
{R : Type u}
(A : Type w)
{ι : Type u_1}
{M : Type u_2}
[comm_semiring R]
[semiring A]
[add_comm_monoid M]
[algebra R A]
[module A M]
[module R M]
[is_scalar_tower R A M]
(b : basis ι R M)
(h : function.bijective ⇑(algebra_map R A))
(ᾰ : M) :
noncomputable
def
basis.algebra_map_coeffs
{R : Type u}
(A : Type w)
{ι : Type u_1}
{M : Type u_2}
[comm_semiring R]
[semiring A]
[add_comm_monoid M]
[algebra R A]
[module A M]
[module R M]
[is_scalar_tower R A M]
(b : basis ι R M)
(h : function.bijective ⇑(algebra_map R A)) :
basis ι A M
If R and A have a bijective algebra_map R A and act identically on M,
then a basis for M as R-module is also a basis for M as R'-module.
Equations
- basis.algebra_map_coeffs A b h = b.map_coeffs (ring_equiv.of_bijective (algebra_map R A) h) _
@[simp]
theorem
basis.algebra_map_coeffs_repr_apply_to_fun
{R : Type u}
(A : Type w)
{ι : Type u_1}
{M : Type u_2}
[comm_semiring R]
[semiring A]
[add_comm_monoid M]
[algebra R A]
[module A M]
[module R M]
[is_scalar_tower R A M]
(b : basis ι R M)
(h : function.bijective ⇑(algebra_map R A))
(ᾰ : M)
(ᾰ_1 : ι) :
⇑(⇑((basis.algebra_map_coeffs A b h).repr) ᾰ) ᾰ_1 = ⇑(algebra_map R A) (⇑(⇑(b.repr) ᾰ) ᾰ_1)
@[simp]
theorem
basis.algebra_map_coeffs_repr_symm_apply
{R : Type u}
(A : Type w)
{ι : Type u_1}
{M : Type u_2}
[comm_semiring R]
[semiring A]
[add_comm_monoid M]
[algebra R A]
[module A M]
[module R M]
[is_scalar_tower R A M]
(b : basis ι R M)
(h : function.bijective ⇑(algebra_map R A))
(ᾰ : ι →₀ A) :
⇑((basis.algebra_map_coeffs A b h).repr.symm) ᾰ = ⇑(finsupp.total ι M R ⇑b) (finsupp.map_range ⇑(module.comp_hom.to_linear_equiv (ring_equiv.of_bijective (algebra_map R A) h).symm) _ ᾰ)
theorem
basis.algebra_map_coeffs_apply
{R : Type u}
(A : Type w)
{ι : Type u_1}
{M : Type u_2}
[comm_semiring R]
[semiring A]
[add_comm_monoid M]
[algebra R A]
[module A M]
[module R M]
[is_scalar_tower R A M]
(b : basis ι R M)
(h : function.bijective ⇑(algebra_map R A))
(i : ι) :
⇑(basis.algebra_map_coeffs A b h) i = ⇑b i
@[simp]
theorem
basis.coe_algebra_map_coeffs
{R : Type u}
(A : Type w)
{ι : Type u_1}
{M : Type u_2}
[comm_semiring R]
[semiring A]
[add_comm_monoid M]
[algebra R A]
[module A M]
[module R M]
[is_scalar_tower R A M]
(b : basis ι R M)
(h : function.bijective ⇑(algebra_map R A)) :
⇑(basis.algebra_map_coeffs A b h) = ⇑b
theorem
linear_independent_smul
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid 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)
noncomputable
def
basis.smul
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[module S A]
[module R A]
[is_scalar_tower R S A]
{ι : Type v₁}
{ι' : Type w₁}
(b : basis ι R S)
(c : basis ι' S A) :
basis.smul (b : basis ι R S) (c : basis ι S A) is the R-basis on A
where the (i, j)th basis vector is b i • c j.
Equations
- b.smul c = {repr := (linear_equiv.restrict_scalars R c.repr).trans ((finsupp.lcongr (equiv.refl ι') b.repr).trans ((finsupp.finsupp_prod_lequiv R).symm.trans (finsupp.lcongr (equiv.prod_comm ι' ι) (linear_equiv.refl R R))))}
@[simp]
theorem
basis.smul_repr
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[module S A]
[module R A]
[is_scalar_tower R S A]
{ι : Type v₁}
{ι' : Type w₁}
(b : basis ι R S)
(c : basis ι' S A)
(x : A)
(ij : ι × ι') :
theorem
basis.smul_repr_mk
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[module S A]
[module R A]
[is_scalar_tower R S A]
{ι : Type v₁}
{ι' : Type w₁}
(b : basis ι R S)
(c : basis ι' S A)
(x : A)
(i : ι)
(j : ι') :
@[simp]
theorem
basis.smul_apply
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[semiring S]
[add_comm_monoid A]
[algebra R S]
[module S A]
[module R A]
[is_scalar_tower R S A]
{ι : Type v₁}
{ι' : Type w₁}
(b : basis ι R S)
(c : basis ι' S A)
(ij : ι × ι') :
theorem
basis.algebra_map_injective
{R : Type u}
{S : Type v}
[comm_ring R]
[ring S]
[algebra R S]
{ι : Type u_1}
[no_zero_divisors R]
[nontrivial S]
(b : basis ι R S) :
theorem
exists_subalgebra_of_fg
(A : Type w)
(B : Type u₁)
(C : Type u_1)
[comm_semiring A]
[comm_semiring B]
[semiring C]
[algebra A B]
[algebra B C]
[algebra A C]
[is_scalar_tower A B C]
(hAC : ⊤.fg)
(hBC : ⊤.fg) :
∃ (B₀ : subalgebra A B), B₀.fg ∧ ⊤.fg
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), let alg : algebra B D := fg.fst.to_ring_hom.to_algebra in alg_hom.restrict_scalars A fg.snd, left_inv := _, right_inv := _}