# Adjoining elements and being finitely generated in an algebra tower #

## Main results #

• Algebra.fg_trans': if S is finitely generated as R-algebra and A as S-algebra, then A is finitely generated as R-algebra
• fg_of_fg_of_fg: Artin--Tate lemma: if C/B/A is a tower of 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.
theorem Algebra.adjoin_restrictScalars (C : Type u_1) (D : Type u_2) (E : Type u_3) [] [] [] [Algebra C D] [Algebra C E] [Algebra D E] [] (S : Set E) :
theorem Algebra.adjoin_res_eq_adjoin_res (C : Type u_1) (D : Type u_2) (E : Type u_3) (F : Type u_4) [] [] [] [] [Algebra C D] [Algebra C E] [Algebra C F] [Algebra D F] [Algebra E F] [] [] {S : Set D} {T : Set E} (hS : = ) (hT : = ) :
theorem Algebra.fg_trans' {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [] [Algebra R S] [Algebra S A] [Algebra R A] [] (hRS : .FG) (hSA : .FG) :
.FG
theorem exists_subalgebra_of_fg (A : Type w) (B : Type u₁) (C : Type u_1) [] [] [] [Algebra A B] [Algebra B C] [Algebra A C] [] (hAC : .FG) (hBC : .FG) :
∃ (B₀ : ), B₀.FG .FG
theorem fg_of_fg_of_fg (A : Type w) (B : Type u₁) (C : Type u_1) [] [] [] [Algebra A B] [Algebra B C] [Algebra A C] [] [] (hAC : .FG) (hBC : .FG) (hBCi : Function.Injective ()) :
.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.