NYLL
Module

CompleteLocalSaturatedPowers.lean

Nyll.EtaleFundamentalGroups.Purity.CompleteLocalSaturatedPowers
14 declarations indexed from sourceView source ↗

Module documentation

Maximal-ideal saturation of powers

Contracting the maximal-ideal-primary component of a quotient gives the maximal-ideal saturation of its defining ideal. If an ideal lies in a nonmaximal prime of a complete Noetherian local domain, its saturated powers and ordinary powers are cofinal. The finite-length error module is the maximal-ideal-primary component itself, so no coheight assumption on the containing prime is required.

Imports10
Imported by3

Declarations

def

maximalIdealSaturation

L41 ↗
EtaleFundamentalGroups.Purity.maximalIdealSaturation
Documentation

The maximal-ideal saturation of an ideal, contracted from the torsion submodule of its quotient.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
def maximalIdealSaturation (I : Ideal R) : Ideal R
theorem

mem_maximalIdealSaturation_iff

L46 ↗
EtaleFundamentalGroups.Purity.mem_maximalIdealSaturation_iff
Documentation

Saturation membership is annihilation modulo the ideal by some power of the maximal ideal.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem mem_maximalIdealSaturation_iff (I : Ideal R) (x : R) :
    x ∈ maximalIdealSaturation I ↔
      ∃ k : ℕ, ∀ a ∈ maximalIdeal R ^ k, a * x ∈ I
theorem

le_maximalIdealSaturation

L67 ↗
EtaleFundamentalGroups.Purity.le_maximalIdealSaturation
Documentation

Every ideal is contained in its saturation.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem le_maximalIdealSaturation (I : Ideal R) : I ≤ maximalIdealSaturation I
theorem

maximalIdealSaturation_mono

L73 ↗
EtaleFundamentalGroups.Purity.maximalIdealSaturation_mono
Documentation

Saturation preserves inclusions of ideals.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem maximalIdealSaturation_mono : Monotone (maximalIdealSaturation (R := R))
def

maximalIdealSaturatedPower

L79 ↗
EtaleFundamentalGroups.Purity.maximalIdealSaturatedPower
Documentation

The descending filtration obtained by saturating ordinary powers.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
def maximalIdealSaturatedPower (I : Ideal R) (n : ℕ) : Ideal R
theorem

pow_le_maximalIdealSaturatedPower

L83 ↗
EtaleFundamentalGroups.Purity.pow_le_maximalIdealSaturatedPower
Documentation

Ordinary powers are contained in their maximal-ideal saturations.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem pow_le_maximalIdealSaturatedPower (I : Ideal R) (n : ℕ) :
    I ^ n ≤ maximalIdealSaturatedPower I n
theorem

maximalIdealSaturatedPower_antitone

L88 ↗
EtaleFundamentalGroups.Purity.maximalIdealSaturatedPower_antitone
Documentation

Saturated powers form a decreasing filtration.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem maximalIdealSaturatedPower_antitone (I : Ideal R) :
    Antitone (maximalIdealSaturatedPower I)
theorem

maximalIdealSaturatedPower_le_primeSymbolicPower

L95 ↗
EtaleFundamentalGroups.Purity.maximalIdealSaturatedPower_le_primeSymbolicPower
Documentation

A saturated power lies in the symbolic power of every containing nonmaximal prime.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem maximalIdealSaturatedPower_le_primeSymbolicPower
    (I P : Ideal R) [P.IsPrime] (hIP : I ≤ P)
    (hP : P ≠ maximalIdeal R) (n : ℕ) :
    maximalIdealSaturatedPower I n ≤ primeSymbolicPower P n
theorem

iInf_maximalIdealSaturatedPower_eq_bot

L109 ↗
EtaleFundamentalGroups.Purity.iInf_maximalIdealSaturatedPower_eq_bot
Documentation

Saturated powers have zero intersection when the ideal lies in a nonmaximal prime of a Noetherian local domain.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem iInf_maximalIdealSaturatedPower_eq_bot
    [IsDomain R] [IsNoetherianRing R]
    (I P : Ideal R) [P.IsPrime] (hIP : I ≤ P)
    (hP : P ≠ maximalIdeal R) :
    (⨅ n : ℕ, maximalIdealSaturatedPower I n) = ⊥
theorem

exists_maximalIdealSaturatedPower_le_maximalIdeal_pow

L120 ↗
EtaleFundamentalGroups.Purity.exists_maximalIdealSaturatedPower_le_maximalIdeal_pow
Documentation

Completeness turns separated saturated powers into an m-adically cofinal filtration.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem exists_maximalIdealSaturatedPower_le_maximalIdeal_pow
    [IsDomain R] [IsNoetherianRing R] [IsAdicComplete (maximalIdeal R) R]
    (I P : Ideal R) [P.IsPrime] (hIP : I ≤ P)
    (hP : P ≠ maximalIdeal R) (k : ℕ) :
    ∃ n : ℕ, maximalIdealSaturatedPower I n ≤ maximalIdeal R ^ k
theorem

isFiniteLength_primaryComponent_quotient

L130 ↗
EtaleFundamentalGroups.Purity.isFiniteLength_primaryComponent_quotient
Documentation

The error module introduced by saturation has finite length.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem isFiniteLength_primaryComponent_quotient
    [IsNoetherianRing R] (I : Ideal R) :
    IsFiniteLength R (Ideal.primaryComponent (R ⧸ I) (maximalIdeal R))
theorem

exists_maximalIdealSaturatedPower_le_pow_of_le_prime

L144 ↗
EtaleFundamentalGroups.Purity.exists_maximalIdealSaturatedPower_le_pow_of_le_prime
Documentation

In a complete Noetherian local domain, saturated powers of an ideal contained in a nonmaximal prime eventually lie in each ordinary power.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem exists_maximalIdealSaturatedPower_le_pow_of_le_prime
    [IsDomain R] [IsNoetherianRing R] [IsAdicComplete (maximalIdeal R) R]
    (I P : Ideal R) [P.IsPrime] (hIP : I ≤ P)
    (hP : P ≠ maximalIdeal R) (n : ℕ) :
    ∃ m : ℕ, maximalIdealSaturatedPower I m ≤ I ^ n
theorem

exists_nonmaximal_prime_over_of_radical_ne

L195 ↗
EtaleFundamentalGroups.Purity.exists_nonmaximal_prime_over_of_radical_ne
Documentation

A proper ideal whose radical is not the maximal ideal is contained in a nonmaximal prime.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem exists_nonmaximal_prime_over_of_radical_ne
    (I : Ideal R) (hI : I ≠ ⊤) (hrad : I.radical ≠ maximalIdeal R) :
    ∃ P : Ideal R, I ≤ P ∧ P.IsPrime ∧ P ≠ maximalIdeal R
theorem

exists_maximalIdealSaturatedPower_le_pow

L211 ↗
EtaleFundamentalGroups.Purity.exists_maximalIdealSaturatedPower_le_pow
Documentation

Saturation does not change the adic topology of a proper ideal whose radical is not the maximal ideal in a complete Noetherian local domain.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open IsLocalRing
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem exists_maximalIdealSaturatedPower_le_pow
    [IsDomain R] [IsNoetherianRing R] [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : I ≠ ⊤) (hrad : I.radical ≠ maximalIdeal R) (n : ℕ) :
    ∃ m : ℕ, maximalIdealSaturatedPower I m ≤ I ^ n

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