NYLL
Module

PuncturedSpectrumConnectedLefschetzAlgebra.lean

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

Module documentation

Algebraic inputs for connected hypersurface restrictions

This file records the completeness and codimension properties of the finite integral-closure model attached to a connected finite-etale cover of a punctured local spectrum. These are the algebraic inputs preceding the connectedness theorem for a punctured hypersurface.

No connectedness conclusion is assumed here.

Imports2
Imported by4

Declarations

theorem

isAdicComplete_map_of_moduleFinite_of_le_maximalIdeal

L32 ↗
AlgebraicGeometry.FiniteEtale.isAdicComplete_map_of_moduleFinite_of_le_maximalIdeal
Documentation

A finite algebra over a complete Noetherian local ring is complete for the extension of every ideal contained in the maximal ideal.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · statement
theorem isAdicComplete_map_of_moduleFinite_of_le_maximalIdeal
    {R : Type u} {C : Type v} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] [CommRing C] [Algebra R C] [Module.Finite R C]
    [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    IsAdicComplete (I.map (algebraMap R C)) C
theorem

integralClosure_faithfulSMul_of_fractionField

L49 ↗
AlgebraicGeometry.FiniteEtale.integralClosure_faithfulSMul_of_fractionField
Documentation

The integral closure in a field extension of a fraction field is a faithful algebra over the base domain.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · statement
theorem integralClosure_faithfulSMul_of_fractionField
    {R K L : Type u} [CommRing R] [IsDomain R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L] :
    FaithfulSMul R (integralClosure R L)
theorem

prime_height_eq_ringKrullDim_of_map_maximalIdeal_le

L71 ↗
AlgebraicGeometry.FiniteEtale.prime_height_eq_ringKrullDim_of_map_maximalIdeal_le
Documentation

In a faithfully integral domain extension of an integrally closed local domain, a prime above the maximal ideal has the same height as the maximal ideal.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · statement
theorem prime_height_eq_ringKrullDim_of_map_maximalIdeal_le
    {R : Type u} {C : Type v} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsIntegrallyClosed R] [CommRing C] [IsDomain C]
    [Algebra R C] [Algebra.IsIntegral R C] [FaithfulSMul R C]
    (P : Ideal C) [P.IsPrime]
    (hP : (maximalIdeal R).map (algebraMap R C) ≤ P) :
    ((P.height : ℕ∞) : WithBot ℕ∞) = ringKrullDim R
theorem

three_le_prime_height_of_map_maximalIdeal_le

L93 ↗
AlgebraicGeometry.FiniteEtale.three_le_prime_height_of_map_maximalIdeal_le
Documentation

Codimension-three form of prime_height_eq_ringKrullDim_of_map_maximalIdeal_le.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · statement
theorem three_le_prime_height_of_map_maximalIdeal_le
    {R : Type u} {C : Type v} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsIntegrallyClosed R] [CommRing C] [IsDomain C]
    [Algebra R C] [Algebra.IsIntegral R C] [FaithfulSMul R C]
    (hdim : ((3 : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim R)
    (P : Ideal C) [P.IsPrime]
    (hP : (maximalIdeal R).map (algebraMap R C) ≤ P) :
    ((3 : ℕ∞) : WithBot ℕ∞) ≤ ((P.height : ℕ∞) : WithBot ℕ∞)
theorem

connectedPuncturedCover_integralClosure_isAdicComplete

L106 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCover_integralClosure_isAdicComplete
Documentation

The integral-closure model of a connected punctured cover is complete along the extension of every ideal contained in the maximal ideal.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · full declaration
theorem connectedPuncturedCover_integralClosure_isAdicComplete
    {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]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    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
    IsAdicComplete
      (I.map (algebraMap R (integralClosure R W.left.functionField)))
      (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 isAdicComplete_map_of_moduleFinite_of_le_maximalIdeal I hI
theorem

connectedPuncturedCover_integralClosure_three_le_prime_height

L168 ↗
AlgebraicGeometry.FiniteEtale.connectedPuncturedCover_integralClosure_three_le_prime_height
Documentation

Every prime of the connected-cover integral closure above the closed point has codimension at least three when the base has dimension at least three.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u v
Lean source · full declaration
theorem connectedPuncturedCover_integralClosure_three_le_prime_height
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R] [IsIntegrallyClosed R]
    (hdim : ((3 : ℕ∞) : 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
        (show (1 : WithBot ℕ∞) ≤ ringKrullDim R from le_trans (by norm_num) hdim)
    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
        (show (1 : WithBot ℕ∞) ≤ ringKrullDim R from le_trans (by norm_num) hdim)
    letI : IsFractionRing R U.functionField :=
      puncturedSpectrumFunctionField_isFractionRing_of_positiveDimension R
        (show (1 : WithBot ℕ∞) ≤ ringKrullDim R from le_trans (by norm_num) hdim)
    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
    ∀ (P : Ideal (integralClosure R W.left.functionField))
      [P.IsPrime],
      (maximalIdeal R).map
          (algebraMap R (integralClosure R W.left.functionField)) ≤ P →
        ((3 : ℕ∞) : WithBot ℕ∞) ≤
          ((P.height : ℕ∞) : WithBot ℕ∞) := by
  dsimp only
  have hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R :=
    le_trans (by norm_num) hdim
  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 : FaithfulSMul R C :=
    integralClosure_faithfulSMul_of_fractionField (R := R) (K := K) (L := L)
  let : Algebra.IsIntegral R C := integralClosure.AlgebraIsIntegral
  intro P _ hP
  exact three_le_prime_height_of_map_maximalIdeal_le hdim P hP

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