Module

Localization.lean

Nyll.SchemeTheory.LocalGeometry.HeightOne.Localization

3 declarations indexed from sourceView source ↗

Module documentation

Height-one localizations of regular rings

This file supplies the commutative-algebra entry point needed to apply the existing DVR form of Abhyankar's lemma to a boundary component.

The hypotheses describe geometric source data: a regular affine domain and a codimension-one prime. No ramification, unramifiedness, or unit conclusion is assumed.

Imports4

Nyll.SchemeTheory.RingTheory.RegularLocalDimensionOne
Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.RegularLocalRing.Defs

Imported by6

theorem

isDiscreteValuationRing_localizationAtPrime_of_height_eq_one

L40 ↗

EtaleFundamentalGroups.isDiscreteValuationRing_localizationAtPrime_of_height_eq_one

Documentation

The local ring of a regular affine domain at a height-one prime is a discrete valuation ring.

This is the bridge from a codimension-one boundary component to the DVR input of TameAbhyankar.SGA1. Regularity supplies the cotangent-space dimension of the local ring, while localization identifies its Krull dimension with the height of the chosen prime.

Source context 4 commands

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

namespace EtaleFundamentalGroups
open IsLocalRing
universe u
variable (A : Type u) [CommRing A] [IsDomain A] [IsRegularRing A]

Lean source · statement

theorem isDiscreteValuationRing_localizationAtPrime_of_height_eq_one
    (P : Ideal A) [P.IsPrime] (hP : P.height = 1) :
    IsDiscreteValuationRing (Localization.AtPrime P)

theorem

isDiscreteValuationRing_localizationAtSpan_of_prime

L59 ↗

EtaleFundamentalGroups.isDiscreteValuationRing_localizationAtSpan_of_prime

Documentation

The localization at the principal ideal generated by a prime element of a regular domain is a discrete valuation ring.

Unlike the height-one formulation above, this is the form consumed by a one-component boundary chart: primality of the parameter produces both the prime-ideal instance and the height computation.

Source context 4 commands

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

namespace EtaleFundamentalGroups
open IsLocalRing
universe u
variable (A : Type u) [CommRing A] [IsDomain A] [IsRegularRing A]

Lean source · statement

theorem isDiscreteValuationRing_localizationAtSpan_of_prime
    (t : A) (ht : Prime t) :
    IsDiscreteValuationRing
      (@Localization.AtPrime A _ (Ideal.span {t})
        (Ideal.isPrime_span_singleton_of_prime ht))

def

localizationAtPrimeMapResidueFieldRingEquiv

L72 ↗

EtaleFundamentalGroups.localizationAtPrimeMapResidueFieldRingEquiv

Documentation

Localizing a ring at a prime containing q does not change the residue field at q.

Source context 4 commands

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

namespace EtaleFundamentalGroups
open IsLocalRing
universe u
variable (A : Type u) [CommRing A] [IsDomain A] [IsRegularRing A]

Lean source · full declaration

def localizationAtPrimeMapResidueFieldRingEquiv
    (P q : Ideal A) [P.IsPrime] [q.IsPrime] (hqP : q ≤ P) :
    letI : (q.map (algebraMap A (Localization.AtPrime P))).IsPrime :=
      Ideal.isPrime_map_of_isLocalizationAtPrime P hqP
    q.ResidueField ≃+*
      (q.map (algebraMap A (Localization.AtPrime P))).ResidueField := by
  let V := Localization.AtPrime P
  let qV := q.map (algebraMap A V)
  have hdisjoint : Disjoint ((P.primeCompl : Submonoid A) : Set A) (q : Set A) :=
    Set.disjoint_compl_left_iff_subset.mpr hqP
  letI : qV.IsPrime :=
    IsLocalization.isPrime_of_isPrime_disjoint P.primeCompl V q
      inferInstance hdisjoint
  have hcomap : q = qV.comap (algebraMap A V) := by
    exact (IsLocalization.under_map_of_isPrime_disjoint
      P.primeCompl V (I := q) inferInstance hdisjoint).symm
  exact RingEquiv.ofBijective
    (Ideal.ResidueField.map q qV (algebraMap A V) hcomap)
    (RingHom.SurjectiveOnStalks.residueFieldMap_bijective
      (RingHom.surjectiveOnStalks_of_isLocalization P.primeCompl V)
      q qV hcomap)

Module documentation

Height-one localizations of regular rings

Declarations

isDiscreteValuationRing_localizationAtPrime_of_height_eq_one

isDiscreteValuationRing_localizationAtSpan_of_prime

localizationAtPrimeMapResidueFieldRingEquiv