NormResidueCoprimeRepresentative.lean

1 import PaperX.CoprimeClassRepresentative
2 import PaperX.NormResidueRepresentative
3 import Mathlib.RingTheory.DedekindDomain.Factorization
4 import Mathlib.RingTheory.Ideal.Norm.AbsNorm
5 
6 /-!
7 # Automatic coprime inverse-class representatives for number fields
8 
9 For a nonzero integer modulus `m`, only finitely many prime ideals divide the
10 principal modulus ideal `(m)`.  Finite-prime avoidance supplies an inverse-class
11 representative avoiding all of them.  A rational prime dividing both its
12 absolute norm and `m` would produce a maximal ideal above that prime dividing
13 both ideals, contradicting the avoidance property.
14 -/
15 
16 set_option autoImplicit false
17 noncomputable section
18 
19 open Ideal NumberField
20 open scoped NumberField nonZeroDivisors
21 
22 namespace PaperX.NormResidue
23 
24 open PaperX.IdealPrimeAvoidance
25 
26 variable (K : Type*) [Field K] [NumberField K]
27 
28 /-- A nonzero integer modulus generates a nonzero ideal in the ring of integers. -/
29 theorem modulusIdeal_ne_bot (m : ℕ) (hm : m ≠ 0) :
30     modulusIdeal (𝓞 K) m ≠ (⊥ : Ideal (𝓞 K)) := by
31   rw [modulusIdeal, ne_eq, Ideal.span_singleton_eq_bot]
32   exact Nat.cast_ne_zero.mpr hm
33 
34 /-- Every ideal class has an inverse-class integral representative whose
35 absolute norm is coprime to any prescribed nonzero integer modulus. -/
36 theorem exists_coprime_inverse_class_representative
37     (C : ClassGroup (𝓞 K)) (m : ℕ) (hm : m ≠ 0) :
38     ∃ J : (Ideal (𝓞 K))⁰,
39       ClassGroup.mk0 J = C⁻¹ ∧
40       (absNorm (J : Ideal (𝓞 K))).Coprime m := by
41   classical
42   let M : Ideal (𝓞 K) := modulusIdeal (𝓞 K) m
43   have hM : M ≠ ⊥ := by
44     simpa [M] using modulusIdeal_ne_bot K m hm
45   let s : Finset (IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :=
46     (Ideal.finite_factors hM).toFinset
47   obtain ⟨I, hI⟩ := ClassGroup.mk0_surjective C
48   let P : {v // v ∈ s} → Ideal (𝓞 K) := fun v => v.1.asIdeal
49   have hP : ∀ v, Prime (P v) := fun v => v.1.prime
50   have hpair : Pairwise fun i j : {v // v ∈ s} => P i ≠ P j := by
51     intro i j hij hEq
52     apply hij
53     apply Subtype.ext
54     exact IsDedekindDomain.HeightOneSpectrum.asIdeal_injective hEq
55   obtain ⟨J, hJclass, havoid⟩ :=
56     exists_inverse_class_representative_avoiding P hP hpair I
57   refine ⟨J, by simpa [hI] using hJclass, ?_⟩
58   by_contra hcop
59   obtain ⟨p, hp, hpJ, hpm⟩ := Nat.Prime.not_coprime_iff_dvd.mp hcop
60   obtain ⟨Q, hQmax, hQunder, hQJ⟩ :=
61     Ideal.exists_isMaximal_dvd_of_dvd_absNorm' hp (J : Ideal (𝓞 K)) hpJ
62   let v : IsDedekindDomain.HeightOneSpectrum (𝓞 K) :=
63     ⟨Q, hQmax.isPrime, Ideal.IsMaximal.ne_bot_of_isIntegral_int Q⟩
64   have hQm : Q ∣ M := by
65     rw [Ideal.dvd_iff_le]
66     change modulusIdeal (𝓞 K) m ≤ Q
67     rw [modulusIdeal]
68     apply Ideal.span_le.mpr
69     intro x hx
70     change x ∈ ({(m : 𝓞 K)} : Set (𝓞 K)) at hx
71     simp only [Set.mem_singleton_iff] at hx
72     subst x
73     have hpUnder : (p : ℤ) ∈ Q.under ℤ := by
74       rw [hQunder]
75       exact Ideal.mem_span_singleton_self (p : ℤ)
76     have hpQ : (p : 𝓞 K) ∈ Q := by
77       simpa [Ideal.mem_under] using hpUnder
78     have hpd : (p : 𝓞 K) ∣ (m : 𝓞 K) := by
79       obtain ⟨k, rfl⟩ := hpm
80       exact ⟨(k : 𝓞 K), by simp⟩
81     exact Q.mem_of_dvd hpd hpQ
82   have hvs : v ∈ s := by
83     simpa [s, v] using hQm
84   let q : {v // v ∈ s} := ⟨v, hvs⟩
85   exact havoid q (by simpa [P, q, v] using hQJ)
86 
87 end PaperX.NormResidue

Back to source controls