The finite normalization of an integral scheme is a modification #
Let Y be an integral scheme and ν : Y^ν ⟶ Y its normalization in its function field, along
Spec k(Y) ⟶ Y. Over an affine open U = Spec A of Y, the scheme Y^ν is the spectrum of the
integral closure of A in k(Y), the fraction field of A.
So ν is an isomorphism over every affine open whose ring is integrally closed
(TauCeti.AlgebraicGeometry.isIso_morphismRestrict_fromNormalization_of_isIntegrallyClosed, in
TauCeti.AlgebraicGeometry.Normalization.IsIso). When ν is finite, these rings are N-1
(TauCeti.AlgebraicGeometry.isFinite_fromNormalization_fromSpecStalk_genericPoint_iff, in
TauCeti.AlgebraicGeometry.Normalization.Finite), and an N-1 domain becomes integrally closed
after inverting one nonzero element. Hence ν is an isomorphism over a nonempty, so dense, basic
open of Y, and being finite it is proper: ν is a modification. Together with
TauCeti.AlgebraicGeometry.isRegular_normalization_fromSpecStalk_genericPoint, this shows that the
finite normalization of an integral locally Noetherian scheme of dimension at most one is a
resolution of singularities: a regular scheme with a finite modification to Y (Stacks,
Lemma 33.41.1 (0C45) over a field).
Main results #
TauCeti.AlgebraicGeometry.isModification_fromNormalization_fromSpecStalk_genericPoint: if this normalization is finite, it is a modification.
References #
Resolution of curves: the normalization is a modification. If the normalization of an
integral scheme Y in its function field, along Spec k(Y) ⟶ Y, is finite over Y, then it is a
modification of Y: it is proper, and an isomorphism over a dense open of Y with dense preimage.
Stacks, Lemma 33.41.1 (0C45) over a field.