NYLL
Module

HeightTwo.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.DimensionTwo.IntegralClosure.HeightTwo
7 declarations indexed from sourceView source ↗

Module documentation

Finite normalizations over a height-two regular local base

The regular-pair freeness theorem can be made input-free in dimension two. A basis of the cotangent space lifts to a regular pair generating the maximal ideal; trace-dual saturation then transports that pair to the finite normalization. Thus a finite normalization in a finite separable extension is free, and hence flat, over the base.

Imports4
Imported by6

Declarations

theorem

integralClosure_finite_of_isRegularLocalRing_dimension_two

L34 ↗
EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_finite_of_isRegularLocalRing_dimension_two
Documentation

A normalization in a finite separable extension of the fraction field of a two-dimensional regular local domain is finite. Normality of the base is produced from regularity and dimension two; finiteness then follows from the trace-dual theorem for separable extensions.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
universe u v w
Lean source · statement
theorem integralClosure_finite_of_isRegularLocalRing_dimension_two
    {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 ℕ∞)) :
    Module.Finite A (integralClosure A L)
theorem

integralClosure_free_of_isRegularLocalRing_dimension_two

L48 ↗
EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_free_of_isRegularLocalRing_dimension_two
Documentation

A finite normalization over a two-dimensional regular local domain is free. The parameter pair is produced internally from the cotangent space.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
universe u v w
Lean source · statement
theorem integralClosure_free_of_isRegularLocalRing_dimension_two
    {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 ℕ∞)) :
    Module.Free A (integralClosure A L)
theorem

integralClosure_flat_of_isRegularLocalRing_dimension_two

L72 ↗
EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_flat_of_isRegularLocalRing_dimension_two
Documentation

A finite normalization over a two-dimensional regular local domain is flat.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
universe u v w
Lean source · statement
theorem integralClosure_flat_of_isRegularLocalRing_dimension_two
    {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 ℕ∞)) :
    Module.Flat A (integralClosure A L)
theorem

integralClosure_finite_localizationAtPrime_of_height_eq_two

L87 ↗
EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_finite_localizationAtPrime_of_height_eq_two
Documentation

At a height-two prime of a regular domain, every normalization in a finite separable extension of the local fraction field is finite.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
universe u v w
Lean source · statement
theorem integralClosure_finite_localizationAtPrime_of_height_eq_two
    {A : Type u} [CommRing A] [IsDomain A] [IsRegularRing A]
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    {K : Type v} {L : Type w}
    [Field K] [Algebra (Localization.AtPrime P) K]
    [IsFractionRing (Localization.AtPrime P) K]
    [Field L] [Algebra (Localization.AtPrime P) L] [Algebra K L]
    [IsScalarTower (Localization.AtPrime P) K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    Module.Finite (Localization.AtPrime P)
      (integralClosure (Localization.AtPrime P) L)
theorem

integralClosure_free_localizationAtPrime_of_height_eq_two

L113 ↗
EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_free_localizationAtPrime_of_height_eq_two
Documentation

At a height-two prime of a regular domain, every finite normalization in a finite separable extension of the local fraction field is free.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
universe u v w
Lean source · statement
theorem integralClosure_free_localizationAtPrime_of_height_eq_two
    {A : Type u} [CommRing A] [IsDomain A] [IsRegularRing A]
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    {K : Type v} {L : Type w}
    [Field K] [Algebra (Localization.AtPrime P) K]
    [IsFractionRing (Localization.AtPrime P) K]
    [Field L] [Algebra (Localization.AtPrime P) L] [Algebra K L]
    [IsScalarTower (Localization.AtPrime P) K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    Module.Free (Localization.AtPrime P)
      (integralClosure (Localization.AtPrime P) L)
theorem

integralClosure_flat_localizationAtPrime_of_height_eq_two

L139 ↗
EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_flat_localizationAtPrime_of_height_eq_two
Documentation

The finite normalization in the preceding height-two localization theorem is flat.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
universe u v w
Lean source · statement
theorem integralClosure_flat_localizationAtPrime_of_height_eq_two
    {A : Type u} [CommRing A] [IsDomain A] [IsRegularRing A]
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    {K : Type v} {L : Type w}
    [Field K] [Algebra (Localization.AtPrime P) K]
    [IsFractionRing (Localization.AtPrime P) K]
    [Field L] [Algebra (Localization.AtPrime P) L] [Algebra K L]
    [IsScalarTower (Localization.AtPrime P) K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    Module.Flat (Localization.AtPrime P)
      (integralClosure (Localization.AtPrime P) L)
theorem

integralClosure_etale_localizationAtPrime_of_height_eq_two

L161 ↗
EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_etale_localizationAtPrime_of_height_eq_two
Documentation

Purity endpoint for a finite normalization at a height-two point: if the normalization is etale after localization at every height-one prime of the local base, then it is already etale over the height-two local base.

Freeness and the regular parameter pair are both produced internally.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
universe u v w
Lean source · statement
theorem integralClosure_etale_localizationAtPrime_of_height_eq_two
    {A : Type u} [CommRing A] [IsDomain A] [IsRegularRing A]
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    {K : Type v} {L : Type w}
    [Field K] [Algebra (Localization.AtPrime P) K]
    [IsFractionRing (Localization.AtPrime P) K]
    [Field L] [Algebra (Localization.AtPrime P) L] [Algebra K L]
    [IsScalarTower (Localization.AtPrime P) K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (hlocal : ∀ (q : Ideal (Localization.AtPrime P)) [q.IsPrime],
      q.height = 1 →
      Algebra.Etale (Localization.AtPrime q)
        (Localization (Algebra.algebraMapSubmonoid
          (integralClosure (Localization.AtPrime P) L) q.primeCompl))) :
    Algebra.Etale (Localization.AtPrime P)
      (integralClosure (Localization.AtPrime P) L)

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