AuxiliaryCyclotomicGeneralBase.lean

1 import PaperX.AuxiliaryCyclotomicBaseChange
2 
3 /-! Auxiliary cyclic cyclotomic extensions over arbitrary number fields. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperX.AuxiliaryCyclotomicGeneralBase
7 open IntermediateField AuxiliaryCyclotomicDisjoint AuxiliaryCyclotomicExistence
8   AuxiliaryCyclotomicBaseChange
9 
10 variable (M : Type*) [Field M] [CharZero M] [IsAlgClosed M]
11   [Algebra.IsAlgebraic ℚ M]
12 
13 omit [Algebra.IsAlgebraic ℚ M] in
14 /-- The base change of a prime cyclotomic field is generated by an actual
15 primitive root of unity in the same ambient algebraic closure. -/
16 theorem compositumOver_primeCyclotomic (K : IntermediateField ℚ M) (p : Nat.Primes) :
17     ∃ z : M, IsPrimitiveRoot z (p : ℕ) ∧
18       compositumOver K (primeCyclotomicPart M p) = IntermediateField.adjoin K {z} := by
19   let : NeZero (p : ℕ) := ⟨p.property.ne_zero⟩
20   let z : M := Classical.choose (HasEnoughRootsOfUnity.exists_primitiveRoot M (p : ℕ))
21   have hz : IsPrimitiveRoot z (p : ℕ) :=
22     Classical.choose_spec (HasEnoughRootsOfUnity.exists_primitiveRoot M (p : ℕ))
23   refine ⟨z, hz, ?_⟩
24   rw [compositumOver_eq_adjoin]
25   change IntermediateField.adjoin K (IntermediateField.adjoin ℚ {z} : Set M) = _
26   exact IntermediateField.adjoin_adjoin_right (F := K) (K := ℚ) (S := ({z} : Set M))
27 
28 /-- The needed auxiliary cyclic degree-n extension exists over any number field K
29 inside L. It is disjoint from L over K and lies in K(zeta_q) for an actual prime q.
30 No auxiliary extension or disjointness is supplied in the hypotheses. -/
31 theorem exists_cyclic_cyclotomic_disjoint_over
32     (K L : IntermediateField ℚ M) [NumberField K] [NumberField L]
33     (hKL : K ≤ L) (n : ℕ) [NeZero n] (forbidden : Finset ℕ) (bound : ℕ) :
34     ∃ p : Nat.Primes, ∃ z : M, ∃ B : IntermediateField K M,
35       bound < (p : ℕ) ∧ (p : ℕ) ∉ forbidden ∧ IsPrimitiveRoot z (p : ℕ) ∧
36       B ≤ IntermediateField.adjoin K {z} ∧ Module.finrank K B = n ∧
37       IsGalois K B ∧ IsCyclic Gal(B/K) ∧
38       B.LinearDisjoint (IntermediateField.extendScalars hKL) := by
39   obtain ⟨p, A, hp, hpnot, hA, hdeg, hgal, hcyc, hdis⟩ :=
40     exists_cyclic_cyclotomic_disjoint M L n forbidden bound
41   have : FiniteDimensional ℚ A :=
42     Module.finite_of_finrank_pos (by rw [hdeg]; exact NeZero.pos n)
43   obtain ⟨z, hz, hfield⟩ := compositumOver_primeCyclotomic M K p
44   let B := compositumOver K A
45   have hB : B ≤ compositumOver K (primeCyclotomicPart M p) := by
46     simp only [B, compositumOver_eq_adjoin]
47     exact IntermediateField.adjoin.mono K _ _ hA
48   refine ⟨p, z, B, hp, hpnot, hz, hfield ▸ hB, ?_, ?_, ?_, ?_⟩
49   · exact (compositumOver_finrank K A (hdis.of_le_right hKL)).trans hdeg
50   · exact compositumOver_isGalois K A
51   · exact compositumOver_isCyclic K A
52   · exact compositumOver_linearDisjoint K A L hKL hdis
53 
54 end PaperX.AuxiliaryCyclotomicGeneralBase

Back to source controls