NYLL
Module

CompleteLocalSymbolicPowerCofinality.lean

Nyll.EtaleFundamentalGroups.Purity.CompleteLocalSymbolicPowerCofinality
1 declaration indexed from sourceView source ↗

Module documentation

Cofinality of symbolic and ordinary prime powers

For a prime with quotient of dimension at most one in a complete Noetherian local domain, sufficiently deep symbolic powers lie in any specified ordinary power. Modulo that ordinary power, the symbolic-power images lie in an Artinian module and hence stabilize. Chevalley's lemma places the stable image in every maximal-ideal power, so Hausdorffness of the finite quotient forces it to vanish.

Imports4
Imported by1

Declarations

theorem

exists_primeSymbolicPower_le_pow

L36 ↗
EtaleFundamentalGroups.Purity.exists_primeSymbolicPower_le_pow
Documentation

Symbolic powers of a prime with quotient dimension at most one are cofinal with its ordinary powers in a complete local domain.

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
  [IsNoetherianRing R] [IsAdicComplete (maximalIdeal R) R]
Lean source · statement
theorem exists_primeSymbolicPower_le_pow
    (P : Ideal R) [P.IsPrime]
    (hdim : ringKrullDim (R ⧸ P) ≤ (1 : WithBot ℕ∞)) (n : ℕ) :
    ∃ m : ℕ, primeSymbolicPower P m ≤ P ^ n

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.