Prime Avoidance in Complete Local Rings

Given a complete local ring and a family of primes, one can find elements avoiding all shifted translates. The countable case uses Cauchy sequences the uncountable case uses a cardinality argument.

Heitmann, "Characterization of completions of UFDs", 1993, Lemmas 2--3.

theorem mem_sub_of_mem_add_singleton {T : Type u_1} [CommRing T] {P : Ideal T} {r u : T} (hmem : u ∈ ↑P + {r}) : u - r ∈ P

Extract u - r ∈ P from u ∈ ↑P + {r} (Minkowski sum).

theorem not_mem_add_singleton_of_add {T : Type u_1} [CommRing T] {P : Ideal T} {r u y : T} (hu : u ∈ ↑P + {r}) (hy : y ∉ P) : u + y ∉ ↑P + {r}

If u ∈ P + {r} and y ∉ P, then u + y ∉ P + {r}.

theorem separation_for_translate {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (P : Ideal T) (hP : P.IsPrime) (_hP_ne : P ≠ IsLocalRing.maximalIdeal T) (x r : T) (hx : x ∉ ↑P + {r}) : ∃ (N : ℕ), ∀ m ∈ IsLocalRing.maximalIdeal T ^ N, x + m ∉ ↑P + {r}

Separation for translates: if x ∉ P + {r} with P prime ≠ 𝔪 in a Noetherian local ring, then ∃ N such that adding any element of 𝔪^N preserves non-membership. Uses the Krull intersection theorem in T ⧸ P.

theorem mem_of_mem_sup_pow {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I : Ideal T) (L : T) (h : ∀ (n : ℕ), L ∈ I ⊔ IsLocalRing.maximalIdeal T ^ n) : L ∈ I

Membership in I via Krull intersection: if L ∈ I + 𝔪^n for all n, then L ∈ I. Uses the Artin-Rees lemma (via Ideal.mem_iInf_smul_pow_eq_bot_iff) on T ⧸ I.

noncomputable def avoidStep {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I P : Ideal T) (hP : P.IsPrime) (hP_ne : P ≠ IsLocalRing.maximalIdeal T) (r : T) (ea : ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (u : T) (q : ℕ) : T × ℕ

Step function for the Cauchy sequence construction. Given current value u and precision level q, produces (u', q') that avoids P + {r} with separation at level q'.

Equations

• avoidStep I P hP hP_ne r ea u q = if hmem : u ∈ ↑P + {r} then (u + ⋯.choose, max (q + 1) ⋯.choose) else (u, max (q + 1) ⋯.choose)

def buildSeq {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I : Ideal T) {C : Set (Ideal T)} (hC_prime : ∀ P ∈ C, P.IsPrime) (hC_ne_max : ∀ P ∈ C, P ≠ IsLocalRing.maximalIdeal T) (exists_avoid : ∀ P ∈ C, ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (P_of : ℕ → Ideal T) (r_of : ℕ → T) (hP_mem : ∀ (n : ℕ), P_of n ∈ C) : ℕ → T × ℕ

Build the Cauchy sequence (u_n, q_n) by iterating avoidStep.

Equations

• One or more equations did not get rendered due to their size.
• buildSeq I hC_prime hC_ne_max exists_avoid P_of r_of hP_mem 0 = (0, 0)

theorem avoidStep_q_inc {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I P : Ideal T) (hP : P.IsPrime) (hP_ne : P ≠ IsLocalRing.maximalIdeal T) (r : T) (ea : ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (u : T) (q : ℕ) : (avoidStep I P hP hP_ne r ea u q).2 ≥ q + 1

theorem avoidStep_diff {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I P : Ideal T) (hP : P.IsPrime) (hP_ne : P ≠ IsLocalRing.maximalIdeal T) (r : T) (ea : ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (u : T) (q : ℕ) : (avoidStep I P hP hP_ne r ea u q).1 - u ∈ I * IsLocalRing.maximalIdeal T ^ q

theorem avoidStep_avoids {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I P : Ideal T) (hP : P.IsPrime) (hP_ne : P ≠ IsLocalRing.maximalIdeal T) (r : T) (ea : ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (u : T) (q : ℕ) : (avoidStep I P hP hP_ne r ea u q).1 ∉ ↑P + {r}

theorem avoidStep_sep {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I P : Ideal T) (hP : P.IsPrime) (hP_ne : P ≠ IsLocalRing.maximalIdeal T) (r : T) (ea : ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (u : T) (q : ℕ) (m : T) : m ∈ IsLocalRing.maximalIdeal T ^ (avoidStep I P hP hP_ne r ea u q).2 → (avoidStep I P hP hP_ne r ea u q).1 + m ∉ ↑P + {r}

theorem buildSeqQInc {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I : Ideal T) {C : Set (Ideal T)} (hC_prime : ∀ P ∈ C, P.IsPrime) (hC_ne_max : ∀ P ∈ C, P ≠ IsLocalRing.maximalIdeal T) (ea : ∀ P ∈ C, ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (P_of : ℕ → Ideal T) (r_of : ℕ → T) (hP_mem : ∀ (n : ℕ), P_of n ∈ C) (n : ℕ) : (buildSeq I hC_prime hC_ne_max ea P_of r_of hP_mem (n + 1)).2 ≥ (buildSeq I hC_prime hC_ne_max ea P_of r_of hP_mem n).2 + 1

theorem buildSeqDiff {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I : Ideal T) {C : Set (Ideal T)} (hC_prime : ∀ P ∈ C, P.IsPrime) (hC_ne_max : ∀ P ∈ C, P ≠ IsLocalRing.maximalIdeal T) (ea : ∀ P ∈ C, ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (P_of : ℕ → Ideal T) (r_of : ℕ → T) (hP_mem : ∀ (n : ℕ), P_of n ∈ C) (n : ℕ) : (buildSeq I hC_prime hC_ne_max ea P_of r_of hP_mem (n + 1)).1 - (buildSeq I hC_prime hC_ne_max ea P_of r_of hP_mem n).1 ∈ I * IsLocalRing.maximalIdeal T ^ (buildSeq I hC_prime hC_ne_max ea P_of r_of hP_mem n).2

theorem buildSeqAvoids {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I : Ideal T) {C : Set (Ideal T)} (hC_prime : ∀ P ∈ C, P.IsPrime) (hC_ne_max : ∀ P ∈ C, P ≠ IsLocalRing.maximalIdeal T) (ea : ∀ P ∈ C, ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (P_of : ℕ → Ideal T) (r_of : ℕ → T) (hP_mem : ∀ (n : ℕ), P_of n ∈ C) (n : ℕ) : (buildSeq I hC_prime hC_ne_max ea P_of r_of hP_mem (n + 1)).1 ∉ ↑(P_of n) + {r_of n}

theorem buildSeqSep {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I : Ideal T) {C : Set (Ideal T)} (hC_prime : ∀ P ∈ C, P.IsPrime) (hC_ne_max : ∀ P ∈ C, P ≠ IsLocalRing.maximalIdeal T) (ea : ∀ P ∈ C, ∀ (n : ℕ), ∃ z ∈ I * IsLocalRing.maximalIdeal T ^ n, z ∉ P) (P_of : ℕ → Ideal T) (r_of : ℕ → T) (hP_mem : ∀ (n : ℕ), P_of n ∈ C) (n : ℕ) (m : T) : m ∈ IsLocalRing.maximalIdeal T ^ (buildSeq I hC_prime hC_ne_max ea P_of r_of hP_mem (n + 1)).2 → (buildSeq I hC_prime hC_ne_max ea P_of r_of hP_mem (n + 1)).1 + m ∉ ↑(P_of n) + {r_of n}

Countable Avoidance (Heitmann Lemma 2)

If I ⊄ P for all P in a countable set C of primes (M ∉ C), then there exists u ∈ I avoiding all translates P + r for P ∈ C, r ∈ D (countable). Requires completeness of T (to take limits of Cauchy sequences).

theorem countable_avoidance {T : Type u_1} [CommRing T] [IsLocalRing T] [TopologicalSpace T] [IsTopologicalRing T] [IsNoetherianRing T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] {C : Set (Ideal T)} (hC_countable : C.Countable) (hC_prime : ∀ P ∈ C, P.IsPrime) (hC_ne_max : ∀ P ∈ C, P ≠ IsLocalRing.maximalIdeal T) {D : Set T} (hD_countable : D.Countable) {I : Ideal T} (hI : ∀ P ∈ C, ¬I ≤ P) : ∃ u ∈ I, ∀ P ∈ C, ∀ r ∈ D, u ∉ ↑P + {r}

Heitmann Lemma 2: Countable avoidance in complete local rings. Given a countable set C of primes not containing M, a countable set D ⊆ T, and an ideal I not contained in any P ∈ C, there exists u ∈ I such that u ∉ P + {r} for all P ∈ C and r ∈ D.

The proof constructs a Cauchy sequence in I whose limit avoids all translates.

Uncountable Avoidance (Heitmann Lemma 3)

If |C × D| < |T/M|, then I ⊄ ⋃{P + r | P ∈ C, r ∈ D}. This is a cardinality argument using the fact that a vector space over a field k cannot be covered by fewer than |k| proper subspaces.

theorem ideal_avoidance_of_card_lt_aux {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (n : ℕ) (I : Ideal T) (C : Set (Ideal T)) : (∀ P ∈ C, P.IsPrime) → Cardinal.mk ↑C < Cardinal.mk (IsLocalRing.ResidueField T) → (∀ P ∈ C, ¬I ≤ P) → (∃ (s : Finset T), Ideal.span ↑s = I ∧ s.card ≤ n) → ∃ t ∈ I, ∀ P ∈ C, t ∉ P

Covering number argument: in a Noetherian local ring, if |C| < |T/M| and I ⊄ P for all primes P ∈ C, then ∃ t ∈ I avoiding all P ∈ C. Proof by induction on the number of generators of I.

theorem ideal_avoidance_of_card_lt {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] (I : Ideal T) (C : Set (Ideal T)) (hC_prime : ∀ P ∈ C, P.IsPrime) (hC_card : Cardinal.mk ↑C < Cardinal.mk (IsLocalRing.ResidueField T)) (hI : ∀ P ∈ C, ¬I ≤ P) : ∃ t ∈ I, ∀ P ∈ C, t ∉ P

Wrapper: in a Noetherian local ring, |C| < |T/M| and I ⊄ P implies ∃ t ∈ I, t ∉ P for all P.

theorem uncountable_avoidance {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] {C : Set (Ideal T)} (hC_prime : ∀ P ∈ C, P.IsPrime) {D : Set T} (hcard : Cardinal.mk (↑C × ↑D) < Cardinal.mk (IsLocalRing.ResidueField T)) {I : Ideal T} (hI : ∀ P ∈ C, ¬I ≤ P) : ∃ u ∈ I, ∀ P ∈ C, ∀ r ∈ D, u ∉ ↑P + {r}

Heitmann Lemma 3: Uncountable avoidance. If the product |C × D| has cardinality strictly less than |T/M|, and I is not contained in any P ∈ C, then there exists u ∈ I avoiding all translates P + r.

theorem avoidance {T : Type u_1} [CommRing T] [IsLocalRing T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] [IsNoetherianRing T] {C : Set (Ideal T)} (hC_prime : ∀ P ∈ C, P.IsPrime) (hC_ne_max : ∀ P ∈ C, P ≠ IsLocalRing.maximalIdeal T) {D : Set T} (hCD_bound : Cardinal.mk (↑C × ↑D) < Cardinal.mk (IsLocalRing.ResidueField T) ∨ C.Countable ∧ D.Countable) {I : Ideal T} (hI : ∀ P ∈ C, ¬I ≤ P) : ∃ u ∈ I, ∀ P ∈ C, ∀ r ∈ D, u ∉ ↑P + {r}

Combined avoidance: works for both countable and uncountable residue fields. If C is a finite or countable set of primes (M ∉ C) and D is appropriately bounded, find u ∈ I avoiding all P + r.