Module

CompleteLocalSymbolicPowers.lean

Nyll.EtaleFundamentalGroups.Purity.CompleteLocalSymbolicPowers

8 declarations indexed from sourceView source ↗

Module documentation

Symbolic powers in the complete-local vanishing argument

The symbolic powers of a prime are the contractions of its powers after localizing at that prime. In a Noetherian domain their intersection is zero. Finite generation also clears the denominators of an entire symbolic power at once: a single element outside the prime sends it into the ordinary power. These two facts supply the separated filtration and the torsion error terms used in the complete-local vanishing argument.

Imports7

Nyll.EtaleFundamentalGroups.Purity.CompleteLocalChevalley
Mathlib.RingTheory.Filtration
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.Ideal
Mathlib.RingTheory.Localization.Submodule

Imported by5

def

primeSymbolicPower

L36 ↗

EtaleFundamentalGroups.Purity.primeSymbolicPower

Documentation

The n-th symbolic power of a prime ideal, defined by contraction from the localization at that prime.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

def primeSymbolicPower (P : Ideal R) [P.IsPrime] (n : ℕ) : Ideal R

theorem

mem_primeSymbolicPower_iff

L42 ↗

EtaleFundamentalGroups.Purity.mem_primeSymbolicPower_iff

Documentation

Symbolic-power membership is ordinary-power membership after multiplying by a denominator outside the prime.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem mem_primeSymbolicPower_iff
    (P : Ideal R) [P.IsPrime] (n : ℕ) (x : R) :
    x ∈ primeSymbolicPower P n ↔
      ∃ s : R, s ∉ P ∧ s * x ∈ P ^ n

theorem

pow_le_primeSymbolicPower

L52 ↗

EtaleFundamentalGroups.Purity.pow_le_primeSymbolicPower

Documentation

The ordinary prime power is contained in its symbolic power.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem pow_le_primeSymbolicPower (P : Ideal R) [P.IsPrime] (n : ℕ) :
    P ^ n ≤ primeSymbolicPower P n

theorem

primeSymbolicPower_antitone

L57 ↗

EtaleFundamentalGroups.Purity.primeSymbolicPower_antitone

Documentation

Symbolic powers form a decreasing filtration.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem primeSymbolicPower_antitone (P : Ideal R) [P.IsPrime] :
    Antitone (primeSymbolicPower P)

theorem

iInf_primeSymbolicPower_eq_bot

L64 ↗

EtaleFundamentalGroups.Purity.iInf_primeSymbolicPower_eq_bot

Documentation

The intersection of all symbolic powers of a prime in a Noetherian domain is zero. Krull intersection is applied in the localized ring.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem iInf_primeSymbolicPower_eq_bot
    [IsDomain R] [IsNoetherianRing R]
    (P : Ideal R) [P.IsPrime] :
    (⨅ n : ℕ, primeSymbolicPower P n) = ⊥

theorem

exists_common_primeCompl_multiplier

L78 ↗

EtaleFundamentalGroups.Purity.exists_common_primeCompl_multiplier

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem exists_common_primeCompl_multiplier
    (P : Ideal R) [P.IsPrime] (I J : Ideal R) (hJfg : J.FG)
    (hJ : ∀ x : R, x ∈ J → ∃ s : R, s ∉ P ∧ s * x ∈ I) :
    ∃ s : R, s ∉ P ∧ ∀ x : R, x ∈ J → s * x ∈ I

theorem

exists_mul_primeSymbolicPower_mem_pow

L107 ↗

EtaleFundamentalGroups.Purity.exists_mul_primeSymbolicPower_mem_pow

Documentation

A single denominator outside the prime sends the entire symbolic power into the corresponding ordinary power.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem exists_mul_primeSymbolicPower_mem_pow
    [IsNoetherianRing R] (P : Ideal R) [P.IsPrime] (n : ℕ) :
    ∃ s : R, s ∉ P ∧
      ∀ x : R, x ∈ primeSymbolicPower P n → s * x ∈ P ^ n

theorem

exists_primeSymbolicPower_le_maximalIdeal_pow

L118 ↗

EtaleFundamentalGroups.Purity.exists_primeSymbolicPower_le_maximalIdeal_pow

Documentation

In a complete Noetherian local domain, symbolic powers eventually lie in any prescribed power of the maximal ideal.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem exists_primeSymbolicPower_le_maximalIdeal_pow
    [IsDomain R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    (P : Ideal R) [P.IsPrime] (k : ℕ) :
    ∃ n : ℕ, primeSymbolicPower P n ≤ IsLocalRing.maximalIdeal R ^ k

Module documentation

Symbolic powers in the complete-local vanishing argument

Declarations