LeanPool.AndersonConjecture.QuasiCompleteRing.QuasiCompleteRing

Imported Lean Pool material for LeanPool.AndersonConjecture.QuasiCompleteRing.QuasiCompleteRing.

Anderson's Characterisations of Quasi-Complete Rings

Two results from Anderson (2014). Theorem 4: a Noetherian local ring R is weakly quasi-complete iff every nonzero prime of its completion contracts to a nonzero ideal of R. Theorem 5: R is quasi-complete iff every quotient R/I is weakly quasi-complete.

theorem Mhat_isMaximal (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : (Ideal.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.maximalIdeal R)).IsMaximal

theorem iInf_comap_add_pow_eq_comap (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] (A : Ideal (AdicCompletion (IsLocalRing.maximalIdeal R) R)) : ⨅ (n : ℕ), Ideal.comap (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (A ⊔ Ideal.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.maximalIdeal R) ^ n) = Ideal.comap (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) A

theorem wqc_implies_ideals_meet (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] (hwqc : IsWeaklyQuasiComplete R) (A : Ideal (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (hA : A ≠ ⊥) : Ideal.comap (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) A ≠ ⊥

theorem not_wqc_exists_maximal_zero_contraction (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] (hnwqc : ¬IsWeaklyQuasiComplete R) : ∃ (A : Ideal (AdicCompletion (IsLocalRing.maximalIdeal R) R)), A ≠ ⊥ ∧ Ideal.comap (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) A = ⊥ ∧ ∀ (B : Ideal (AdicCompletion (IsLocalRing.maximalIdeal R) R)), A < B → Ideal.comap (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) B ≠ ⊥

theorem isWeaklyQuasiComplete_iff_primes_meet (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] : IsWeaklyQuasiComplete R ↔ ∀ (P : Ideal (AdicCompletion (IsLocalRing.maximalIdeal R) R)), P.IsPrime → P ≠ ⊥ → Ideal.comap (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) P ≠ ⊥

theorem IsWeaklyQuasiComplete.isAnalyticallyIrreducible (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] (hwqc : IsWeaklyQuasiComplete R) : IsAnalyticallyIrreducible R

theorem dim1_ai_nonzero_prime_contracts (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] (hdim : ringKrullDim R = 1) (hAI : IsAnalyticallyIrreducible R) (P : Ideal (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (hPprime : P.IsPrime) (hPne : P ≠ ⊥) : Ideal.comap (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) P ≠ ⊥

Helper: in a 1-dim Noetherian local domain R with completion a domain, every nonzero prime P of the completion has nonzero contraction to R.

Proof outline:

1. M ≠ ⊥ (dim R = 1 implies R is not a field).
2. M̂ = Ideal.map f M is maximal in R̂ (via Mhat_isMaximal).
3. If comap f P = ⊥, then f(m) ∉ P for all nonzero m ∈ M, so M̂ ⊄ P.
4. Since M̂ is maximal and P is proper prime, this means P ⊊ M̂.
5. But comap f M̂ = M ≠ ⊥, so ⊥ < P < M̂ with comap P = ⊥ and comap M̂ = M.

The final contradiction uses going-down for flat extensions (AdicCompletion.flat_of_isNoetherian): height(M̂) ≤ height(M) + dim(fiber). Since R̂/M̂ ≅ R/M is a field, height(M̂) ≤ 1, but ⊥ < P < M̂ gives height(M̂) ≥ 2.

theorem dim1_wqc_iff_analyticallyIrreducible (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] (hdim : ringKrullDim R = 1) : IsWeaklyQuasiComplete R ↔ IsAnalyticallyIrreducible R

theorem dim1_qc_iff_wqc (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] (hdim : ringKrullDim R = 1) : IsQuasiComplete R ↔ IsWeaklyQuasiComplete R

theorem isQuasiComplete_iff_quotients_wqc (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : IsQuasiComplete R ↔ ∀ (I : Ideal R) (hI : I ≠ ⊤), IsWeaklyQuasiComplete (R ⧸ I)