NYLL
Module

PuncturedSpectrumNormalizationExtension.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumNormalizationExtension
18 declarations indexed from sourceView source ↗

Module documentation

Relative normalization across a punctured local spectrum

Let W be a finite-etale scheme over the punctured spectrum of a Noetherian local ring. This file constructs the relative normalization of the full local spectrum in the composite morphism from W. The resulting morphism is integral, its pullback to the punctured spectrum is finite etale, and that pullback is canonically isomorphic to W over the punctured spectrum.

No global finiteness or etaleness of the normalization morphism is asserted here. Those are separate algebraic inputs in a purity argument.

Imports3
Imported by2

Declarations

theorem

puncturedSpectrumInclusion_isOpenImmersion

L34 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumInclusion_isOpenImmersion
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem puncturedSpectrumInclusion_isOpenImmersion
    (R : Type u) [CommRing R] [IsLocalRing R] :
    IsOpenImmersion (Scheme.puncturedSpectrumInclusion R)
def

puncturedSpectrumCoverToSpec

L42 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumCoverToSpec
Documentation

The composite morphism from a finite-etale punctured cover to the full local spectrum.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumCoverToSpec
    (R : Type u) [CommRing R] [IsLocalRing R]
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    W.left ⟶ Spec (.of R)
theorem

puncturedSpectrumComposite_quasiCompact

L48 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumComposite_quasiCompact
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem puncturedSpectrumComposite_quasiCompact
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    QuasiCompact (puncturedSpectrumCoverToSpec R W)
theorem

puncturedSpectrumComposite_quasiSeparated

L63 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumComposite_quasiSeparated
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumComposite_quasiSeparated
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    QuasiSeparated (puncturedSpectrumCoverToSpec R W)
def

puncturedSpectrumNormalizationExtension

L81 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtension
Documentation

The relative normalization of the full local spectrum in a finite-etale cover of its punctured spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
def puncturedSpectrumNormalizationExtension
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) : Scheme
def

puncturedSpectrumNormalizationExtensionHom

L87 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtensionHom
Documentation

The canonical morphism from the punctured-spectrum normalization candidate to the full local spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
def puncturedSpectrumNormalizationExtensionHom
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    puncturedSpectrumNormalizationExtension R W ⟶ Spec (.of R)
def

puncturedSpectrumToNormalizationExtension

L94 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumToNormalizationExtension
Documentation

The original punctured cover maps canonically to the relative normalization candidate.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
def puncturedSpectrumToNormalizationExtension
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    W.left ⟶ puncturedSpectrumNormalizationExtension R W
theorem

puncturedSpectrumToNormalizationExtension_comp_extensionHom

L102 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumToNormalizationExtension_comp_extensionHom
Documentation

The normalization candidate really extends the composite morphism from the punctured cover to the full local spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
theorem puncturedSpectrumToNormalizationExtension_comp_extensionHom
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    puncturedSpectrumToNormalizationExtension R W ≫
        puncturedSpectrumNormalizationExtensionHom R W =
      W.hom ≫ Scheme.puncturedSpectrumInclusion R
theorem

puncturedSpectrumNormalizationExtensionHom_isIntegral

L110 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtensionHom_isIntegral
Documentation

The normalization extension morphism is integral.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
theorem puncturedSpectrumNormalizationExtensionHom_isIntegral
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    IsIntegralHom (puncturedSpectrumNormalizationExtensionHom R W)
theorem

puncturedSpectrumNormalizationExtension_isAffine

L119 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtension_isAffine
Documentation

The normalization candidate is affine. Thus its global sections form the actual integral algebra candidate over the local base.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
theorem puncturedSpectrumNormalizationExtension_isAffine
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    IsAffine (puncturedSpectrumNormalizationExtension R W)
theorem

puncturedSpectrumNormalizationExtension_appTop_isIntegral

L131 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtension_appTop_isIntegral
Documentation

