mem_integralClosure_iff_mem_fg — Mathlib

English

An element r belongs to integralClosure R A iff r lies in some finitely generated subalgebra M of A.

Русский

Элемент r принадлежит интегральному замыканию, если он лежит в некоторой конечномерной ( FG) подалгебре M ≤ A.

LaTeX

$$$r \\in integralClosure R A \\iff \\exists M \\; M.toSubmodule.FG \\land r \\in M$$$

Lean4

theorem mem_integralClosure_iff_mem_fg {r : A} :
    r ∈ integralClosure R A ↔ ∃ M : Subalgebra R A, M.toSubmodule.FG ∧ r ∈ M :=
  ⟨fun hr => ⟨Algebra.adjoin R { r }, hr.fg_adjoin_singleton, Algebra.subset_adjoin rfl⟩, fun ⟨M, Hf, hrM⟩ =>
    .of_mem_of_fg M Hf _ hrM⟩

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