Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.DimensionTwo.IntegralClosure.Unramified

theorem

integralClosure_etale_of_dvr_of_isUnramifiedAt_all_maximalIdeals

EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_etale_of_dvr_of_isUnramifiedAt_all_maximalIdeals

Documentation

The normalization in a finite separable extension of the fraction field of a DVR is etale when it is unramified at every maximal ideal.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v w

Lean source · statement

theorem integralClosure_etale_of_dvr_of_isUnramifiedAt_all_maximalIdeals
    {V : Type u} {K : Type v} {L : Type w}
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    [Field L] [Algebra V L] [Algebra K L] [IsScalarTower V K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (hunramified : ∀ (Q : Ideal (integralClosure V L)) [Q.IsMaximal],
      Algebra.IsUnramifiedAt V Q) :
    Algebra.Etale V (integralClosure V L)

theorem

integralClosure_etale_of_isRegularLocalRing_dimension_two_of_unramifiedAt_height_one

L52 ↗

EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_etale_of_isRegularLocalRing_dimension_two_of_unramifiedAt_height_one

Documentation

A normalization over a two-dimensional regular local domain is etale if, above every height-one prime, its localized normalization is unramified at all maximal ideals.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v w

Lean source · full declaration

theorem integralClosure_etale_of_isRegularLocalRing_dimension_two_of_unramifiedAt_height_one
    {A : Type u} {K : Type v} {L : Type w}
    [CommRing A] [IsDomain A] [IsRegularLocalRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (hdim : ringKrullDim A = ((2 : ℕ∞) : WithBot ℕ∞))
    (hunramified : ∀ (q : Ideal A) [q.IsPrime], q.height = 1 →
      letI := EtaleFundamentalGroups.localizationAtPrimeToExtensionAlgebra
        (K := K) (L := L) q
      ∀ (Q : Ideal (integralClosure (Localization.AtPrime q) L))
        [Q.IsMaximal],
        Algebra.IsUnramifiedAt (Localization.AtPrime q) Q) :
    Algebra.Etale A (integralClosure A L) := by
  apply integralClosure_etale_of_isRegularLocalRing_dimension_two
    (K := K) hdim
  intro q _ hq
  let V := Localization.AtPrime q
  let : Algebra V K :=
    EtaleFundamentalGroups.localizationAtPrimeToFractionFieldAlgebra
      (K := K) q
  let : IsFractionRing V K :=
    EtaleFundamentalGroups.localizationAtPrimeToFractionField_isFractionRing
      (K := K) q
  let : Algebra V L :=
    EtaleFundamentalGroups.localizationAtPrimeToExtensionAlgebra
      (K := K) (L := L) q
  let : IsScalarTower V K L :=
    EtaleFundamentalGroups.localizationAtPrimeToFractionFieldToExtension_isScalarTower
      (K := K) (L := L) q
  have : IsDiscreteValuationRing V :=
    (open _root_.EtaleFundamentalGroups in
      isDiscreteValuationRing_localizationAtPrime_of_isRegularLocalRing_dimension_two
        hdim q hq)
  have hlocal : Algebra.Etale V (integralClosure V L) :=
    integralClosure_etale_of_dvr_of_isUnramifiedAt_all_maximalIdeals
      (V := V) (K := K) (L := L)
      (hunramified q hq)
  exact
    EtaleFundamentalGroups.localization_integralClosure_etale_of_local_integralClosure_etale
      (K := K) (L := L) q hlocal

Unramified.lean

Module documentation

Codimension-one unramifiedness and two-dimensional purity

integralClosure_etale_of_dvr_of_isUnramifiedAt_all_maximalIdeals

integralClosure_etale_of_isRegularLocalRing_dimension_two_of_unramifiedAt_height_one

Module documentation

Codimension-one unramifiedness and two-dimensional purity

Declarations

integralClosure_etale_of_dvr_of_isUnramifiedAt_all_maximalIdeals

integralClosure_etale_of_isRegularLocalRing_dimension_two_of_unramifiedAt_height_one