The ring map on global sections of the normalization candidate is integral.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
theorem puncturedSpectrumNormalizationExtension_appTop_isIntegral
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    (puncturedSpectrumNormalizationExtensionHom R W).appTop.hom.IsIntegral
theorem

puncturedSpectrumNormalizationExtensionHom_isFinite_iff_appTop

L142 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtensionHom_isFinite_iff_appTop
Documentation

Since the normalization candidate is already affine and integral, its remaining global finiteness problem is exactly finiteness of the induced map on global sections.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
theorem puncturedSpectrumNormalizationExtensionHom_isFinite_iff_appTop
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    IsFinite (puncturedSpectrumNormalizationExtensionHom R W) ↔
      (puncturedSpectrumNormalizationExtensionHom R W).appTop.hom.Finite
def

puncturedSpectrumNormalizationExtensionSectionsIso

L163 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtensionSectionsIso
Documentation

On global sections of the affine base, the normalization extension is the integral closure inside the sections of the original composite cover.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · full declaration
def puncturedSpectrumNormalizationExtensionSectionsIso
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    let f := puncturedSpectrumCoverToSpec R W
    letI : Algebra
        Γ(Spec (.of R), (⊤ : (Spec (.of R)).Opens))
        Γ(W.left, (⊤ : W.left.Opens)) :=
      f.appTop.hom.toAlgebra
    Γ(puncturedSpectrumNormalizationExtension R W, ⊤) ≅
      .of (integralClosure
        Γ(Spec (.of R), (⊤ : (Spec (.of R)).Opens))
        Γ(W.left, (⊤ : W.left.Opens))) :=
  (puncturedSpectrumCoverToSpec R W).normalizationObjIso
    (isAffineOpen_top (Spec (.of R)))
def

puncturedSpectrumNormalizationExtensionPullbackIso

L179 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtensionPullbackIso
Documentation

The original cover is canonically isomorphic to the restriction of the normalization candidate to the punctured spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
def puncturedSpectrumNormalizationExtensionPullbackIso
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    W.left ≅ Limits.pullback (puncturedSpectrumNormalizationExtensionHom R W)
      (Scheme.puncturedSpectrumInclusion R)
theorem

puncturedSpectrumNormalizationExtensionPullbackIso_hom_snd

L189 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtensionPullbackIso_hom_snd
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
theorem puncturedSpectrumNormalizationExtensionPullbackIso_hom_snd
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    (puncturedSpectrumNormalizationExtensionPullbackIso R W).hom ≫
        Limits.pullback.snd (puncturedSpectrumNormalizationExtensionHom R W)
          (Scheme.puncturedSpectrumInclusion R) =
      W.hom
theorem

puncturedSpectrumNormalizationExtension_pullback_isFiniteEtale

L202 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtension_pullback_isFiniteEtale
Documentation

The actual restriction morphism of the normalization candidate is finite etale.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
theorem puncturedSpectrumNormalizationExtension_pullback_isFiniteEtale
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    IsFiniteEtale
      (Limits.pullback.snd (puncturedSpectrumNormalizationExtensionHom R W)
        (Scheme.puncturedSpectrumInclusion R))
def

puncturedSpectrumNormalizationExtensionRestriction

L214 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtensionRestriction
Documentation

The restriction of the normalization candidate, packaged as an actual finite-etale object over the punctured spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
def puncturedSpectrumNormalizationExtensionRestriction
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    FiniteEtale (Scheme.puncturedSpectrum R)
def

puncturedSpectrumNormalizationExtensionRestrictionIso

L224 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumNormalizationExtensionRestrictionIso
Documentation

The restriction comparison as an isomorphism in the category of finite-etale objects over the punctured spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
attribute [local instance] puncturedSpectrumComposite_quasiCompact
  puncturedSpectrumComposite_quasiSeparated
Lean source · statement
def puncturedSpectrumNormalizationExtensionRestrictionIso
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    W ≅ puncturedSpectrumNormalizationExtensionRestriction R W

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.