Module

CompleteLocalChevalley.lean

Nyll.EtaleFundamentalGroups.Purity.CompleteLocalChevalley

4 declarations indexed from sourceView source ↗

Module documentation

Descending ideals in complete local rings

Chevalley's lemma compares a descending sequence of ideals with zero intersection to the powers of the maximal ideal. The proof uses stable images modulo these powers and lifts compatible representatives directly.

Imports2

Mathlib.RingTheory.AdicCompletion.Noetherian
Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Imported by3

theorem

maximalIdeal_pow_quotient_artinian

L28 ↗

EtaleFundamentalGroups.maximalIdeal_pow_quotient_artinian

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups
universe u
variable {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]

Lean source · statement

theorem maximalIdeal_pow_quotient_artinian (k : ℕ) :
    IsArtinianRing (C ⧸ maximalIdeal C ^ k)

theorem

exists_eq_iInf_sup_maximalIdeal_pow

L44 ↗

EtaleFundamentalGroups.exists_eq_iInf_sup_maximalIdeal_pow

Documentation

The images of a descending sequence of ideals modulo a fixed power of the maximal ideal stabilize.

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups
universe u
variable {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]

Lean source · statement

theorem exists_eq_iInf_sup_maximalIdeal_pow
    (J : ℕ → Ideal C) (hJ : Antitone J) (k : ℕ) :
    ∃ N : ℕ, J N ⊔ maximalIdeal C ^ k =
      ⨅ n : ℕ, J n ⊔ maximalIdeal C ^ k

theorem

mem_ideal_of_mem_sup_maximalIdeal_pow

L71 ↗

EtaleFundamentalGroups.mem_ideal_of_mem_sup_maximalIdeal_pow

Documentation

Every ideal of a Noetherian local ring is closed for the topology defined by powers of the maximal ideal.

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups
universe u
variable {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]

Lean source · statement

theorem mem_ideal_of_mem_sup_maximalIdeal_pow
    (J : Ideal C) (x : C)
    (hx : ∀ n : ℕ, x ∈ J ⊔ maximalIdeal C ^ n) : x ∈ J

theorem

exists_le_maximalIdeal_pow_of_antitone_iInf_eq_bot

L91 ↗

EtaleFundamentalGroups.exists_le_maximalIdeal_pow_of_antitone_iInf_eq_bot

Documentation

Chevalley's lemma: in a complete Noetherian local ring, every descending sequence of ideals with zero intersection is eventually contained in each power of the maximal ideal.

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups
universe u
variable {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]

Lean source · statement

theorem exists_le_maximalIdeal_pow_of_antitone_iInf_eq_bot
    [IsAdicComplete (maximalIdeal C) C]
    (J : ℕ → Ideal C) (hJ : Antitone J)
    (hinf : (⨅ n : ℕ, J n) = ⊥) (k : ℕ) :
    ∃ N : ℕ, J N ≤ maximalIdeal C ^ k

Module documentation

Descending ideals in complete local rings

Declarations

maximalIdeal_pow_quotient_artinian

exists_eq_iInf_sup_maximalIdeal_pow

mem_ideal_of_mem_sup_maximalIdeal_pow

exists_le_maximalIdeal_pow_of_antitone_iInf_eq_bot