NYLL
Module

PuncturedSpectrumConnectedNormalizationLocal.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumConnectedNormalizationLocal
5 declarations indexed from sourceView source ↗

Module documentation

Locality of connected finite normalizations over complete local rings

A finite domain algebra over a complete Noetherian local ring is local. The proof passes to the closed fibre: completeness lifts idempotents, so the closed fibre is connected; finite-dimensionality makes it Artinian, hence its prime spectrum is discrete and consists of one point. The Jacobson radical comparison for finite algebras then lifts uniqueness of the maximal ideal to the original algebra.

Imports3
Imported by3

Declarations

theorem

isLocalRing_of_isArtinianRing_of_connectedSpace_spec

L32 ↗
AlgebraicGeometry.FiniteEtale.isLocalRing_of_isArtinianRing_of_connectedSpace_spec
Documentation

A nontrivial Artinian ring with connected prime spectrum is local.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · statement
theorem isLocalRing_of_isArtinianRing_of_connectedSpace_spec
    (Q : Type u) [CommRing Q] [IsArtinianRing Q] [Nontrivial Q]
    [ConnectedSpace (PrimeSpectrum Q)] :
    IsLocalRing Q
theorem

isLocalRing_of_finiteDomain_of_maximalAdicComplete

L60 ↗
AlgebraicGeometry.FiniteEtale.isLocalRing_of_finiteDomain_of_maximalAdicComplete
Documentation

A finite domain algebra over a complete Noetherian local ring has a unique maximal ideal.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · statement
theorem isLocalRing_of_finiteDomain_of_maximalAdicComplete
    {R C : Type u}
    [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (maximalIdeal R) R]
    [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C] :
    IsLocalRing C
theorem

ringKrullDim_eq_of_finiteIntegralDomain_of_maximalAdicComplete

L129 ↗
AlgebraicGeometry.FiniteEtale.ringKrullDim_eq_of_finiteIntegralDomain_of_maximalAdicComplete
Documentation

A faithfully integral finite domain over a complete normal local domain has the same Krull dimension as the base.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · statement
theorem ringKrullDim_eq_of_finiteIntegralDomain_of_maximalAdicComplete
    {R C : Type u}
    [CommRing R] [IsDomain R] [IsLocalRing R] [IsNoetherianRing R]
    [IsIntegrallyClosed R] [IsAdicComplete (maximalIdeal R) R]
    [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
    [Algebra.IsIntegral R C] [FaithfulSMul R C] :
    ringKrullDim C = ringKrullDim R
theorem

connectedPuncturedCover_integralClosure_isLocalRing

L160 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCover_integralClosure_isLocalRing
Documentation

The integral-closure algebra attached to a connected finite-etale cover of a positive-dimensional punctured spectrum is local when the base is complete.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · full declaration
theorem connectedPuncturedCover_integralClosure_isLocalRing
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R] [IsIntegrallyClosed R]
    [IsAdicComplete (maximalIdeal R) 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
    IsLocalRing (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 C := integralClosure R L
  let : Module.Finite R C :=
    connectedPuncturedCover_integralClosure_finite_of_positiveDimension
      R hpos W
  exact isLocalRing_of_finiteDomain_of_maximalAdicComplete
    (R := R) (C := C)
theorem

connectedPuncturedCover_integralClosure_ringKrullDim_eq

L219 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCover_integralClosure_ringKrullDim_eq
Documentation

The integral-closure algebra of a connected punctured cover has the same Krull dimension as the complete normal local base.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · full declaration
theorem connectedPuncturedCover_integralClosure_ringKrullDim_eq
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R] [IsIntegrallyClosed R]
    [IsAdicComplete (maximalIdeal R) 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
    ringKrullDim (integralClosure R W.left.functionField) =
      ringKrullDim R := 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 C := integralClosure R L
  let : Module.Finite R C :=
    connectedPuncturedCover_integralClosure_finite_of_positiveDimension
      R hpos W
  let : Algebra.IsIntegral R C := integralClosure.AlgebraIsIntegral
  let : FaithfulSMul R C :=
    integralClosure_faithfulSMul_of_fractionField
      (R := R) (K := K) (L := L)
  exact
    ringKrullDim_eq_of_finiteIntegralDomain_of_maximalAdicComplete
      (R := R) (C := C)

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