Module

PairPrimeDichotomy.lean

Nyll.EtaleFundamentalGroups.Kummer.LocalGeometry.Regular.PairPrimeDichotomy

11 declarations indexed from sourceView source ↗

Module documentation

Prime ideals containing one member of a regular pair

In a two-dimensional regular local ring presented by a regular parameter pair, every prime containing the first parameter is either its principal height-one prime or the closed point. This elementary dichotomy is useful after maximal-adic completion: contraction to the original non-closed branch rules out the second alternative and hence identifies the completed branch without a formal-fibre comparison hypothesis.

Imports3

Mathlib.RingTheory.KrullDimension.Zero
Nyll.EtaleFundamentalGroups.Kummer.LocalGeometry.HeightTwo.MaximalAdicCompletionGeometry
Nyll.SchemeTheory.LocalGeometry.RegularLocal.SystemDomain

Imported by4

theorem

completionQuotientFirstRegularParameter_isDomain

L33 ↗

EtaleFundamentalGroups.Kummer.completionQuotientFirstRegularParameter_isDomain

Documentation

Domainhood needed to state the DVR structure on the completed parameter quotient.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · full declaration

theorem completionQuotientFirstRegularParameter_isDomain
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {x y : R}
    (hreg : IsRegular R [x, y])
    (hgen : Ideal.ofList [x, y] = maximalIdeal R) :
    let Rhat := AdicCompletion (maximalIdeal R) R
    let I := Ideal.span ({x} : Set R)
    IsDomain (Rhat ⧸ I.map (algebraMap R Rhat)) := by
  dsimp only
  let Rhat := AdicCompletion (maximalIdeal R) R
  let I : Ideal R := Ideal.span ({x} : Set R)
  have hIPrime :
      (I.map (algebraMap R Rhat)).IsPrime := by
    simp only [I, Ideal.map_span, Set.image_singleton]
    exact Ideal.isPrime_span_singleton_of_prime
      (prime_first_maximalAdicCompletion_of_regularPair hreg hgen)
  let : (I.map (algebraMap R Rhat)).IsPrime := hIPrime
  exact (Ideal.Quotient.isDomain_iff_prime
    (I.map (algebraMap R Rhat))).mpr inferInstance

theorem

quotientFirstRegularParameter_isDVR

L55 ↗

EtaleFundamentalGroups.Kummer.quotientFirstRegularParameter_isDVR

Documentation

A quotient by the first member of a regular parameter pair is a DVR once its canonical domain structure is installed.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

theorem quotientFirstRegularParameter_isDVR
    {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T]
    {a b : T}
    (hreg : IsRegular T [a, b])
    (hgen : Ideal.ofList [a, b] = maximalIdeal T)
    [IsDomain (T ⧸ Ideal.span ({a} : Set T))] :
    IsDiscreteValuationRing (T ⧸ Ideal.span ({a} : Set T))

theorem

maximalAdicCompletion_of_dvr_isDomain

L105 ↗

EtaleFundamentalGroups.Kummer.maximalAdicCompletion_of_dvr_isDomain

Documentation

The maximal-adic completion of a DVR is a domain, via the standard complete valued-field model.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

theorem maximalAdicCompletion_of_dvr_isDomain
    {T : Type u} [CommRing T] [IsDomain T]
    [IsNoetherianRing T] [IsDiscreteValuationRing T] :
    IsDomain (AdicCompletion (maximalIdeal T) T)

theorem

maximalAdicCompletion_of_dvr_isDVR

L118 ↗

EtaleFundamentalGroups.Kummer.maximalAdicCompletion_of_dvr_isDVR

Documentation

The preceding completed domain carries the transported DVR structure.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

theorem maximalAdicCompletion_of_dvr_isDVR
    {T : Type u} [CommRing T] [IsDomain T]
    [IsNoetherianRing T] [IsDiscreteValuationRing T] :
    @IsDiscreteValuationRing
      (AdicCompletion (maximalIdeal T) T) inferInstance
      (maximalAdicCompletion_of_dvr_isDomain (T := T))

def

completionQuotientRingEquiv

L137 ↗

EtaleFundamentalGroups.Kummer.completionQuotientRingEquiv

Documentation

The tensor/quotient comparison followed by finite base change identifies the completed source quotient with the quotient of the completed source.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

def completionQuotientRingEquiv
    {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T]
    (I : Ideal T) :
    AdicCompletion
        ((maximalIdeal T).map (algebraMap T (T ⧸ I))) (T ⧸ I) ≃+*
      (AdicCompletion (maximalIdeal T) T ⧸
        I.map (algebraMap T (AdicCompletion (maximalIdeal T) T)))

theorem

mappedQuotientCompletion_isDomain

L157 ↗

EtaleFundamentalGroups.Kummer.mappedQuotientCompletion_isDomain

Documentation

The completion at the image of the source maximal ideal is a domain, because that image is the quotient's maximal ideal.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

theorem mappedQuotientCompletion_isDomain
    {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T]
    (I : Ideal T)
    (hSourceDomain : IsDomain (T ⧸ I))
    (hSourceDVR :
      @IsDiscreteValuationRing (T ⧸ I) inferInstance hSourceDomain) :
    IsDomain
      (AdicCompletion
        ((maximalIdeal T).map (algebraMap T (T ⧸ I))) (T ⧸ I))

theorem

