Normal schemes

A scheme is normal if every local ring is an integrally closed domain (Stacks, Definition 28.7.1 (033I)). This file defines the class TauCeti.AlgebraicGeometry.IsNormalScheme and proves its basic properties: normality is local, so it can be checked on the rings of sections over affine opens, whose localizations at primes are the local rings of the scheme (Stacks, Lemma 28.7.2 (033J)); open subschemes of normal schemes are normal; normal schemes are reduced (Stacks, Lemma 28.7.3 (033K)); the spectrum of a domain is normal exactly when the domain is integrally closed; on a normal scheme the domain of sections over an affine open is integrally closed; and on a locally Noetherian normal scheme the local ring at a point of coheight one is a discrete valuation ring (Stacks, Lemma 10.119.7 (00PD)).

Following Stacks, Definition 10.37.11 (00GV), a ring R is normal when every localization of R at a prime is an integrally closed domain; isNormalScheme_Spec_iff_forall_localization says that this holds exactly when Spec R is a normal scheme, and the affine statements below use IsNormalScheme (Spec R) for it.

Main results

• TauCeti.AlgebraicGeometry.IsNormalScheme: every local ring is an integrally closed domain.
• TauCeti.AlgebraicGeometry.isNormalScheme_Spec_iff_forall_localization: Spec R is normal iff every localization of R at a prime is an integrally closed domain.
• TauCeti.AlgebraicGeometry.isNormalScheme_iff_forall_affineOpens: a scheme is normal iff the ring of sections over every affine open is normal.
• TauCeti.AlgebraicGeometry.isNormalScheme_iff_forall_exists_affineOpens: it suffices that every point has an affine open neighbourhood with normal ring of sections.
• TauCeti.AlgebraicGeometry.isNormalScheme_iff_openCover: normality is local on an open cover.
• TauCeti.AlgebraicGeometry.IsNormalScheme.of_isOpenImmersion: the source of an open immersion into a normal scheme is normal; open subschemes and the components of open covers of a normal scheme are normal (instances).
• TauCeti.AlgebraicGeometry.IsNormalScheme.isReduced: normal schemes are reduced.
• TauCeti.AlgebraicGeometry.isNormalScheme_Spec_iff: for a domain R, Spec R is normal iff R is integrally closed.
• TauCeti.AlgebraicGeometry.IsNormalScheme.isIntegrallyClosed_of_isAffineOpen: on a normal scheme, a domain of sections over an affine open is integrally closed.
• TauCeti.AlgebraicGeometry.IsNormalScheme.isDiscreteValuationRing_stalk: on a locally Noetherian normal scheme, the local ring at a point of coheight one is a discrete valuation ring, by the ring-level IsDiscreteValuationRing.of_ringKrullDim_eq_one.

References

• Stacks Project, Definition 28.7.1, Lemma 28.7.2, Lemma 28.7.3 and Lemma 10.119.7.
• IsNormalScheme.isDiscreteValuationRing_stalk is ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0): it is Pcf.SchemeDivisorPoint.stalk_isDiscreteValuationRing in lean/Pcf/Bounding/SchemeDynamics.lean, whose ring-level step (ported as IsDiscreteValuationRing.of_ringKrullDim_eq_one) is Pcf.isDiscreteValuationRing_localizationAtPrime_of_heightOne in lean/Pcf/Bounding/Divisors.lean. The source states it for an integral scheme with its own affine-sections predicate Pcf.IsNormalScheme (lean/Pcf/Bounding/SchemeExtraction.lean); here it is stated for the stalkwise class and needs neither integrality nor an affine chart.

class TauCeti.AlgebraicGeometry.IsNormalScheme (X : AlgebraicGeometry.Scheme) : Prop

A scheme is normal if every local ring is a domain and integrally closed. Stacks, Definition 28.7.1 (033I).

• isDomain_stalk (x : ↥X) : IsDomain ↑(X.presheaf.stalk x)
• isIntegrallyClosed_stalk (x : ↥X) : IsIntegrallyClosed ↑(X.presheaf.stalk x)

theorem TauCeti.AlgebraicGeometry.isNormalScheme_iff_forall_stalk {X : AlgebraicGeometry.Scheme} : IsNormalScheme X ↔ ∀ (x : ↥X), IsDomain ↑(X.presheaf.stalk x) ∧ IsIntegrallyClosed ↑(X.presheaf.stalk x)

A scheme is normal iff each of its local rings is an integrally closed domain; this is the definition, as a single condition per point.

theorem TauCeti.AlgebraicGeometry.IsNormalScheme.of_isOpenImmersion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [IsNormalScheme Y] : IsNormalScheme X

The source of an open immersion into a normal scheme is normal.

