# 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 (Algebra.adjoin D S) = Subalgebra.restrictScalars C (Algebra.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 : Algebra.adjoin C S = ⊤)
(hT : Algebra.adjoin C T = ⊤)
:

Subalgebra.restrictScalars C (Algebra.adjoin E (⇑(algebraMap D F) '' S)) = Subalgebra.restrictScalars C (Algebra.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; Stacks 00IS; Altman--Kleiman 16.17.