NYLL
Module

PuncturedSpectrumConnectedNormalizationFinite.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumConnectedNormalizationFinite
3 declarations indexed from sourceView source ↗

Module documentation

Finite connected normalizations across a punctured spectrum

For a connected finite-etale cover of the puncture of a positive-dimensional normal Noetherian local domain, the integral closure in the cover's function field is finite over the local domain. No finite-type hypothesis over ℤ, and no dimension-two hypothesis, is used.

Imports2
Imported by2

Declarations

theorem

connectedPuncturedCover_integralClosure_finite_of_positiveDimension

L33 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCover_integralClosure_finite_of_positiveDimension
Documentation

For a connected finite-etale cover of a positive-dimensional punctured local spectrum, the integral closure of a normal Noetherian local domain in the cover's function field is finite.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R]
Lean source · full declaration
theorem connectedPuncturedCover_integralClosure_finite_of_positiveDimension
    [IsNoetherianRing R] [IsIntegrallyClosed R]
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W] :
    let U := Scheme.puncturedSpectrum R
    letI : Nonempty U :=
      Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim R hpos
    letI : IsOpenImmersion (Scheme.puncturedSpectrumInclusion R) := by
      dsimp only [Scheme.puncturedSpectrumInclusion]
      infer_instance
    letI : IsIntegral U :=
      isIntegral_of_isOpenImmersion (Scheme.puncturedSpectrumInclusion R)
    letI : Algebra R U.functionField :=
      puncturedSpectrumFunctionFieldAlgebraOfPositiveDimension R hpos
    letI : IsFractionRing R U.functionField :=
      puncturedSpectrumFunctionField_isFractionRing_of_positiveDimension R hpos
    letI : IsIntegral W.left :=
      EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
    letI : Algebra U.functionField W.left.functionField :=
      EtaleFundamentalGroups.finiteEtaleFunctionFieldAlgebra W
    letI : Algebra R W.left.functionField :=
      ((algebraMap U.functionField W.left.functionField).comp
        (algebraMap R U.functionField)).toAlgebra
    letI : IsScalarTower R U.functionField W.left.functionField :=
      IsScalarTower.of_algebraMap_eq' rfl
    letI : FiniteDimensional U.functionField W.left.functionField :=
      EtaleFundamentalGroups.finiteDimensional_functionField_of_finiteEtale_isConnected W
    letI : Algebra.IsSeparable U.functionField W.left.functionField :=
      EtaleFundamentalGroups.isSeparable_functionField_of_finiteEtale_isConnected W
    Module.Finite R (integralClosure R W.left.functionField) := by
  dsimp only
  let U := Scheme.puncturedSpectrum R
  let : Nonempty U :=
    Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim R hpos
  let : IsOpenImmersion (Scheme.puncturedSpectrumInclusion R) := by
    dsimp only [Scheme.puncturedSpectrumInclusion]
    infer_instance
  let : IsIntegral U :=
    isIntegral_of_isOpenImmersion (Scheme.puncturedSpectrumInclusion R)
  let K : Type u := U.functionField
  let : Algebra R K :=
    puncturedSpectrumFunctionFieldAlgebraOfPositiveDimension R hpos
  let : IsFractionRing R K :=
    puncturedSpectrumFunctionField_isFractionRing_of_positiveDimension R hpos
  let : IsIntegral W.left :=
    EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
  let L : Type u := W.left.functionField
  let : Algebra K L :=
    EtaleFundamentalGroups.finiteEtaleFunctionFieldAlgebra W
  let : Algebra R L :=
    ((algebraMap K L).comp (algebraMap R K)).toAlgebra
  let : IsScalarTower R K L := IsScalarTower.of_algebraMap_eq' rfl
  let : FiniteDimensional K L :=
    EtaleFundamentalGroups.finiteDimensional_functionField_of_finiteEtale_isConnected W
  let : Algebra.IsSeparable K L :=
    EtaleFundamentalGroups.isSeparable_functionField_of_finiteEtale_isConnected W
  exact IsIntegralClosure.finite R K L (integralClosure R L)
def

connectedPuncturedCoverIntegralClosureOverOfPositiveDimension

L93 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCoverIntegralClosureOverOfPositiveDimension
Documentation

The integral-closure normalization of a connected finite-etale cover of the puncture, as an actual scheme over the full local spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R]
Lean source · statement
def
    connectedPuncturedCoverIntegralClosureOverOfPositiveDimension
    [IsNoetherianRing R] [IsIntegrallyClosed R]
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W] :
    Over (Spec (.of R))
theorem

connectedPuncturedCoverIntegralClosureOver_hom_isFinite

L122 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCoverIntegralClosureOver_hom_isFinite
Documentation

The connected punctured-cover normalization is finite over the full local spectrum in every positive dimension.

Source context 6 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R]
Lean source · statement
theorem connectedPuncturedCoverIntegralClosureOver_hom_isFinite
    [IsNoetherianRing R] [IsIntegrallyClosed R]
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W] :
    IsFinite
      (connectedPuncturedCoverIntegralClosureOverOfPositiveDimension
        R hpos W).hom

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