# mathlibdocumentation

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} [semiring S] [ S] [ A] [ A] [ A] (r : R) (x : A) :
S) r x = r x

theorem is_scalar_tower.smul_left_comm {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ 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} [semiring A] [ S] [ A] [ A] :
(∀ (x : R), A) x = A) ( S) x)) A

@[instance]
def is_scalar_tower.subalgebra (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] (S₀ : S) :
S A

theorem is_scalar_tower.algebra_map_eq (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] :
A = A).comp S)

theorem is_scalar_tower.algebra_map_apply (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] (x : R) :
A) x = A) ( S) x)

@[instance]
def is_scalar_tower.subalgebra' (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] (S₀ : S) :
S₀ A

@[ext]
theorem is_scalar_tower.algebra.ext {S : Type u} {A : Type v} [semiring A] (h1 h2 : 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) [semiring A] [ S] [ A] [ A] [ A] :
= _inst_8

def is_scalar_tower.to_alg_hom (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ 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) [semiring A] [ S] [ A] [ A] [ A] (y : S) :
A) y = A) y

def is_scalar_tower.restrict_base (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ 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₁} [semiring A] [semiring B] [ S] [ A] [ B] [ A] [ B] [ A] [ B] (f : A →ₐ[S] B) (x : A) :
= f x

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

@[instance]
def is_scalar_tower.nat {S : Type v} {A : Type w} [semiring A] [ A] :
A

@[instance]
def is_scalar_tower.comap {R : Type u_1} {S : Type u_2} {A : Type u_3} [semiring A] [ S] [ A] :
S A)

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

@[instance]
def is_scalar_tower.subring {S : Type u_1} {A : Type u_2} [comm_ring S] [ring A] [ A] (U : set S) [is_subring U] :
A

@[nolint, instance]
def is_scalar_tower.of_ring_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [ A] [ B] (f : A →ₐ[R] B) :
B

@[instance]
def is_scalar_tower.polynomial (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] :

theorem is_scalar_tower.aeval_apply (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] (x : A) (p : polynomial R) :
p = (polynomial.map S) p)

def is_scalar_tower.invertible.algebra_tower (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] (r : R) [invertible ( 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) [semiring A] [ 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₁) [ A] [ B] [ B] [ B] (x : A) (p : polynomial R) :
B) ( p) = (polynomial.aeval ( 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₁) [ A] [ B] [ B] [ B] {x : A} {p : polynomial R} :
(polynomial.aeval ( B) x)) p = 0 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} [field A] [nontrivial B] [ A] [ B] [ B] [ B] {x : A} {p : polynomial R} :
(polynomial.aeval ( B) x)) p = 0 p = 0

@[instance]
def is_scalar_tower.linear_map (R : Type u) (A : Type v) (V : Type w) [ V] [ A] :
(V →ₗ[R] A)

@[instance]
def is_scalar_tower.int (S : Type v) (A : Type w) [comm_ring S] [comm_ring A] [ A] :
A

@[instance]
def is_scalar_tower.rat (R : Type u) (S : Type v) [field R] [ S] [char_zero R] [char_zero S] :
S

theorem algebra.adjoin_algebra_map' {R : Type u} {S : Type v} {A : Type w} [comm_ring R] [comm_ring S] [comm_ring A] [ S] [ A] (s : set S) :
( S A)) '' s) = s).map 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] [ S] [ A] [ A] [ A] (s : set S) :
( A) '' s) = s).map A)

def subalgebra.res (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] :
A 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} [semiring A] [ S] [ A] [ A] [ A] :

@[simp]
theorem subalgebra.mem_res (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] {U : A} {x : A} :
x x U

theorem subalgebra.res_inj (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] {U V : A} :
= U = V

def subalgebra.of_under {R : Type u_1} {A : Type u_2} {B : Type u_3} [semiring B] [ A] [ B] (S : A) (U : A) [ B] [ B] :
(U →ₐ[S] B)((S.under U) →ₐ[R] B)

Produces a map from subalgebra.under.

Equations
theorem is_scalar_tower.range_under_adjoin (R : Type u) (S : Type v) (A : Type w) [ S] [ A] [ A] [ A] (t : set A) :

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] [ S] [ A] [ A] [ A] :
.fg.fg.fg

theorem submodule.smul_mem_span_smul_of_mem {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ A] {s : set S} {t : set A} {k : S} (hks : k ) {x : A} :
x tk x (s t)

theorem submodule.smul_mem_span_smul {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ A] {s : set S} (hs : = ) {t : set A} {k : S} {x : A} :
x k x (s t)

theorem submodule.smul_mem_span_smul' {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ A] {s : set S} (hs : = ) {t : set A} {k : S} {x : A} :
x (s t)k x (s t)

theorem submodule.span_smul {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ A] {s : set S} (hs : = ) (t : set A) :
(s t) =

theorem linear_independent_smul {R : Type u} {S : Type v} {A : Type w} [comm_ring R] [ring S] [ S] [ A] [ A] [ A] {ι : Type v₁} {b : ι → S} {ι' : Type w₁} {c : ι' → A} :
(λ (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] [ S] [ A] [ A] [ A] {ι : Type v₁} {b : ι → S} {ι' : Type w₁} {c : ι' → A} :
b c (λ (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] [ S] [ A] [ A] [ A] {ι : Type u_1} {ι' : Type u_2} {b : ι → S} {c : ι' → A} (hb : b) (hc : 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] [ S] [ A] [ A] [ A] {ι : Type u_1} {ι' : Type u_2} {b : ι → S} {c : ι' → A} (hb : b) (hc : 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] [ B] [ C] [ C] [ C] :
.fg.fg(∃ (B₀ : 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] [ B] [ C] [ C] [ C]  :
.fg.fg.fg

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.