Quasi-Complete Local Rings

Definitions of quasi-completeness and weak quasi-completeness for local rings, following Anderson (2014). A local ring (R, M) is quasi-complete if every descending chain of ideals eventually stabilizes modulo powers of M. The weak variant restricts to chains with zero intersection. We also define analytical irreducibility (the M-adic completion is a domain).

def IsQuasiComplete (R : Type u_1) [CommRing R] [IsLocalRing R] : Prop

A local ring R is quasi-complete if for any antitone sequence of ideals A : ℕ → Ideal R and each k : ℕ, there exists s such that A s ≤ (⨅ n, A n) ⊔ (IsLocalRing.maximalIdeal R) ^ k.

This is Definition 1.1 of Anderson (2014).

Equations

• IsQuasiComplete R = ∀ (A : ℕ → Ideal R), Antitone A → ∀ (k : ℕ), ∃ (s : ℕ), A s ≤ (⨅ (n : ℕ), A n) ⊔ IsLocalRing.maximalIdeal R ^ k

def IsWeaklyQuasiComplete (R : Type u_1) [CommRing R] [IsLocalRing R] : Prop

A local ring R is weakly quasi-complete if for any antitone sequence of ideals A : ℕ → Ideal R with ⨅ n, A n = ⊥ and each k : ℕ, there exists s such that A s ≤ (IsLocalRing.maximalIdeal R) ^ k.

Equivalently, this is IsQuasiComplete restricted to sequences whose intersection is ⊥.

Equations

• IsWeaklyQuasiComplete R = ∀ (A : ℕ → Ideal R), Antitone A → ⨅ (n : ℕ), A n = ⊥ → ∀ (k : ℕ), ∃ (s : ℕ), A s ≤ IsLocalRing.maximalIdeal R ^ k

def IsAnalyticallyIrreducible (R : Type u_1) [CommRing R] [IsLocalRing R] : Prop

A local ring R is analytically irreducible if its maximal-ideal-adic completion is a domain. (This notion is primarily of interest for Noetherian local rings.)

Equations

• IsAnalyticallyIrreducible R = IsDomain (AdicCompletion (IsLocalRing.maximalIdeal R) R)

theorem IsQuasiComplete.isWeaklyQuasiComplete (R : Type u_1) [CommRing R] [IsLocalRing R] (h : IsQuasiComplete R) : IsWeaklyQuasiComplete R

Quasi-completeness implies weak quasi-completeness.

theorem IsQuasiComplete.quotient_isWeaklyQuasiComplete (R : Type u_1) [CommRing R] [IsLocalRing R] (h : IsQuasiComplete R) (I : Ideal R) (hI : I ≠ ⊤) : IsWeaklyQuasiComplete (R ⧸ I)

If R is quasi-complete, then every quotient R ⧸ I is weakly quasi-complete. This is one direction of Anderson Theorem 5, Item 3.