Module

RegularPair.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.HeightTwo.RegularPair

4 declarations indexed from sourceView source ↗

Module documentation

An unconstrained regular parameter pair in dimension two

For the finite-normalization argument we do not need to prescribe the first parameter. In a two-dimensional regular local domain, lift any basis of the cotangent space. The two lifts generate the maximal ideal and form a regular sequence.

The only delicate point is the second regularity condition. After quotienting by the first lift, the maximal ideal is principal. If its generator were a zero-divisor, Krull intersection would make it nilpotent and force the quotient to have dimension zero, contradicting the principal-ideal dimension bound.

Imports5

Mathlib.LinearAlgebra.Dimension.Free
Mathlib.LinearAlgebra.Basis.VectorSpace
Mathlib.RingTheory.Filtration
Mathlib.RingTheory.KrullDimension.Zero
Nyll.SchemeTheory.LocalGeometry.HeightTwo.RegularParameters

Imported by3

theorem

isSMulRegular_of_span_singleton_eq_maximalIdeal_of_not_krullDimLE_zero

L39 ↗

EtaleFundamentalGroups.isSMulRegular_of_span_singleton_eq_maximalIdeal_of_not_krullDimLE_zero

Documentation

In a positive-dimensional Noetherian local ring with principal maximal ideal, a generator of the maximal ideal is a non-zero-divisor.

Source context 6 commands

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

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

Lean source · statement

theorem isSMulRegular_of_span_singleton_eq_maximalIdeal_of_not_krullDimLE_zero
    {S : Type u} [CommRing S] [IsLocalRing S] [IsNoetherianRing S]
    {y : S} (hspan : Ideal.span {y} = maximalIdeal S)
    (hdim : ¬ Ring.KrullDimLE 0 S) :
    IsSMulRegular S y

theorem

isRegular_pair_of_finrank_cotangentSpace_eq_two_of_span_eq

L112 ↗

EtaleFundamentalGroups.isRegular_pair_of_finrank_cotangentSpace_eq_two_of_span_eq

Documentation

In a two-dimensional Noetherian local domain, two minimal generators of the maximal ideal form a regular sequence.

Source context 6 commands

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

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

Lean source · statement

theorem isRegular_pair_of_finrank_cotangentSpace_eq_two_of_span_eq
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    {x y : R}
    (hfin : Module.finrank (ResidueField R) (CotangentSpace R) = 2)
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (hspan : Ideal.ofList [x, y] = maximalIdeal R) :
    IsRegular R [x, y]

theorem

exists_regular_pair_of_finrank_cotangentSpace_eq_two_unconstrained

L219 ↗

EtaleFundamentalGroups.exists_regular_pair_of_finrank_cotangentSpace_eq_two_unconstrained

Documentation

A two-dimensional regular local domain admits a regular pair generating its maximal ideal, with no prescribed first parameter.

Source context 6 commands

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

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

Lean source · statement

theorem exists_regular_pair_of_finrank_cotangentSpace_eq_two_unconstrained
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (hfin : Module.finrank (ResidueField R) (CotangentSpace R) = 2)
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    ∃ x y : R, IsRegular R [x, y] ∧
      Ideal.ofList [x, y] = maximalIdeal R

theorem

exists_regular_pair_localizationAtPrime_of_height_eq_two_unconstrained

L282 ↗

EtaleFundamentalGroups.exists_regular_pair_localizationAtPrime_of_height_eq_two_unconstrained

Documentation

A height-two localization of a regular domain has an unconstrained regular pair of parameters.

Source context 6 commands

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

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

Lean source · statement

theorem exists_regular_pair_localizationAtPrime_of_height_eq_two_unconstrained
    {A : Type u} [CommRing A] [IsDomain A] [IsRegularRing A]
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2) :
    ∃ x y : Localization.AtPrime P,
      IsRegular (Localization.AtPrime P) [x, y] ∧
      Ideal.ofList [x, y] =
        maximalIdeal (Localization.AtPrime P)

Module documentation

An unconstrained regular parameter pair in dimension two

Declarations

isSMulRegular_of_span_singleton_eq_maximalIdeal_of_not_krullDimLE_zero

isRegular_pair_of_finrank_cotangentSpace_eq_two_of_span_eq

exists_regular_pair_of_finrank_cotangentSpace_eq_two_unconstrained

exists_regular_pair_localizationAtPrime_of_height_eq_two_unconstrained