instance TauCeti.AlgebraicGeometry.IsNormalScheme.opens {X : AlgebraicGeometry.Scheme} [IsNormalScheme X] (U : X.Opens) : IsNormalScheme ↑U

Open subschemes of a normal scheme are normal.

theorem TauCeti.AlgebraicGeometry.IsNormalScheme.of_forall_exists_isOpenImmersion {X : AlgebraicGeometry.Scheme} (h : ∀ (x : ↥X), ∃ (Y : AlgebraicGeometry.Scheme) (f : Y ⟶ X), AlgebraicGeometry.IsOpenImmersion f ∧ IsNormalScheme Y ∧ x ∈ Set.range ⇑f) : IsNormalScheme X

A scheme is normal as soon as every point lies in the image of an open immersion from a normal scheme.

theorem TauCeti.AlgebraicGeometry.isNormalScheme_iff_openCover {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : IsNormalScheme X ↔ ∀ (i : 𝒰.I₀), IsNormalScheme (𝒰.X i)

Normality is local on an open cover. Stacks, Lemma 28.7.2 (033J), in the form "normality is local".

instance TauCeti.AlgebraicGeometry.IsNormalScheme.openCover {X : AlgebraicGeometry.Scheme} [IsNormalScheme X] (𝒰 : X.OpenCover) (i : 𝒰.I₀) : IsNormalScheme (𝒰.X i)

The components of an open cover of a normal scheme are normal.

theorem TauCeti.AlgebraicGeometry.isNormalScheme_Spec_iff_forall_localization (R : CommRingCat) : IsNormalScheme (AlgebraicGeometry.Spec R) ↔ ∀ (p : Ideal ↑R) [inst : p.IsPrime], IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)

Spec R is normal iff R is a normal ring in the sense of Stacks, Definition 10.37.11 (00GV): every localization of R at a prime is an integrally closed domain. The local rings of Spec R are these localizations (Mathlib AlgebraicGeometry.Spec.stalkIso).

theorem TauCeti.AlgebraicGeometry.isNormalScheme_iff_forall_affineOpens {X : AlgebraicGeometry.Scheme} : IsNormalScheme X ↔ ∀ (U : ↑X.affineOpens), IsNormalScheme (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ↑U)))

A scheme is normal iff the ring of sections over every affine open is normal: Spec Γ(X, U) is normal, which by isNormalScheme_Spec_iff_forall_localization says that every localization of Γ(X, U) at a prime is an integrally closed domain. Stacks, Lemma 28.7.2 (033J).

theorem TauCeti.AlgebraicGeometry.isNormalScheme_iff_forall_exists_affineOpens {X : AlgebraicGeometry.Scheme} : IsNormalScheme X ↔ ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ IsNormalScheme (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ↑U)))

A scheme is normal as soon as every point has an affine open neighbourhood whose ring of sections is normal. Stacks, Lemma 28.7.2 (033J), the affine open covering form.

instance TauCeti.AlgebraicGeometry.IsNormalScheme.isReduced (X : AlgebraicGeometry.Scheme) [IsNormalScheme X] : AlgebraicGeometry.IsReduced X

A normal scheme is reduced: its local rings are domains. Stacks, Lemma 28.7.3 (033K).

theorem TauCeti.AlgebraicGeometry.isNormalScheme_Spec_iff (R : CommRingCat) [IsDomain ↑R] : IsNormalScheme (AlgebraicGeometry.Spec R) ↔ IsIntegrallyClosed ↑R

The spectrum of a domain R is normal exactly when R is integrally closed.

instance TauCeti.AlgebraicGeometry.isNormalScheme_Spec (R : CommRingCat) [IsDomain ↑R] [IsIntegrallyClosed ↑R] : IsNormalScheme (AlgebraicGeometry.Spec R)

The spectrum of an integrally closed domain is normal.

theorem TauCeti.AlgebraicGeometry.IsNormalScheme.isIntegrallyClosed_of_isAffineOpen {X : AlgebraicGeometry.Scheme} [IsNormalScheme X] {U : X.Opens} [IsDomain ↑(X.presheaf.obj (Opposite.op U))] (hU : AlgebraicGeometry.IsAffineOpen U) : IsIntegrallyClosed ↑(X.presheaf.obj (Opposite.op U))

On a normal scheme, the domain of sections over an affine open is integrally closed. For an integral scheme, IsIntegral.component_integral supplies the domain instance.

theorem TauCeti.AlgebraicGeometry.IsNormalScheme.isDiscreteValuationRing_stalk {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] [IsNormalScheme X] (x : ↥X) (hx : Order.coheight x = 1) : IsDiscreteValuationRing ↑(X.presheaf.stalk x)

On a locally Noetherian normal scheme the local ring at a point of coheight one is a discrete valuation ring. Stacks, Lemma 10.119.7 (00PD).