Main Theorem: WQC Does Not Imply QC #
There exists a Noetherian local UFD that is weakly quasi-complete but not quasi-complete. The ring is obtained via Jensen--Heitmann with completion T = ℂ[[x,y,z]]/(x²-yz) Anderson's theorems reduce the problem to a quotient that fails weak quasi-completeness.
The ring A from jensen_special_case is weakly quasi-complete. Uses: trivial generic formal fiber + isWeaklyQuasiComplete_iff_primes_meet.
X₀ is not in conjI = (x²-yz): coefficient at degree-1 monomial x is 1 for X₀ but 0 for any multiple of x²-yz (which has minimum degree 2).
The contraction of Q through the completion isomorphism has height 1. Uses faithful flatness of adic completion: 1 ≤ ht(q) ≤ ht(Q') = ht(Q) = 1.
algebraMap A Â is a local ring hom: if r ∈ M_A then evalOneₐ sends its
image to 0, so it cannot be a unit.
dim(A) ≤ dim(Â) for Noetherian local rings via flat going-down. Proof: algebraMap A  is a local ring hom (via evalOneₐ), so maximalIdeal  lies over maximalIdeal A, then height_eq_height_add gives ht(M_A) ≤ ht(M_Â) = dim(Â).
A/M is M-adic Hausdorff (M kills A/M, so the filtration is trivially zero).
A/M is M-adic precomplete (the adic topology is discrete).
map mkQ (mk a) = of (evalOneₐ (mk a)) — component-wise comparison.
map mkQ x = 0 ↔ evalOneₐ x = 0 — kernel equivalence.
range(map subtype) ⊆ Ideal.map algebraMap M — via tensor product description.
ker(evalOneₐ M) = Ideal.map (algebraMap A Â) M for Noetherian local rings. Uses: exact sequence of completions + tensor product description + of_bijective.
Ideal.map (algebraMap A Â) M = maxIdeal  for Noetherian local rings.
evalₐ M n z = 0 implies map M (mkQ (M^n)) z = 0. Component-wise: each component of (map mkQ z) in (A/M^n)/(M^k•(A/M^n)) is 0.
range(map M (subtype (M^n))) ⊆ Ideal.map algebraMap (M^n).
ker(evalₐ M n) ⊆ maximalIdeal(Â)^n for Noetherian local rings.
The quotient A/(a) has Krull dimension 1. Since A is a 2-dimensional UFD and a is prime, dim(A/(a)) = dim(A) - 1 = 1. Uses: dim(Â) = dim(A) via faithful flatness, and dim(T) = 2.
If b ∈ Q is nonzero, then span {b} is not prime: span{b} ≤ Q and ht Q = 1,
so if span{b} were prime it would equal Q (chain ⊥ < span{b} < Q is too long),
contradicting that Q is not principal.
The quotient A/(a) is not analytically irreducible. Key argument: b = φ(algebraMap a) ∈ Q, so span{b} ≤ Q. Since Q is not principal, span{b} ≠ Q. Since ht(Q) = 1, span{b} is not prime, so T/bT is not a domain. Since completion commutes with quotient: completion(A/(a)) ≅ T/bT, done.
There exists a prime element a in A such that A/(a) is a 1-dim Noetherian local domain that is not weakly quasi-complete.
Main Theorem: There exists a weakly quasi-complete Noetherian local ring that is not quasi-complete.