of_mem_of_fg — Mathlib

English

Let S be a subalgebra of B over R such that S is finitely generated as an R-module. Then every element of S is integral over R.

Русский

Пусть S ⊆ B будет подалгеброй над R и S FG как R-модуль. Тогда каждый элемент S интеграль над R.

LaTeX

$$$S \le B \text{ subalgebra over }R,\; S.toSubmodule.FG \Rightarrow \forall x\in S: IsIntegral(R, x).$$$

Lean4

/-- If `S` is a sub-`R`-algebra of `A` and `S` is finitely-generated as an `R`-module,
  then all elements of `S` are integral over `R`. -/
theorem of_mem_of_fg (S : Subalgebra R B) (HS : S.toSubmodule.FG) (x : B) (hx : x ∈ S) : IsIntegral R x :=
  have : Module.Finite R S := ⟨(fg_top _).mpr HS⟩
  (isIntegral_algHom_iff S.val Subtype.val_injective).mpr (.of_finite R (⟨x, hx⟩ : S))

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