AuxiliaryCyclotomicDisjoint.lean

1 import Mathlib.FieldTheory.LinearDisjoint
2 import Mathlib.FieldTheory.PrimitiveElement
3 import Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
4 import Mathlib.NumberTheory.LSeries.PrimesInAP
5 import Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
6 
7 /-! Auxiliary cyclotomic fields can be chosen disjoint from a supplied number field.
8 The proof uses finite intermediate fields and pairwise disjoint prime conductors,
9 without invoking ramification or prime distribution over number fields. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperX.AuxiliaryCyclotomicDisjoint
13 open IntermediateField
14 
15 section FiniteExceptions
16 variable {k M I : Type*} [Field k] [Field M] [Algebra k M]
17   (L : IntermediateField k M) [Finite (IntermediateField k L)]
18   (C : I → IntermediateField k M)
19 
20 /-- Pairwise disjoint extensions have nontrivial intersection with a fixed
21 extension at only finitely many indices, if that extension has finitely many
22 intermediate fields. -/
23 theorem finite_nontrivial_intersections
24     (hC : ∀ i j, i ≠ j → C i ⊓ C j = ⊥) :
25     Set.Finite {i | L ⊓ C i ≠ ⊥} := by
26   let f : {i // L ⊓ C i ≠ ⊥} → IntermediateField k L :=
27     fun i => (L ⊓ C i.val).restrict inf_le_left
28   have hf : Function.Injective f := by
29     intro i j hij
30     apply Subtype.ext
31     by_contra hne
32     have heq : L ⊓ C i.val = L ⊓ C j.val := by
33       have hh := congrArg IntermediateField.lift hij
34       simpa only [f, lift_restrict] using hh
35     apply i.property
36     apply le_antisymm _ bot_le
37     calc
38       L ⊓ C i.val ≤ C i.val ⊓ C j.val :=
39         le_inf inf_le_right (heq ▸ inf_le_right)
40       _ = ⊥ := hC i.val j.val hne
41   exact Set.finite_coe_iff.mp (Finite.of_injective f hf)
42 end FiniteExceptions
43 
44 section CyclotomicFields
45 variable (M : Type*) [Field M] [CharZero M] [IsAlgClosed M] [Algebra.IsAlgebraic ℚ M]
46 
47 /-- The actual cyclotomic subfield in the fixed ambient algebraically closed field. -/
48 def cyclotomicPart (n : ℕ) [NeZero n] : IntermediateField ℚ M :=
49   IntermediateField.adjoin ℚ {Classical.choose (HasEnoughRootsOfUnity.exists_primitiveRoot M n)}
50 
51 instance cyclotomicPart_isCyclotomic (n : ℕ) [NeZero n] :
52     IsCyclotomicExtension {n} ℚ (cyclotomicPart M n) :=
53   IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension ℚ
54     (Classical.choose_spec (HasEnoughRootsOfUnity.exists_primitiveRoot M n))
55 
56 instance cyclotomicPart_finite (n : ℕ) [NeZero n] :
57     FiniteDimensional ℚ (cyclotomicPart M n) :=
58   IsCyclotomicExtension.finite_of_singleton n ℚ _
59 
60 instance cyclotomicPart_numberField (n : ℕ) [NeZero n] :
61     NumberField (cyclotomicPart M n) := {}
62 
63 /-- Coprime conductors give linearly disjoint actual cyclotomic subfields. -/
64 theorem cyclotomicPart_linearDisjoint (m n : ℕ) [NeZero m] [NeZero n]
65     (h : m.Coprime n) : (cyclotomicPart M m).LinearDisjoint (cyclotomicPart M n) := by
66   have : NeZero (m.lcm n) := ⟨Nat.lcm_ne_zero (NeZero.ne _) (NeZero.ne _)⟩
67   have : IsCyclotomicExtension {m.lcm n} ℚ
68       (cyclotomicPart M m ⊔ cyclotomicPart M n : IntermediateField ℚ M) :=
69     IntermediateField.isCyclotomicExtension_lcm_sup ℚ M m n _ _
70   have : NumberField (cyclotomicPart M m ⊔ cyclotomicPart M n : IntermediateField ℚ M) :=
71     {}
72   apply IntermediateField.LinearDisjoint.of_finrank_sup
73   rw [IsCyclotomicExtension.Rat.finrank (m.lcm n),
74     IsCyclotomicExtension.Rat.finrank m, IsCyclotomicExtension.Rat.finrank n,
75     h.lcm_eq_mul, Nat.totient_mul h]
76 
77 /-- The cyclotomic field of prime conductor. -/
78 def primeCyclotomicPart (p : Nat.Primes) : IntermediateField ℚ M :=
79   let : NeZero (p : ℕ) := ⟨p.property.ne_zero⟩
80   cyclotomicPart M (p : ℕ)
81 
82 instance primeCyclotomicPart_isCyclotomic (p : Nat.Primes) :
83     IsCyclotomicExtension {(p : ℕ)} ℚ (primeCyclotomicPart M p) := by
84   let : NeZero (p : ℕ) := ⟨p.property.ne_zero⟩
85   exact cyclotomicPart_isCyclotomic M p
86 
87 instance primeCyclotomicPart_finite (p : Nat.Primes) :
88     FiniteDimensional ℚ (primeCyclotomicPart M p) := by
89   let : NeZero (p : ℕ) := ⟨p.property.ne_zero⟩
90   exact cyclotomicPart_finite M p
91 
92 instance primeCyclotomicPart_numberField (p : Nat.Primes) :
93     NumberField (primeCyclotomicPart M p) := {}
94 
95 /-- Distinct prime conductors give trivial intersection. -/
96 theorem primeCyclotomicPart_inf (p q : Nat.Primes) (hpq : p ≠ q) :
97     primeCyclotomicPart M p ⊓ primeCyclotomicPart M q = ⊥ := by
98   let : NeZero (p : ℕ) := ⟨p.property.ne_zero⟩
99   let : NeZero (q : ℕ) := ⟨q.property.ne_zero⟩
100   apply (cyclotomicPart_linearDisjoint M (p : ℕ) (q : ℕ) _).inf_eq_bot
101   exact (Nat.coprime_primes p.property q.property).mpr (fun h => hpq (Subtype.ext h))
102 
103 /-- Only finitely many prime cyclotomic fields intersect a fixed number field
104 nontrivially. The finite exceptional set is derived, not supplied. -/
105 theorem finite_bad_prime_conductors (L : IntermediateField ℚ M) [NumberField L] :
106     Set.Finite {p : Nat.Primes | L ⊓ primeCyclotomicPart M p ≠ ⊥} := by
107   have : Finite (IntermediateField ℚ L) :=
108     Field.finite_intermediateField_of_exists_primitive_element ℚ L
109       (Field.exists_primitive_element ℚ L)
110   exact finite_nontrivial_intersections L (primeCyclotomicPart M)
111     (primeCyclotomicPart_inf M)
112 
113 /-- A prime conductor congruent to one modulo any positive integer can be
114 chosen outside every finite exclusion, with cyclotomic field disjoint from L. -/
115 theorem exists_prime_conductor (L : IntermediateField ℚ M) [NumberField L]
116     (n : ℕ) [NeZero n] (forbidden : Finset ℕ) (B : ℕ) :
117     ∃ p : Nat.Primes, B < (p : ℕ) ∧ (p : ℕ) ∉ forbidden ∧
118       ((p : ℕ) : ZMod n) = 1 ∧
119       (primeCyclotomicPart M p).LinearDisjoint L := by
120   classical
121   let bad := (finite_bad_prime_conductors M L).toFinset.image (fun p : Nat.Primes => (p : ℕ))
122   let exc := forbidden ∪ bad
123   obtain ⟨p, hpB, hp, hres⟩ := Nat.forall_exists_prime_gt_and_eq_mod
124     (show IsUnit (1 : ZMod n) from isUnit_one) (max B (exc.sup id))
125   have hpnot : p ∉ exc := by
126     intro hm
127     exact (not_lt_of_ge ((Finset.le_sup (f := id) hm).trans (le_max_right _ _))) hpB
128   let p' : Nat.Primes := ⟨p, hp⟩
129   have hbad : L ⊓ primeCyclotomicPart M p' = ⊥ := by
130     by_contra h
131     apply hpnot
132     apply Finset.mem_union_right
133     apply Finset.mem_image.mpr
134     exact ⟨p', (Set.Finite.mem_toFinset _).mpr h, rfl⟩
135   refine ⟨p', (le_max_left _ _).trans_lt hpB, ?_, hres, ?_⟩
136   · intro hm
137     exact hpnot (Finset.mem_union_left _ hm)
138   · have : IsCyclotomicExtension {(p' : ℕ)} ℚ (primeCyclotomicPart M p') :=
139       primeCyclotomicPart_isCyclotomic M p'
140     have : IsGalois ℚ (primeCyclotomicPart M p') :=
141       IsCyclotomicExtension.isGalois {(p' : ℕ)} ℚ _
142     apply IntermediateField.LinearDisjoint.of_inf_eq_bot
143     simpa only [inf_comm] using hbad
144 
145 end CyclotomicFields
146 end PaperX.AuxiliaryCyclotomicDisjoint

Back to source controls