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

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

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

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

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.