# 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.

source
theorem Algebra.adjoin_restrictScalars (C : Type u_1) (D : Type u_2) (E : Type u_3) [CommSemiring C] [CommSemiring D] [CommSemiring E] [Algebra C D] [Algebra C E] [Algebra D E] [IsScalarTower C D E] (S : Set E) :
Subalgebra.restrictScalars C (adjoin D S) = Subalgebra.restrictScalars C (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S)
source
theorem Algebra.adjoin_res_eq_adjoin_res (C : Type u_1) (D : Type u_2) (E : Type u_3) (F : Type u_4) [CommSemiring C] [CommSemiring D] [CommSemiring E] [CommSemiring F] [Algebra C D] [Algebra C E] [Algebra C F] [Algebra D F] [Algebra E F] [IsScalarTower C D F] [IsScalarTower C E F] {S : Set D} {T : Set E} (hS : adjoin C S = ⊤) (hT : adjoin C T = ⊤) :
Subalgebra.restrictScalars C (adjoin E (⇑(algebraMap D F) '' S)) = Subalgebra.restrictScalars C (adjoin D (⇑(algebraMap E F) '' T))
source
theorem Algebra.fg_trans' {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (hRS : ⊤.FG) (hSA : ⊤.FG) :
⊤.FG
source
theorem exists_subalgebra_of_fg (A : Type w) (B : Type u₁) (C : Type u_1) [CommSemiring A] [CommSemiring B] [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (hAC : ⊤.FG) (hBC : ⊤.FG) :
∃ (B₀ : Subalgebra A B), B₀.FG ∧ ⊤.FG
source
theorem fg_of_fg_of_fg (A : Type w) (B : Type u₁) (C : Type u_1) [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [IsNoetherianRing A] (hAC : ⊤.FG) (hBC : ⊤.FG) (hBCi : Function.Injective ⇑(algebraMap B C)) :
⊤.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; Altman--Kleiman 16.17.