English
For a ring extension R ⊆ A, IsIntegrallyClosedIn R A is equivalent to the algebraMap R A being injective and every integral element of A over R coming from R.
Русский
Для расширения колец R ⊆ A условие IsIntegrallyClosedIn R A эквивалентно тому, что отображение алгебраMap R A инъективно, и каждый элемент A, являющийся интегральным над R, получен как образ элемента R.
LaTeX
$$$IsIntegrallyClosedIn\,R\,A \iff \Big( \text{Injective}(\mathrm{algebraMap}\;R\;A) \wedge \forall x (IsIntegral\,R\,x \rightarrow \exists y\in R, \ algebraMap\;R\;A\;y = x) \Big)$$$
Lean4
/-- `R` is integrally closed in `A` iff all integral elements of `A` are also elements of `R`. -/
theorem isIntegrallyClosedIn_iff {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] :
IsIntegrallyClosedIn R A ↔
Function.Injective (algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, algebraMap R A y = x :=
by
constructor
· rintro ⟨_, cl⟩
simp_all
· rintro ⟨inj, cl⟩
refine ⟨inj, by simp_all, ?_⟩
rintro ⟨y, rfl⟩
apply isIntegral_algebraMap
