Module

RegularLocalParameters.lean

Nyll.EtaleFundamentalGroups.Purity.Local.RegularLocalParameters

2 declarations indexed from sourceView source ↗

Module documentation

Existence of regular systems of parameters

Successively cut a regular local ring by a nonzero cotangent vector. The quotient is again regular local with dimension one smaller. Lifting its regular system of parameters gives a regular system in the original ring.

Imports3

Nyll.SchemeTheory.RingTheory.RegularLocalDomain
Nyll.EtaleFundamentalGroups.Purity.Local.RegularLocalGeneral
Mathlib.RingTheory.Regular.RegularSequence

Imported by3

theorem

exists_regularSystem_of_ringKrullDim_eq

L28 ↗

EtaleFundamentalGroups.exists_regularSystem_of_ringKrullDim_eq

Documentation

A regular local ring of dimension n has a regular system of exactly n parameters.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing RingTheory.Sequence
universe u

Lean source · statement

theorem exists_regularSystem_of_ringKrullDim_eq :
    ∀ (n : ℕ) (R : Type u) [CommRing R] [IsRegularLocalRing R],
      ringKrullDim R = (n : WithBot ℕ∞) →
      ∃ ps : List R, IsRegular R ps ∧
        Ideal.ofList ps = maximalIdeal R ∧ ps.length = n

theorem

exists_regularSystem_of_isRegularLocalRing

L102 ↗

EtaleFundamentalGroups.exists_regularSystem_of_isRegularLocalRing