English
If the base ring is a domain and deg f ≠ 0, then the AdjoinRoot algebra is nontrivial.
Русский
Если основание является доменом и deg f ≠ 0, то AdjoinRoot f не тривиален.
LaTeX
$$$\\text{AdjoinRoot f}$ is nontrivial if $\\deg f \\neq 0$ and $R$ is a domain$$
Lean4
/-- **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. -/
@[stacks 00IS]
theorem fg_of_fg_of_fg [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).FG) (hBC : (⊤ : Submodule B C).FG)
(hBCi : Function.Injective (algebraMap B C)) : (⊤ : Subalgebra A B).FG :=
let ⟨B₀, hAB₀, hB₀C⟩ := exists_subalgebra_of_fg A B C hAC hBC
Algebra.fg_trans' (B₀.fg_top.2 hAB₀) <|
Subalgebra.fg_of_submodule_fg <|
have : IsNoetherianRing B₀ := isNoetherianRing_of_fg hAB₀
have : Module.Finite B₀ C := ⟨hB₀C⟩
fg_of_injective (IsScalarTower.toAlgHom B₀ B C).toLinearMap hBCi
