mathlib documentation

ring_theory.algebra_tower

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] :

invertible ↑n

A natural number that is invertible when coerced to R is also invertible when coerced to any R-algebra.

Equations

is_scalar_tower.invertible_algebra_coe_nat R A n = is_scalar_tower.invertible.algebra_tower ℕ R A n

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))

theorem algebra.fg_trans' {R : Type u_1} {S : Type u_2} {A : Type u_3} [comm_ring R] [comm_ring S] [comm_ring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (hRS : ⊤.fg) (hSA : ⊤.fg) :

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) :

is_basis R (λ (p : ι × ι'), b p.fst • c p.snd)

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 : ι × ι') :

⇑(⇑(_.repr) x) ij = ⇑(⇑(hb.repr) (⇑(⇑(hc.repr) x) ij.snd)) ij.fst

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 : ι') :

⇑(⇑(_.repr) x) (i, j) = ⇑(⇑(hb.repr) (⇑(⇑(hc.repr) x) j)) i

theorem exists_subalgebra_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] (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.

Equations

alg_hom.extend_scalars B f = {to_fun := f.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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] :

(C →ₐ[A] D) ≃ Σ (f : B →ₐ[A] D), C →ₐ[B] D

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 := _}