fg_adjoin_singleton — Mathlib

English

If x is integral over R, then the submodule underlying the subalgebra generated by x is finitely generated.

Русский

Если x интегрален над R, то подмодуль, лежащий в основе подалгебры, порожденной x, является конечно порожденным.

LaTeX

$$$\\bigl(\\operatorname{Adjoin}_R\\{x\\}\\bigr)_{\\text{toSubmodule}} \\text{ is FG}$$$

Lean4

theorem fg_adjoin_singleton [Algebra R B] {x : B} (hx : IsIntegral R x) : (Algebra.adjoin R { x }).toSubmodule.FG := by
  classical
  rcases hx with ⟨f, hfm, hfx⟩
  use (Finset.range <| f.natDegree).image (x ^ ·)
  exact span_range_natDegree_eq_adjoin hfm (by rwa [aeval_def])

Похожие утверждения