English
Let R be a commutative ring and A an R-algebra. If s is a finite subset of A and every element of s is integral over R, then the underlying R-submodule of the subalgebra generated by s is finitely generated.
Русский
Пусть R — коммутативное кольцо и A — R-алгебра. Если s — конечный подмножество A и каждый элемент s интегрирован над R, то соответствующий подмодуль над R, порожденный алгеброй, порожден этим s, конечно порожден.
LaTeX
$$$\\text{If } s \\subseteq A \\text{ is finite and every } x\\in s \\text{ is integral over } R, \\text{ then } (\\mathrm{adjoin}\\, R\\, s).\\text{toSubmodule}$ is FG.$$
Lean4
@[stacks 09GH]
theorem fg_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsIntegral R x) :
(Algebra.adjoin R s).toSubmodule.FG := by
induction s, hfs using Set.Finite.induction_on with
| empty =>
refine ⟨{ 1 }, Submodule.ext fun x => ?_⟩
rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]
| @insert a s _ _ ih =>
rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]
exact FG.mul (ih fun i hi => his i <| Set.mem_insert_of_mem a hi) (his a <| Set.mem_insert a s).fg_adjoin_singleton
