CyclotomicCrossingExistence.lean

1 import PaperX.CyclotomicCrossingContainment
2 import PaperX.AuxiliaryCyclotomicExistence
3 
4 /-!
5 # Existence of the cyclotomic crossing over Q
6 
7 The auxiliary field, prime conductor, primitive root, and crossing automorphism
8 are constructed. No prescribed arithmetic Frobenius occurrence is asserted.
9 -/
10 
11 set_option autoImplicit false
12 
13 noncomputable section
14 
15 namespace PaperX.CyclotomicCrossingExistence
16 
17 open IntermediateField CyclotomicCrossing AuxiliaryCyclotomicDisjoint
18 
19 section Restriction
20 
21 variable {K M : Type*} [Field K] [Field M] [Algebra K M]
22 
23 /-- The left field, considered inside the compositum. -/
24 def leftPart (L A : IntermediateField K M) : IntermediateField K (L ⊔ A : IntermediateField K M) :=
25   L.restrict le_sup_left
26 
27 /-- The auxiliary field, considered inside the compositum. -/
28 def rightPart (L A : IntermediateField K M) : IntermediateField K (L ⊔ A : IntermediateField K M) :=
29   A.restrict le_sup_right
30 
31 /-- The restricted fields generate the compositum as an actual ambient field. -/
32 theorem parts_sup_eq_top (L A : IntermediateField K M) : leftPart L A ⊔ rightPart L A = ⊤ := by
33   apply lift_injective
34   simp only [leftPart, rightPart, lift_sup, lift_restrict, lift_top]
35 
36 /-- Linear disjointness is preserved upon changing the ambient field to the compositum. -/
37 theorem parts_linearDisjoint (L A : IntermediateField K M)
38     [FiniteDimensional K L] [FiniteDimensional K A] [IsGalois K L]
39     (hdisj : L.LinearDisjoint A) : (leftPart L A).LinearDisjoint (rightPart L A) := by
40   let eL : L ≃ₐ[K] leftPart L A := restrictAlgEquiv (le_sup_left : L ≤ L ⊔ A)
41   have : IsGalois K (leftPart L A) := IsGalois.of_algEquiv eL
42   apply LinearDisjoint.of_inf_eq_bot
43   apply lift_injective
44   simp only [leftPart, rightPart, lift_inf, lift_restrict, lift_bot, hdisj.inf_eq_bot]
45 
46 /-- The restriction automorphism equality gives the actual action on each
47 element of the original left field after embedding in the compositum. -/
48 theorem action_of_restriction_eq (L A : IntermediateField K M)
49     [Normal K (leftPart L A)] (sigma : L ≃ₐ[K] L)
50     (rho : (L ⊔ A : IntermediateField K M) ≃ₐ[K] (L ⊔ A : IntermediateField K M))
51     (h : AlgEquiv.restrictNormalHom (leftPart L A) rho =
52       (restrictAlgEquiv (le_sup_left : L ≤ L ⊔ A)).autCongr sigma) :
53     ∀ x : L, (rho (inclusion (le_sup_left : L ≤ L ⊔ A) x) : M) = (sigma x : M) := by
54   let eL : L ≃ₐ[K] leftPart L A := restrictAlgEquiv le_sup_left
55   intro x
56   have hh := AlgEquiv.restrictNormal_commutes rho (leftPart L A) (eL x)
57   change rho.restrictNormal (leftPart L A) = eL.autCongr sigma at h
58   rw [h] at hh
59   simp only [AlgEquiv.autCongr_apply, AlgEquiv.trans_apply, AlgEquiv.symm_apply_apply] at hh
60   have heL (y : L) : (algebraMap (leftPart L A) (L ⊔ A : IntermediateField K M)) (eL y) =
61       inclusion (le_sup_left : L ≤ L ⊔ A) y := rfl
62   rw [heL, heL] at hh
63   exact congrArg ((↑) : (L ⊔ A : IntermediateField K M) → M) hh.symm
64 
65 end Restriction
66 
67 section Existence
68 
69 variable (M : Type*) [Field M] [CharZero M] [IsAlgClosed M] [Algebra.IsAlgebraic ℚ M]
70 
71 /-- For every finite Galois number field inside an algebraic closure of Q and
72 every automorphism, the actual cyclotomic crossing exists. The prime conductor
73 can avoid any supplied finite set and exceed any supplied bound. -/
74 theorem exists_cyclotomic_crossing
75     (L : IntermediateField ℚ M) [NumberField L] [IsGalois ℚ L]
76     (sigma : L ≃ₐ[ℚ] L) (forbidden : Finset ℕ) (B : ℕ) :
77     ∃ p : Nat.Primes, ∃ A : IntermediateField ℚ M, ∃ ζ : M,
78       ∃ rho : (L ⊔ A : IntermediateField ℚ M) ≃ₐ[ℚ] (L ⊔ A : IntermediateField ℚ M),
79       B < (p : ℕ) ∧ (p : ℕ) ∉ forbidden ∧ IsPrimitiveRoot ζ (p : ℕ) ∧
80       NumberField (L ⊔ A : IntermediateField ℚ M) ∧
81       IsGalois ℚ (L ⊔ A : IntermediateField ℚ M) ∧
82       (∀ x : L, (rho (inclusion (le_sup_left : L ≤ L ⊔ A) x) : M) = (sigma x : M)) ∧
83       fixedField (Subgroup.zpowers rho) ⊔ rightPart L A = ⊤ ∧
84       IsGalois (fixedField (Subgroup.zpowers rho)) (L ⊔ A : IntermediateField ℚ M) ∧
85       IsCyclic ((L ⊔ A : IntermediateField ℚ M) ≃ₐ[fixedField (Subgroup.zpowers rho)]
86         (L ⊔ A : IntermediateField ℚ M)) ∧
87       Module.finrank (fixedField (Subgroup.zpowers rho)) (L ⊔ A : IntermediateField ℚ M) =
88         orderOf sigma ∧
89       (L ⊔ A : IntermediateField ℚ M) ≤
90         (adjoin ((fixedField (Subgroup.zpowers rho)).map (L ⊔ A).val) ({ζ} : Set M)).restrictScalars ℚ := by
91   have hn : 0 < orderOf sigma := orderOf_pos sigma
92   have : NeZero (orderOf sigma) := ⟨hn.ne'⟩
93   obtain ⟨p, A, hpB, hpnot, hA, hdegree, hgal, hcyc, hdis⟩ :=
94     AuxiliaryCyclotomicExistence.exists_cyclic_cyclotomic_disjoint
95       M L (orderOf sigma) forbidden B
96   have : IsGalois ℚ A := hgal
97   have : IsCyclic (A ≃ₐ[ℚ] A) := hcyc
98   have : FiniteDimensional ℚ A := Module.finite_of_finrank_pos (hdegree.symm ▸ hn)
99   have : IsGalois ℚ (L ⊔ A : IntermediateField ℚ M) := {}
100   let eL : L ≃ₐ[ℚ] leftPart L A := restrictAlgEquiv le_sup_left
101   let eA : A ≃ₐ[ℚ] rightPart L A := restrictAlgEquiv le_sup_right
102   have : IsGalois ℚ (leftPart L A) := IsGalois.of_algEquiv eL
103   have : IsGalois ℚ (rightPart L A) := IsGalois.of_algEquiv eA
104   have : IsCyclic ((rightPart L A) ≃ₐ[ℚ] (rightPart L A)) :=
105     isCyclic_of_surjective eA.autCongr eA.autCongr.surjective
106   have hdegree' : Module.finrank ℚ (rightPart L A) = orderOf (eL.autCongr sigma) := by
107     rw [← eA.toLinearEquiv.finrank_eq, eL.autCongr.orderOf_eq, hdegree]
108   obtain ⟨rho, hrestrict, hsup, hcyclic, hdeg⟩ := exists_crossing_of_cyclic_auxiliary
109     (leftPart L A) (rightPart L A) (parts_linearDisjoint L A hdis.symm)
110     (parts_sup_eq_top L A) (eL.autCongr sigma) hdegree'
111   have : NeZero (p : ℕ) := ⟨p.property.ne_zero⟩
112   let ζ : M := Classical.choose (HasEnoughRootsOfUnity.exists_primitiveRoot M (p : ℕ))
113   have hζ : IsPrimitiveRoot ζ (p : ℕ) :=
114     Classical.choose_spec (HasEnoughRootsOfUnity.exists_primitiveRoot M (p : ℕ))
115   have hAζ : (rightPart L A).map (L ⊔ A).val ≤ adjoin ℚ ({ζ} : Set M) := by
116     change lift (A.restrict (le_sup_right : A ≤ L ⊔ A)) ≤ _
117     rw [lift_restrict]
118     exact hA
119   refine ⟨p, A, ζ, rho, hpB, hpnot, hζ, {}, inferInstance,
120     action_of_restriction_eq L A sigma rho hrestrict,
121     hsup, isGalois_fixedField_zpowers rho, hcyclic, ?_, ?_⟩
122   · simpa only [eL.autCongr.orderOf_eq] using hdeg
123   · have hh := fieldRange_le_adjoin_of_sup_eq_top _ (rightPart L A) hsup (L ⊔ A).val ζ hAζ
124     simpa only [fieldRange_val] using hh
125 
126 end Existence
127 
128 end PaperX.CyclotomicCrossingExistence

Back to source controls