English
Let R be a domain with fraction field K and let (S_i) be a family of subalgebras of K over R. If every S_i is integrally closed and the infimum of all S_i is the bottom subalgebra, then R is integrally closed.
Русский
Пусть R — интегрально замкнутая область над своей полевой дробной оболочкой K, и пусть (S_i) — Family подалгебр K над R. Если каждая S_i интегрально замкнута и их общая пересечение (или экв. инфимум) равно минимальной подалгебре, то R интегрально замкнута.
LaTeX
$$$\\Big( \\forall i, \\ IsIntegrallyClosed(S_i) \\Big) \\land \\big( \\inf_{i} S_i = \\bot \\big) \\;\Rightarrow\\; IsIntegrallyClosed(R).$$$
Lean4
theorem of_iInf_eq_bot {ι : Type*} (S : ι → Subalgebra R K) (h : ∀ i : ι, IsIntegrallyClosed (S i))
(hs : ⨅ i : ι, S i = ⊥) : IsIntegrallyClosed R :=
have f : (⊥ : Subalgebra R K) ≃ₐ[R] R := Algebra.botEquivOfInjective (FaithfulSMul.algebraMap_injective R K)
(IsIntegrallyClosed.iInf S h).of_equiv (hs ▸ f).toRingEquiv
