Module

RegularParameters.lean

Nyll.SchemeTheory.LocalGeometry.HeightTwo.RegularParameters

2 declarations indexed from sourceView source ↗

Module documentation

A prescribed first parameter in dimension two

In a two-dimensional regular local ring, an element whose cotangent class is nonzero can be completed to a minimal pair of generators of the maximal ideal. If the prescribed element is prime, the resulting pair is a regular sequence.

The localization theorem at the end obtains the cotangent dimension directly from regularity and the height of the source prime. The only extra datum it needs is the geometric transversality statement that the prescribed local equation does not lie in the square of the localized maximal ideal.

Imports4

Mathlib.LinearAlgebra.Dimension.RankNullity
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Regular.RegularSequence
Mathlib.RingTheory.RegularLocalRing.Defs

Imported by4

theorem

exists_regular_pair_of_finrank_cotangentSpace_eq_two

L37 ↗

EtaleFundamentalGroups.exists_regular_pair_of_finrank_cotangentSpace_eq_two

Documentation

In cotangent dimension two, a prime element with nonzero cotangent class can be completed to a regular pair generating the maximal ideal.

Source context 5 commands

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

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

Lean source · statement

theorem exists_regular_pair_of_finrank_cotangentSpace_eq_two
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (hfin : Module.finrank (ResidueField R) (CotangentSpace R) = 2)
    {x : R} (hxPrime : Prime x) (hxMem : x ∈ maximalIdeal R)
    (hxSq : x ∉ maximalIdeal R ^ 2) :
    ∃ y : R, IsRegular R [x, y] ∧
      Ideal.ofList [x, y] = maximalIdeal R

theorem

exists_regular_pair_localizationAtPrime_of_height_eq_two

L148 ↗

EtaleFundamentalGroups.exists_regular_pair_localizationAtPrime_of_height_eq_two