Integrally closed sections of affine opens #
If the ring of sections over an affine open V is a domain, it is integrally closed as
soon as the local rings at the points of V are: its localizations at maximal ideals are local
rings of the scheme at points of V.
Main results #
AlgebraicGeometry.IsAffineOpen.isDomain_and_isIntegrallyClosed_stalk_iff: normality of a stalk is equivalent to normality of the corresponding localization of affine sections.AlgebraicGeometry.IsAffineOpen.isIntegrallyClosed: a domain of sections over an affine open is integrally closed when its local rings are.TauCeti.AlgebraicGeometry.isDomain_and_isIntegrallyClosed_stalk_iff_of_isOpenImmersion: open immersions preserve the domain and integral-closure conditions on stalks.
theorem
TauCeti.AlgebraicGeometry.isDomain_and_isIntegrallyClosed_stalk_iff_of_isOpenImmersion
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.IsOpenImmersion f]
(x : ↥X)
:
An open immersion identifies the local rings at corresponding points, preserving the conjunction of domain and integral-closure properties.
theorem
AlgebraicGeometry.IsAffineOpen.isDomain_and_isIntegrallyClosed_stalk_iff
{T : Scheme}
{V : T.Opens}
(hV : IsAffineOpen V)
(x : ↥V)
:
IsDomain ↑(T.presheaf.stalk ↑x) ∧ IsIntegrallyClosed ↑(T.presheaf.stalk ↑x) ↔ IsDomain (Localization.AtPrime (hV.primeIdealOf x).asIdeal) ∧ IsIntegrallyClosed (Localization.AtPrime (hV.primeIdealOf x).asIdeal)
The stalk at a point of an affine open is an integrally closed domain exactly when the localization of its ring of sections at the corresponding prime is an integrally closed domain.
theorem
AlgebraicGeometry.IsAffineOpen.isIntegrallyClosed
{T : Scheme}
{V : T.Opens}
[IsDomain ↑(T.presheaf.obj (Opposite.op V))]
(hV : IsAffineOpen V)
(hT : ∀ x ∈ V, IsIntegrallyClosed ↑(T.presheaf.stalk x))
:
IsIntegrallyClosed ↑(T.presheaf.obj (Opposite.op V))
The domain of sections over an affine open V is integrally closed if the local rings
at the points of V are: its localizations at maximal ideals are local rings of the scheme at
points of V.