Module

DimensionTwoIntegralClosure.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.DimensionTwoIntegralClosure

3 declarations indexed from sourceView source ↗

Module documentation

Freeness of a finite normalization over a two-parameter local ring

A regular pair in a domain is nonzero. For a finite normalization in a finite separable field extension, trace-dual saturation makes the same pair regular on the normalization. If the pair generates the maximal ideal, the two-parameter freeness criterion then makes the normalization a free, hence flat, module over the base. No factoriality, normality of the base, or primality hypothesis on a chosen parameter is needed.

Imports2

Imported by3

theorem

regular_pair_nonzero_and_isRelPrime

L34 ↗

EtaleFundamentalGroups.SpecialLocalPurity.regular_pair_nonzero_and_isRelPrime

Documentation

A two-element regular sequence in a domain consists of nonzero, relatively-prime elements.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open scoped Pointwise
open IsLocalRing
open RingTheory.Sequence
universe u v w

Lean source · statement

theorem regular_pair_nonzero_and_isRelPrime
    {A : Type u} [CommRing A] [IsDomain A] {x y : A}
    (hregular : IsRegular A [x, y]) :
    x ≠ 0 ∧ y ≠ 0 ∧ IsRelPrime x y

theorem

integralClosure_free_of_regular_pair

L86 ↗

EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_free_of_regular_pair

Documentation

A finite normalization is free over a Noetherian local domain whose maximal ideal is generated by a regular pair.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open scoped Pointwise
open IsLocalRing
open RingTheory.Sequence
universe u v w

Lean source · statement

theorem integralClosure_free_of_regular_pair
    {A : Type u} {K : Type v} {L : Type w}
    [CommRing A] [IsDomain A]
    [IsLocalRing A] [IsNoetherianRing 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]
    [Module.Finite A (integralClosure A L)]
    {x y : A} (hregular : IsRegular A [x, y])
    (hspan : Ideal.ofList [x, y] = maximalIdeal A) :
    Module.Free A (integralClosure A L)

theorem

integralClosure_flat_of_regular_pair

L134 ↗

EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_flat_of_regular_pair

Documentation

The finite normalization in the preceding theorem is flat over the base.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open scoped Pointwise
open IsLocalRing
open RingTheory.Sequence
universe u v w

Lean source · statement

theorem integralClosure_flat_of_regular_pair
    {A : Type u} {K : Type v} {L : Type w}
    [CommRing A] [IsDomain A]
    [IsLocalRing A] [IsNoetherianRing 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]
    [Module.Finite A (integralClosure A L)]
    {x y : A} (hregular : IsRegular A [x, y])
    (hspan : Ideal.ofList [x, y] = maximalIdeal A) :
    Module.Flat A (integralClosure A L)

Module documentation

Freeness of a finite normalization over a two-parameter local ring

Declarations

regular_pair_nonzero_and_isRelPrime

integralClosure_free_of_regular_pair

integralClosure_flat_of_regular_pair