mappedQuotientCompletion_isDVR

L182 ↗

EtaleFundamentalGroups.Kummer.mappedQuotientCompletion_isDVR

Documentation

The domain above inherits the DVR structure from the maximal-adic completion of the quotient DVR.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

theorem mappedQuotientCompletion_isDVR
    {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T]
    (I : Ideal T)
    (hSourceDomain : IsDomain (T ⧸ I))
    (hSourceDVR :
      @IsDiscreteValuationRing (T ⧸ I) inferInstance hSourceDomain)
    (hMappedDomain : IsDomain
      (AdicCompletion
        ((maximalIdeal T).map (algebraMap T (T ⧸ I))) (T ⧸ I))) :
    @IsDiscreteValuationRing
      (AdicCompletion
        ((maximalIdeal T).map (algebraMap T (T ⧸ I))) (T ⧸ I))
      inferInstance hMappedDomain

theorem

completionQuotient_isDVR_of_quotientDVR

L218 ↗

EtaleFundamentalGroups.Kummer.completionQuotient_isDVR_of_quotientDVR

Documentation

Completion base change carries a DVR quotient to the corresponding quotient of the maximal-adic completion.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

theorem completionQuotient_isDVR_of_quotientDVR
    {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T]
    (I : Ideal T)
    (hSourceDomain : IsDomain (T ⧸ I))
    (hSourceDVR :
      @IsDiscreteValuationRing (T ⧸ I) inferInstance hSourceDomain)
    (hTargetDomain : IsDomain
      (AdicCompletion (maximalIdeal T) T ⧸
        I.map (algebraMap T (AdicCompletion (maximalIdeal T) T)))) :
    @IsDiscreteValuationRing
      (AdicCompletion (maximalIdeal T) T ⧸
        I.map (algebraMap T (AdicCompletion (maximalIdeal T) T)))
      inferInstance hTargetDomain

theorem

completionQuotientFirstRegularParameter_isDVR_aux

L258 ↗

EtaleFundamentalGroups.Kummer.completionQuotientFirstRegularParameter_isDVR_aux

Documentation

The quotient of the maximal-adic completion by the extension of the first parameter of a regular pair is a DVR.

The source quotient has the one-element regular system given by the second parameter, hence is a DVR. Tensor/quotient compatibility identifies the completed quotient with the maximal-adic completion of that DVR, and the standard valued-field completion model supplies the target DVR structure.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

theorem completionQuotientFirstRegularParameter_isDVR_aux
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {x y : R}
    (hreg : IsRegular R [x, y])
    (hgen : Ideal.ofList [x, y] = maximalIdeal R)
    [IsDomain
      (AdicCompletion (maximalIdeal R) R ⧸
        (Ideal.span ({x} : Set R)).map
          (algebraMap R (AdicCompletion (maximalIdeal R) R)))] :
    IsDiscreteValuationRing
      (AdicCompletion (maximalIdeal R) R ⧸
        (Ideal.span ({x} : Set R)).map
          (algebraMap R (AdicCompletion (maximalIdeal R) R)))

theorem

completionQuotientFirstRegularParameter_isDVR

L306 ↗

EtaleFundamentalGroups.Kummer.completionQuotientFirstRegularParameter_isDVR

Documentation

The quotient of the maximal-adic completion by the extension of the first parameter of a regular pair is a DVR.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · full declaration

theorem completionQuotientFirstRegularParameter_isDVR
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {x y : R}
    (hreg : IsRegular R [x, y])
    (hgen : Ideal.ofList [x, y] = maximalIdeal R) :
    let Rhat := AdicCompletion (maximalIdeal R) R
    let I := Ideal.span ({x} : Set R)
    @IsDiscreteValuationRing
      (Rhat ⧸ I.map (algebraMap R Rhat)) inferInstance
      (completionQuotientFirstRegularParameter_isDomain hreg hgen) := by
  dsimp only
  let : IsDomain
      (AdicCompletion (maximalIdeal R) R ⧸
        (Ideal.span ({x} : Set R)).map
          (algebraMap R (AdicCompletion (maximalIdeal R) R))) :=
    completionQuotientFirstRegularParameter_isDomain hreg hgen
  exact completionQuotientFirstRegularParameter_isDVR_aux hreg hgen

theorem

maximalAdicCompletion_prime_eq_mapped_span_first_of_under_eq

L330 ↗

EtaleFundamentalGroups.Kummer.maximalAdicCompletion_prime_eq_mapped_span_first_of_under_eq

Documentation

A prime of the maximal-adic completion which contracts to the first parameter prime is exactly the extension of that parameter prime.

The quotient by the mapped parameter is a DVR. Thus a strict enlargement would be the closed point, which is excluded by contraction to the original non-closed branch.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

theorem maximalAdicCompletion_prime_eq_mapped_span_first_of_under_eq
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {x y : R}
    (hreg : IsRegular R [x, y])
    (hgen : Ideal.ofList [x, y] = maximalIdeal R)
    (q : Ideal (AdicCompletion (maximalIdeal R) R)) [q.IsPrime]
    (hunder : q.under R = Ideal.span ({x} : Set R)) :
    q = Ideal.span
      ({algebraMap R (AdicCompletion (maximalIdeal R) R) x} :
        Set (AdicCompletion (maximalIdeal R) R))

Module documentation

Prime ideals containing one member of a regular pair

Declarations