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.

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) :
r s x = s r x

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

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

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

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

@[ext]
theorem is_scalar_tower.algebra.ext {S : Type u} {A : Type v} [comm_semiring S] [semiring A] (h1 h2 : algebra S A) :
(∀ {r : S} {x : A}, r x = r x)h1 = h2

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.

Equations
@[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) :

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] :
(A →ₐ[S] B)(A →ₐ[R] B)

R ⟶ S induces S-Alg ⥤ R-Alg

Equations
@[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) :

@[instance]
def is_scalar_tower.right (R : Type u) {S : Type v} [comm_semiring R] [comm_semiring S] [algebra R S] :

@[instance]
def is_scalar_tower.nat {S : Type v} {A : Type w} [comm_semiring S] [semiring A] [algebra 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] :

@[instance]
def is_scalar_tower.subsemiring {S : Type v} {A : Type w} [comm_semiring S] [semiring A] [algebra S A] (U : subsemiring S) :

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

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

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

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

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

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

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

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

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

@[instance]
def is_scalar_tower.int (S : Type v) (A : Type w) [comm_ring S] [comm_ring A] [algebra 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] :

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

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

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

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

@[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} :

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

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] :
(U →ₐ[S] B)((S.under U) →ₐ[R] B)

Produces a map from subalgebra.under.

Equations
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] :
.fg.fg.fg

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

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 blinear_independent S clinear_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} :
is_basis R bis_basis S cis_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] :
.fg.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] :

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.