FinitePrimeAvoidance.lean

1 import PaperX.NormResidueRepresentative
2 import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
3 
4 /-!
5 # Simultaneous finite-prime avoidance inside a nonzero Dedekind ideal
6 
7 For a finite family of distinct nonzero prime ideals and a nonzero integral
8 ideal `I`, construct an element of `I` whose valuation at every selected prime
9 is exactly the valuation already forced by `I`.  Equivalently, the element is
10 not in `P * I` for any selected prime `P`.
11 
12 This is the algebraic CRT mechanism needed to replace a prescribed ideal-class
13 representative by one avoiding all primes above a fixed modulus.
14 -/
15 
16 set_option autoImplicit false
17 noncomputable section
18 
19 open Ideal
20 open scoped BigOperators
21 
22 namespace PaperX.IdealPrimeAvoidance
23 
24 variable {R ι : Type*} [CommRing R] [IsDedekindDomain R]
25 
26 private theorem exists_mem_not_mem_prime_mul
27     (P I : Ideal R) (hP : Prime P) (hI : I ≠ ⊥) :
28     ∃ a : R, a ∈ I ∧ a ∉ P * I := by
29   have hPt : P < (⊤ : Ideal R) :=
30     lt_top_iff_ne_top.mpr (isPrime_of_prime hP).ne_top
31   have hpos : (⊥ : Ideal R) < I := bot_lt_iff_ne_bot.mpr hI
32   have hmul : P * I < (⊤ : Ideal R) * I :=
33     mul_lt_mul_of_pos_right hPt hpos
34   have hstrict : P * I < I := by simpa using hmul
35   obtain ⟨a, haI, haPI⟩ := SetLike.exists_of_lt hstrict
36   exact ⟨a, haI, haPI⟩
37 
38 /-- A nonzero ideal contains an element which simultaneously avoids `P * I`
39 for every ideal in a finite pairwise-distinct prime family. -/
40 theorem exists_mem_avoiding_prime_multiples [Fintype ι]
41     (P : ι → Ideal R) (hP : ∀ i, Prime (P i))
42     (hpair : Pairwise fun i j => P i ≠ P j)
43     (I : Ideal R) (hI : I ≠ ⊥) :
44     ∃ a : R, a ∈ I ∧ ∀ i, a ∉ P i * I := by
45   classical
46   have ha_exists : ∀ i : ι, ∃ a : R, a ∈ I ∧ a ∉ P i * I :=
47     fun i => exists_mem_not_mem_prime_mul (P i) I (hP i) hI
48   choose a0 ha0I ha0not using ha_exists
49 
50   let target : ι → (↥(Finset.univ : Finset ι) → R) := fun i j =>
51     if (j : ι) = i then 1 else 0
52 
53   have he_exists : ∀ i : ι, ∃ e : R, ∀ j : ι,
54       e - (if j = i then 1 else 0) ∈ P j := by
55     intro i
56     obtain ⟨e, he⟩ := IsDedekindDomain.exists_forall_sub_mem_ideal
57       (s := (Finset.univ : Finset ι)) P (fun _ => 1)
58       (fun j _ => hP j)
59       (fun j _ k _ hjk => hpair hjk)
60       (target i)
61     refine ⟨e, ?_⟩
62     intro j
63     simpa [target] using he j (Finset.mem_univ j)
64   choose e he using he_exists
65 
66   let a : R := ∑ i : ι, e i * a0 i
67   refine ⟨a, ?_, ?_⟩
68   · dsimp [a]
69     exact Ideal.sum_mem _ fun i _ => I.mul_mem_left (e i) (ha0I i)
70   · intro k hak
71     have hdiff : a - a0 k ∈ P k * I := by
72       have hsum :
73           ∑ i : ι, (e i - (if i = k then 1 else 0)) * a0 i ∈ P k * I := by
74         exact Ideal.sum_mem _ fun i _ =>
75           Ideal.mul_mem_mul (by simpa [eq_comm] using he i k) (ha0I i)
76       have hid :
77           (∑ i : ι, (e i - (if i = k then 1 else 0)) * a0 i) = a - a0 k := by
78         simp [a, sub_mul]
79       rw [hid] at hsum
80       exact hsum
81     have ha0bad : a0 k ∈ P k * I := by
82       have : a0 k = a - (a - a0 k) := by ring
83       rw [this]
84       exact (P k * I).sub_mem hak hdiff
85     exact (ha0not k) ha0bad
86 
87 
88 /-- The simultaneous avoiding element can be chosen nonzero, including when the
89 finite prime family is empty. -/
90 theorem exists_ne_zero_mem_avoiding_prime_multiples [Fintype ι]
91     (P : ι → Ideal R) (hP : ∀ i, Prime (P i))
92     (hpair : Pairwise fun i j => P i ≠ P j)
93     (I : Ideal R) (hI : I ≠ ⊥) :
94     ∃ a : R, a ∈ I ∧ a ≠ 0 ∧ ∀ i, a ∉ P i * I := by
95   classical
96   cases isEmpty_or_nonempty ι with
97   | inl hEmpty =>
98       obtain ⟨a, haI, ha0⟩ := (Submodule.ne_bot_iff I).mp hI
99       exact ⟨a, haI, ha0, fun i => (hEmpty.false i).elim⟩
100   | inr hNonempty =>
101       obtain ⟨a, haI, ha⟩ :=
102         exists_mem_avoiding_prime_multiples P hP hpair I hI
103       refine ⟨a, haI, ?_, ha⟩
104       intro ha0
105       subst a
106       let i : ι := Classical.choice hNonempty
107       exact ha i (P i * I).zero_mem
108 
109 end PaperX.IdealPrimeAvoidance

Back to source controls