English
The infimum (intersection) of a family of integrally closed subalgebras of a field extension is integrally closed, provided each member is.
Русский
Пересечение семейства интегрально замкнутых подалгебр расширения поля интегрально замкнуто, если каждый член интегрально замкнут.
LaTeX
$$$\\forall i,\\; IsIntegrallyClosed(S_i) \\Rightarrow IsIntegrallyClosed(\\bigwedge_i S_i)$$$
Lean4
theorem iInf {ι : Type*} (S : ι → Subalgebra R K) (h : ∀ i, IsIntegrallyClosed (S i)) :
IsIntegrallyClosed (⨅ i, S i : Subalgebra R K) :=
by
refine (isIntegrallyClosed_iff K).mpr (fun {x} hx ↦ CanLift.prf x (Algebra.mem_iInf.mpr ?_))
intro i
have le : (⨅ i : ι, S i : Subalgebra R K) ≤ S i := iInf_le S i
algebraize [(Subalgebra.inclusion le).toRingHom]
have : IsScalarTower ↥(⨅ i, S i) (S i) K := Subalgebra.inclusion.isScalarTower_right le K
rcases (isIntegrallyClosed_iff K).mp (h i) hx.tower_top with ⟨⟨_, hin⟩, hy⟩
rwa [← hy]
