Module

PuncturedSpectrum.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrum

5 declarations indexed from sourceView source ↗

Module documentation

Finite étale covers of punctured local spectra

For a local ring R, the punctured spectrum is the complement of its unique closed point. This file supplies the canonical open immersion and packages local purity as essential surjectivity of finite-étale pullback along that immersion. It then connects this exact cover-extension property to the induced map on étale fundamental groups.

The substantive algebraization theorem asserting local purity is deliberately not assumed here under a replacement name: HasPuncturedPurity R is exactly the standard categorical predicate that every finite-étale cover of the punctured spectrum extends, up to isomorphism, over Spec R.

Imports3

Imported by10

def

HasPuncturedPurity

L39 ↗

AlgebraicGeometry.FiniteEtale.HasPuncturedPurity

Documentation

Local purity for a local ring, expressed without a replacement cover category: pullback of finite-étale covers to the canonical punctured spectrum is essentially surjective.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace FiniteEtale

Lean source · statement

def HasPuncturedPurity (R : Type u) [CommRing R] [IsLocalRing R] : Prop

theorem

hasPuncturedPurity_iff

L45 ↗

AlgebraicGeometry.FiniteEtale.hasPuncturedPurity_iff

Documentation

The categorical local-purity predicate says exactly that each finite-étale cover of the punctured spectrum is isomorphic to the restriction of a cover of the full local spectrum.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace FiniteEtale

Lean source · statement

theorem hasPuncturedPurity_iff
    (R : Type u) [CommRing R] [IsLocalRing R] :
    HasPuncturedPurity R ↔
      ∀ Y : FiniteEtale (Scheme.puncturedSpectrum R),
        ∃ X : FiniteEtale (Spec (.of R)),
          Nonempty
            ((pullback (Scheme.puncturedSpectrumInclusion R)).obj X ≅ Y)

def

puncturedSpectrumPullbackFullyFaithful

L62 ↗

AlgebraicGeometry.FiniteEtale.puncturedSpectrumPullbackFullyFaithful

Documentation

On a positive-dimensional normal Noetherian local domain, restriction of finite-etale covers to the punctured spectrum is fully faithful. Thus an extension, when it exists, and every morphism between extensions are uniquely determined on the puncture.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace FiniteEtale

Lean source · statement

def puncturedSpectrumPullbackFullyFaithful
    (R : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsLocalRing R] [IsNoetherianRing R]
    (hdim : (1 : WithBot ℕ∞) ≤ ringKrullDim R) :
    (pullback (Scheme.puncturedSpectrumInclusion R)).FullyFaithful

theorem

fundamentalGroupHom_surjective_puncturedSpectrum

L86 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_surjective_puncturedSpectrum

Documentation

The punctured-spectrum map is always surjective on étale fundamental groups for a positive-dimensional normal Noetherian local domain. This is the unconditional half of local purity: it uses only that the puncture is a nonempty open subscheme.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace FiniteEtale

Lean source · statement

theorem fundamentalGroupHom_surjective_puncturedSpectrum
    (R : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsLocalRing R] [IsNoetherianRing R]
    (hdim : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ Scheme.puncturedSpectrum R) :
    Function.Surjective
      (fundamentalGroupHom (Scheme.puncturedSpectrumInclusion R) xi)

theorem

fundamentalGroupHom_bijective_puncturedSpectrum_of_hasPuncturedPurity

L106 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_bijective_puncturedSpectrum_of_hasPuncturedPurity

Documentation

Local purity together with the usual normality hypotheses identifies the étale fundamental group of a positive-dimensional local spectrum with that of its punctured spectrum. Injectivity is the finite-cover extension criterion; surjectivity is the nonempty-open theorem.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace FiniteEtale

Lean source · statement

theorem fundamentalGroupHom_bijective_puncturedSpectrum_of_hasPuncturedPurity
    (R : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsLocalRing R] [IsNoetherianRing R]
    (hdim : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (hpurity : HasPuncturedPurity R)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ Scheme.puncturedSpectrum R) :
    Function.Bijective
      (fundamentalGroupHom (Scheme.puncturedSpectrumInclusion R) xi)

Module documentation

Finite étale covers of punctured local spectra

Declarations

HasPuncturedPurity

hasPuncturedPurity_iff

puncturedSpectrumPullbackFullyFaithful

fundamentalGroupHom_surjective_puncturedSpectrum

fundamentalGroupHom_bijective_puncturedSpectrum_of_hasPuncturedPurity