English
If A is Noetherian, C is algebra-finite over A, and B is module-finite over C with an injective A→C map, then B is finitely generated over A.
Русский
Если A - конечно порожденное кольцо Нётерова, C - алгебра над A конечна, B - модульно конечно над C, и A→C внедримо, то B порождено над A.
LaTeX
$$$\\text{Artin--Tate: FG}(B/A) \\Leftarrow \\text{Noetherian}(A)$ и др.; $B$ FG over $A$$$
Lean4
theorem fg_trans' {R S A : Type*} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A]
[Algebra R A] [IsScalarTower R S A] (hRS : (⊤ : Subalgebra R S).FG) (hSA : (⊤ : Subalgebra S A).FG) :
(⊤ : Subalgebra R A).FG := by
classical
rcases hRS with ⟨s, hs⟩
rcases hSA with ⟨t, ht⟩
exact
⟨s.image (algebraMap S A) ∪ t, by
rw [Finset.coe_union, Finset.coe_image, Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin, hs,
Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top, Subalgebra.restrictScalars_top]⟩
