NYLL
Module

PuncturedSpectrumDimensionTwoPurity.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumDimensionTwoPurity
6 declarations indexed from sourceView source ↗

Module documentation

Purity for two-dimensional regular local punctures

This file algebraizes connected finite-etale covers of the punctured spectrum by normalizing the full spectrum in their function fields. The normalization is finite etale by the two-dimensional integral-closure theorem, and its restriction is identified with the original connected cover. Finite coproduct decomposition then handles arbitrary covers.

Imports4
Imported by2

Declarations

theorem

puncturedSpectrum_nonempty_dimension_two'

L33 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrum_nonempty_dimension_two'
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsRegularLocalRing R]
Lean source · statement
theorem puncturedSpectrum_nonempty_dimension_two'
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    Nonempty (Scheme.puncturedSpectrum R)
theorem

puncturedSpectrumFunctionFieldRingEquiv_apply_germ

L42 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumFunctionFieldRingEquiv_apply_germ
Documentation

The function-field equivalence induced by the punctured open immersion intertwines germs of global sections.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsRegularLocalRing R]
Lean source · full declaration
theorem puncturedSpectrumFunctionFieldRingEquiv_apply_germ
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (r : Γ(Spec (.of R), ⊤)) :
    let X := Spec (.of R)
    let U := Scheme.puncturedSpectrum R
    let j : U ⟶ X := Scheme.puncturedSpectrumInclusion R
    letI : Nonempty U :=
      Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim R hpos
    letI : IsOpenImmersion j := by
      dsimp only [j, Scheme.puncturedSpectrumInclusion]
      infer_instance
    letI : IsIntegral U := isIntegral_of_isOpenImmersion j
    letI : Nonempty (⊤ : X.Opens) :=
      ⟨⟨genericPoint X, by trivial⟩⟩
    letI : Algebra R X.functionField :=
      AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
    letI : Nonempty (⊤ : U.Opens) :=
      ⟨⟨genericPoint U, by trivial⟩⟩
    puncturedSpectrumFunctionFieldRingEquivOfPositiveDimension R hpos
        (X.germToFunctionField ⊤ r) =
      U.germToFunctionField ⊤ (j.appTop r) := by
  dsimp only
  let X := Spec (.of R)
  let U := Scheme.puncturedSpectrum R
  let j : U ⟶ X := Scheme.puncturedSpectrumInclusion R
  let : Nonempty U :=
    Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim R hpos
  let : IsOpenImmersion j := by
    dsimp only [j, Scheme.puncturedSpectrumInclusion]
    infer_instance
  let : IsIntegral U := isIntegral_of_isOpenImmersion j
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨genericPoint X, by trivial⟩⟩
  let : Algebra R X.functionField :=
    AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
  let : Nonempty (⊤ : U.Opens) :=
    ⟨⟨genericPoint U, by trivial⟩⟩
  let hgen : j (genericPoint U) = genericPoint X :=
    genericPoint_eq_of_isOpenImmersion j
  change j.stalkMap (genericPoint U)
      ((X.presheaf.stalkCongr (.of_eq hgen.symm)).hom
        (X.germToFunctionField ⊤ r)) =
    U.germToFunctionField ⊤ (j.appTop r)
  simp only [TopCat.Presheaf.stalkCongr_hom]
  have htransport :
      X.presheaf.stalkSpecializes
          (Inseparable.of_eq hgen.symm).ge
          (X.presheaf.germ ⊤ (genericPoint X) (by trivial) r) =
        X.presheaf.germ ⊤ (j (genericPoint U)) (by trivial) r := by
    exact DFunLike.congr_fun
      (CommRingCat.hom_ext_iff.mp
        (X.presheaf.germ_stalkSpecializes
          (show genericPoint X ∈ (⊤ : X.Opens) by trivial)
          (Inseparable.of_eq hgen.symm).ge)) r
  rw [htransport]
  exact j.germ_stalkMap_apply (⊤ : X.Opens) (genericPoint U)
    (by trivial) r
theorem

specFunctionField_algebraMap_ΓSpecIso_hom

L103 ↗
AlgebraicGeometry.FiniteEtale.specFunctionField_algebraMap_ΓSpecIso_hom
Documentation

The literal fraction-field algebra on an affine spectrum is the germ of global sections, after the standard global-sections equivalence.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsRegularLocalRing R]
omit [IsRegularLocalRing R] in
Lean source · full declaration
theorem specFunctionField_algebraMap_ΓSpecIso_hom
    (r : Γ(Spec (.of R), ⊤)) :
    let X := Spec (.of R)
    letI : Nonempty (⊤ : X.Opens) :=
      ⟨⟨genericPoint X, by trivial⟩⟩
    letI : Algebra R X.functionField :=
      AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
    algebraMap R X.functionField ((Scheme.ΓSpecIso (.of R)).hom r) =
      X.germToFunctionField ⊤ r := by
  dsimp only
  let X := Spec (.of R)
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨genericPoint X, by trivial⟩⟩
  let : Algebra R X.functionField :=
    AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
  change X.presheaf.germ ⊤ (genericPoint X) (by trivial)
      ((Scheme.ΓSpecIso (.of R)).inv
        ((Scheme.ΓSpecIso (.of R)).hom r)) =
    X.germToFunctionField ⊤ r
  change X.presheaf.germ ⊤ (genericPoint X) (by trivial)
      ((Scheme.ΓSpecIso (.of R)).inv
        ((Scheme.ΓSpecIso (.of R)).hom r)) =
    X.presheaf.germ ⊤ (genericPoint X) (by trivial) r
  exact congrArg (fun s ↦
    X.presheaf.germ ⊤ (genericPoint X) (by trivial) s)
      (Iso.hom_inv_id_apply (Scheme.ΓSpecIso (.of R)) r)
def

connectedPuncturedCoverGenericNormalizationExtension

L132 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCoverGenericNormalizationExtension
Documentation

The normalization of the full local spectrum in the function field of a connected punctured cover, packaged as a finite-etale cover.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsRegularLocalRing R]
Lean source · statement
def connectedPuncturedCoverGenericNormalizationExtension
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W] :
    FiniteEtale (Spec (.of R))
def

connectedPuncturedCoverGenericNormalizationExtensionRestrictionIso

L242 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCoverGenericNormalizationExtensionRestrictionIso
Documentation

A connected punctured cover is canonically the restriction of its function-field normalization over the full spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsRegularLocalRing R]
Lean source · statement
def
    connectedPuncturedCoverGenericNormalizationExtensionRestrictionIso
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W] :
    W ≅ (pullback (Scheme.puncturedSpectrumInclusion R)).obj
      (connectedPuncturedCoverGenericNormalizationExtension R hdim W)
theorem

hasPuncturedPurity_of_isRegularLocalRing_dimension_two

L273 ↗
AlgebraicGeometry.FiniteEtale.hasPuncturedPurity_of_isRegularLocalRing_dimension_two
Documentation

Every finite-etale cover of the punctured spectrum of a two-dimensional regular local domain extends over the full spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsRegularLocalRing R]
Lean source · statement
theorem hasPuncturedPurity_of_isRegularLocalRing_dimension_two
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    HasPuncturedPurity R

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