Module

RegularLocalGeneral.lean

Nyll.EtaleFundamentalGroups.Purity.Local.RegularLocalGeneral

4 declarations indexed from sourceView source ↗

Module documentation

Regular hypersurface sections of regular local domains

The induction on dimension in local purity cuts a regular local ring by a parameter whose cotangent class is nonzero. This file supplies the local algebra behind that step in arbitrary dimension: quotienting a regular local domain by an element of the maximal ideal which is not in its square again gives a regular local ring.

The proof does not choose a full regular system of parameters. It extends the nonzero cotangent class to a basis, lifts the remaining basis vectors, and uses Nakayama to generate the maximal ideal after quotienting. The principal non-zero-divisor dimension formula then identifies the dimension of the quotient.

Imports4

Mathlib.LinearAlgebra.Basis.VectorSpace
Mathlib.RingTheory.KrullDimension.Regular
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.RingTheory.RegularLocalRing.Defs

Imported by3

theorem

isRegularLocalRing_quotient_span_singleton_of_not_mem_maximalIdeal_sq

L38 ↗

EtaleFundamentalGroups.isRegularLocalRing_quotient_span_singleton_of_not_mem_maximalIdeal_sq

Documentation

A hypersurface cut by a nonzero cotangent vector in a regular local domain is regular local. This is valid in every finite Krull dimension.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe u

Lean source · statement

theorem isRegularLocalRing_quotient_span_singleton_of_not_mem_maximalIdeal_sq
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    {x : R} (hxMem : x ∈ maximalIdeal R)
    (hxSq : x ∉ maximalIdeal R ^ 2) :
    IsRegularLocalRing (R ⧸ Ideal.span ({x} : Set R))

theorem

exists_parameter_with_regularLocalRing_quotient

L208 ↗

EtaleFundamentalGroups.exists_parameter_with_regularLocalRing_quotient

Documentation

A positive-dimensional regular local domain contains a parameter whose principal quotient is again regular local. The parameter and its transversality to the square of the maximal ideal are produced internally from a nonzero cotangent vector.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe u

Lean source · statement

theorem exists_parameter_with_regularLocalRing_quotient
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    (hdim : (1 : WithBot ℕ∞) ≤ ringKrullDim R) :
    ∃ x : R, x ∈ maximalIdeal R ∧ x ∉ maximalIdeal R ^ 2 ∧
      IsRegularLocalRing (R ⧸ Ideal.span ({x} : Set R))

theorem

exists_parameter_with_regularLocalRing_quotient_ringKrullDim_eq

L239 ↗

EtaleFundamentalGroups.exists_parameter_with_regularLocalRing_quotient_ringKrullDim_eq

Documentation

Cutting a regular local domain of dimension n + 1 by the parameter constructed above gives a regular local ring of dimension exactly n. This is the dimension-decreasing datum used by induction in local purity.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe u

Lean source · statement

theorem exists_parameter_with_regularLocalRing_quotient_ringKrullDim_eq
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    (n : ℕ)
    (hdim : ringKrullDim R = ((n + 1 : ℕ) : WithBot ℕ∞)) :
    ∃ x : R, x ∈ maximalIdeal R ∧ x ∉ maximalIdeal R ^ 2 ∧
      IsRegularLocalRing (R ⧸ Ideal.span ({x} : Set R)) ∧
      ringKrullDim (R ⧸ Ideal.span ({x} : Set R)) =
        (n : WithBot ℕ∞)

theorem

exists_parameter_with_regularLocalRing_quotient_of_three_le_ringKrullDim

L280 ↗

EtaleFundamentalGroups.exists_parameter_with_regularLocalRing_quotient_of_three_le_ringKrullDim

Documentation

In dimension at least three, one can choose the regular parameter so that the regular local quotient still has dimension at least two. This is the purely algebraic induction step preceding the local extension theorem.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe u

Lean source · statement

theorem exists_parameter_with_regularLocalRing_quotient_of_three_le_ringKrullDim
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    (hdim : (3 : WithBot ℕ∞) ≤ ringKrullDim R) :
    ∃ x : R, x ∈ maximalIdeal R ∧ x ∉ maximalIdeal R ^ 2 ∧
      IsRegularLocalRing (R ⧸ Ideal.span ({x} : Set R)) ∧
      (2 : WithBot ℕ∞) ≤
        ringKrullDim (R ⧸ Ideal.span ({x} : Set R))

Module documentation

Regular hypersurface sections of regular local domains

Declarations

isRegularLocalRing_quotient_span_singleton_of_not_mem_maximalIdeal_sq

exists_parameter_with_regularLocalRing_quotient

exists_parameter_with_regularLocalRing_quotient_ringKrullDim_eq

exists_parameter_with_regularLocalRing_quotient_of_three_le_ringKrullDim