CoprimeClassRepresentative.lean

1 import PaperX.FinitePrimeAvoidance
2 import Mathlib.RingTheory.ClassGroup.Basic
3 
4 /-!
5 # Ideal-class representatives avoiding finitely many primes
6 
7 This is the elementary class-group step needed by the norm-residue counting
8 lane.  Starting from a nonzero ideal `I`, finite-prime avoidance produces a
9 nonzero `a ∈ I` with `a ∉ P * I` for every selected prime.  Factoring the
10 principal ideal `(a)` as `I * J` then puts `J` in the inverse ideal class and
11 forces `J` to avoid every selected prime.
12 -/
13 
14 set_option autoImplicit false
15 noncomputable section
16 
17 open Ideal
18 open scoped nonZeroDivisors
19 
20 namespace PaperX.IdealPrimeAvoidance
21 
22 variable {R ι : Type*} [CommRing R] [IsDedekindDomain R]
23 
24 /-- Every inverse ideal class has a nonzero integral representative avoiding a
25 prescribed finite pairwise-distinct family of prime ideals. -/
26 theorem exists_inverse_class_representative_avoiding [Fintype ι]
27     (P : ι → Ideal R) (hP : ∀ i, Prime (P i))
28     (hpair : Pairwise fun i j => P i ≠ P j)
29     (I : (Ideal R)⁰) :
30     ∃ J : (Ideal R)⁰,
31       ClassGroup.mk0 J = (ClassGroup.mk0 I)⁻¹ ∧
32       ∀ i, ¬ P i ∣ (J : Ideal R) := by
33   classical
34   obtain ⟨a, haI, ha0, haAvoid⟩ :=
35     exists_ne_zero_mem_avoiding_prime_multiples P hP hpair (I : Ideal R)
36       (mem_nonZeroDivisors_iff_ne_zero.mp I.2)
37   have hdiv : (I : Ideal R) ∣ Ideal.span {a} :=
38     Ideal.dvd_iff_le.mpr (Ideal.span_le.mpr (by
39       intro x hx
40       simp only [Set.mem_singleton_iff] at hx
41       subst x
42       exact haI))
43   obtain ⟨J, hJ⟩ := hdiv
44   have hJ0 : J ≠ (⊥ : Ideal R) := by
45     intro h0
46     subst J
47     have : Ideal.span ({a} : Set R) = ⊥ := by simpa using hJ
48     exact ha0 (Ideal.span_singleton_eq_bot.mp this)
49   let J0 : (Ideal R)⁰ := ⟨J, mem_nonZeroDivisors_iff_ne_zero.mpr hJ0⟩
50   refine ⟨J0, ?_, ?_⟩
51   · have hclass : ClassGroup.mk0 I = (ClassGroup.mk0 J0)⁻¹ := by
52       rw [ClassGroup.mk0_eq_mk0_inv_iff]
53       exact ⟨a, ha0, by simpa [J0] using hJ.symm⟩
54     have hinv := congrArg (fun z : ClassGroup R => z⁻¹) hclass
55     simpa using hinv.symm
56   · intro i hPiJ
57     apply haAvoid i
58     have hJP : J ≤ P i := Ideal.dvd_iff_le.mp hPiJ
59     have hmul : (I : Ideal R) * J ≤ (I : Ideal R) * P i :=
60       Ideal.mul_mono le_rfl hJP
61     have haProd : a ∈ (I : Ideal R) * J := by
62       rw [← hJ]
63       exact Ideal.mem_span_singleton_self a
64     have : a ∈ (I : Ideal R) * P i := hmul haProd
65     simpa [mul_comm] using this
66 
67 end PaperX.IdealPrimeAvoidance

Back to source controls