AuxiliaryCyclotomicExistence.lean

1 import PaperX.AuxiliaryCyclotomicDisjoint
2 import PaperX.AuxiliaryCyclotomicDegree
3 
4 /-! Existence of the cyclic cyclotomic auxiliary field used in field crossing.
5 No auxiliary field or disjointness witness is assumed in the existence theorem. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.AuxiliaryCyclotomicExistence
9 open IntermediateField AuxiliaryCyclotomicDisjoint AuxiliaryCyclotomicDegree
10 
11 variable (M : Type*) [Field M] [CharZero M] [IsAlgClosed M]
12   [Algebra.IsAlgebraic ℚ M]
13 
14 /-- For every number field L in an algebraic closure and every positive degree n,
15 there is a cyclic degree-n field A contained in a prime cyclotomic field and
16 linearly disjoint from L. Its prime conductor can avoid any supplied finite set
17 and exceed any supplied bound. -/
18 theorem exists_cyclic_cyclotomic_disjoint (L : IntermediateField ℚ M) [NumberField L]
19     (n : ℕ) [NeZero n] (forbidden : Finset ℕ) (B : ℕ) :
20     ∃ p : Nat.Primes, ∃ A : IntermediateField ℚ M,
21       B < (p : ℕ) ∧ (p : ℕ) ∉ forbidden ∧
22       A ≤ primeCyclotomicPart M p ∧ Module.finrank ℚ A = n ∧
23       IsGalois ℚ A ∧ IsCyclic Gal(A/ℚ) ∧ A.LinearDisjoint L := by
24   obtain ⟨p, hpB, hpnot, hres, hdis⟩ := exists_prime_conductor M L n forbidden B
25   have : Fact (p : ℕ).Prime := ⟨p.property⟩
26   have : NeZero (p : ℕ) := ⟨p.property.ne_zero⟩
27   have : IsCyclotomicExtension {(p : ℕ)} ℚ (primeCyclotomicPart M p) :=
28     primeCyclotomicPart_isCyclotomic M p
29   have hn : n ∣ (p : ℕ) - 1 := by
30     apply (ZMod.natCast_eq_zero_iff _ n).mp
31     rw [Nat.cast_sub p.property.one_le, hres, Nat.cast_one, sub_self]
32   obtain ⟨A, hdegree, hgal, hcyc⟩ := exists_prime_cyclotomic_subfield
33     (p : ℕ) (primeCyclotomicPart M p) n hn
34   have hgal' : IsGalois ℚ (IntermediateField.lift A) := IsGalois.of_algEquiv (IntermediateField.liftAlgEquiv A)
35   have hcyc' : IsCyclic Gal((IntermediateField.lift A)/ℚ) :=
36     isCyclic_of_surjective (IntermediateField.liftAlgEquiv A).autCongr
37       (IntermediateField.liftAlgEquiv A).autCongr.surjective
38   refine ⟨p, IntermediateField.lift A, hpB, hpnot, (IntermediateField.lift_le A), ?_, hgal', hcyc',
39     hdis.of_le_left (IntermediateField.lift_le A)⟩
40   exact (IntermediateField.liftAlgEquiv A).toLinearEquiv.finrank_eq.symm.trans hdegree
41 
42 /-- Specialization to the actual algebraic closure of Q. -/
43 theorem exists_in_algebraicClosure
44     (L : IntermediateField ℚ (AlgebraicClosure ℚ)) [NumberField L]
45     (n : ℕ) [NeZero n] :
46     ∃ p : Nat.Primes, ∃ A : IntermediateField ℚ (AlgebraicClosure ℚ),
47       A ≤ primeCyclotomicPart (AlgebraicClosure ℚ) p ∧ Module.finrank ℚ A = n ∧
48       IsGalois ℚ A ∧ IsCyclic Gal(A/ℚ) ∧ A.LinearDisjoint L := by
49   obtain ⟨p, A, _, _, hle, hdeg, hgal, hcyc, hdis⟩ :=
50     exists_cyclic_cyclotomic_disjoint (AlgebraicClosure ℚ) L n ∅ 0
51   exact ⟨p, A, hle, hdeg, hgal, hcyc, hdis⟩
52 
53 end PaperX.AuxiliaryCyclotomicExistence

Back to source controls