Module

Normal.lean

Nyll.SchemeTheory.Normalization.Normal

7 declarations indexed from sourceView source ↗

Module documentation

Normal integral schemes

This file provides a focused normality interface for integral schemes. The definition is phrased on affine charts, and the basic stalk consequence is recorded here so that normalization and divisor developments can share the same notion without importing one another.

Imports3

Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Normalization
Mathlib.RingTheory.LocalProperties.IntegrallyClosed

Imported by17

class

IsNormalIntegral

L30 ↗

AlgebraicGeometry.IsNormalIntegral

Documentation

An integral scheme is normal when its nonempty affine charts are integrally closed.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · full declaration

class IsNormalIntegral (X : Scheme.{u}) [IsIntegral X] : Prop where
  /-- The section ring of every nonempty affine chart is integrally closed. -/
  isIntegrallyClosed (U : X.Opens) (hU : IsAffineOpen U) [Nonempty U] :
    IsIntegrallyClosed Γ(X, U)

theorem

affine_isIntegrallyClosed

L39 ↗

AlgebraicGeometry.IsNormalIntegral.affine_isIntegrallyClosed

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace IsNormalIntegral
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]

Lean source · statement

theorem affine_isIntegrallyClosed (U : X.Opens) (hU : IsAffineOpen U) [Nonempty U] :
    IsIntegrallyClosed Γ(X, U)

theorem

stalk_isIntegrallyClosed

L44 ↗

AlgebraicGeometry.IsNormalIntegral.stalk_isIntegrallyClosed

Documentation

Every local ring of a normal integral scheme is integrally closed.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace IsNormalIntegral
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]

Lean source · statement

theorem stalk_isIntegrallyClosed (x : X) :
    IsIntegrallyClosed (X.presheaf.stalk x)

instance

(anonymous instance)

L62 ↗

Documentation

A nonempty open subscheme of a normal integral scheme is normal.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace IsNormalIntegral
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]

Lean source · full declaration

instance {U : X.Opens} [Nonempty U] : IsNormalIntegral U where
  isIntegrallyClosed V hV := by
    intro hVnonempty
    let : Nonempty V := hVnonempty
    let W : X.Opens := U.ι ''ᵁ V
    have hW : IsAffineOpen W := hV.image_of_isOpenImmersion U.ι
    let : Nonempty W := by
      obtain ⟨v⟩ := (inferInstance : Nonempty V)
      exact ⟨⟨U.ι.base v.1, ⟨v.1, v.2, rfl⟩⟩⟩
    let : IsIntegrallyClosed Γ(X, W) :=
      IsNormalIntegral.affine_isIntegrallyClosed W hW
    exact IsIntegrallyClosed.of_equiv
      (U.ι.appIso V).commRingCatIsoToRingEquiv

theorem

of_stalks

L80 ↗

AlgebraicGeometry.IsNormalIntegral.of_stalks

Documentation

An integral scheme is normal if all of its local rings are integrally closed. This is the stalkwise constructor for IsNormalIntegral.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · full declaration

theorem IsNormalIntegral.of_stalks
    (X : Scheme.{u}) [IsIntegral X]
    (h : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x)) :
    IsNormalIntegral X where
  isIntegrallyClosed U hU := by
    intro hUnonempty
    let : Nonempty U := hUnonempty
    apply IsIntegrallyClosed.of_isLocalization_maximal
      (fun P [_] ↦ Localization.AtPrime P)
    intro P hP
    let : P.IsMaximal := hP
    let : P.IsPrime := hP.isPrime
    let y : PrimeSpectrum Γ(X, U) := ⟨P, inferInstance⟩
    let x : X := hU.fromSpec y
    have hxU : x ∈ U := (hU.isoSpec.inv y).2
    let : IsIntegrallyClosed (X.presheaf.stalk x) := h x
    let : Algebra Γ(X, U) (X.presheaf.stalk x) :=
      (X.presheaf.germ U x hxU).hom.toAlgebra
    let : IsLocalization.AtPrime (X.presheaf.stalk x) P := by
      exact hU.isLocalization_stalk' y hxU
    let e : Localization.AtPrime P ≃ₐ[Γ(X, U)] X.presheaf.stalk x :=
      IsLocalization.algEquiv P.primeCompl
        (Localization.AtPrime P) (X.presheaf.stalk x)
    exact IsIntegrallyClosed.of_equiv e.symm.toRingEquiv

theorem

of_isAffine

L111 ↗

AlgebraicGeometry.IsNormalIntegral.of_isAffine

Documentation

An integral affine scheme whose ring of global sections is integrally closed is normal.

For an affine open U, normality of Γ(X, U) is checked at maximal ideals. The corresponding localizations are the stalks of X; those stalks are localizations of the integrally closed ring Γ(X, ⊤).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · full declaration

theorem IsNormalIntegral.of_isAffine
    (X : Scheme.{u}) [IsIntegral X] [IsAffine X]
    [IsIntegrallyClosed Γ(X, ⊤)] :
    IsNormalIntegral X where
  isIntegrallyClosed U hU := by
    intro hUnonempty
    let : Nonempty U := hUnonempty
    apply IsIntegrallyClosed.of_isLocalization_maximal
      (fun P [_] ↦ Localization.AtPrime P)
    intro P hP
    let : P.IsMaximal := hP
    let : P.IsPrime := hP.isPrime
    let y : PrimeSpectrum Γ(X, U) := ⟨P, inferInstance⟩
    let x : X := hU.fromSpec y
    have hxU : x ∈ U := (hU.isoSpec.inv y).2
    let xTop : (⊤ : X.Opens) := ⟨x, by simp⟩
    let : Algebra Γ(X, ⊤) (X.presheaf.stalk x) :=
      (X.presheaf.germ ⊤ x (by simp)).hom.toAlgebra
    let : IsLocalization.AtPrime (X.presheaf.stalk x)
        ((isAffineOpen_top X).primeIdealOf xTop).asIdeal :=
      (isAffineOpen_top X).isLocalization_stalk xTop
    have hxNormal : IsIntegrallyClosed (X.presheaf.stalk x) :=
      isIntegrallyClosed_of_isLocalization
        (X.presheaf.stalk x)
        ((isAffineOpen_top X).primeIdealOf xTop).asIdeal.primeCompl
        ((isAffineOpen_top X).primeIdealOf
          xTop).asIdeal.primeCompl_le_nonZeroDivisors
    let : IsIntegrallyClosed (X.presheaf.stalk x) := hxNormal
    let : Algebra Γ(X, U) (X.presheaf.stalk x) :=
      (X.presheaf.germ U x hxU).hom.toAlgebra
    let : IsLocalization.AtPrime (X.presheaf.stalk x) P := by
      exact hU.isLocalization_stalk' y hxU
    let e : Localization.AtPrime P ≃ₐ[Γ(X, U)] X.presheaf.stalk x :=
      IsLocalization.algEquiv P.primeCompl
        (Localization.AtPrime P) (X.presheaf.stalk x)
    exact IsIntegrallyClosed.of_equiv e.symm.toRingEquiv

instance

isNormalIntegral_spec

L150 ↗

AlgebraicGeometry.isNormalIntegral_spec

Documentation

The spectrum of an integrally closed domain is a normal integral scheme.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

instance isNormalIntegral_spec (R : CommRingCat.{u})
    [IsDomain R] [IsIntegrallyClosed R] :
    IsNormalIntegral (Spec R)

Module documentation

Normal integral schemes

Declarations

IsNormalIntegral

affine_isIntegrallyClosed

stalk_isIntegrallyClosed

(anonymous instance)

of_stalks

of_isAffine

isNormalIntegral_spec