GeneralArithmeticCoverage.lean

1 import PaperX.CofiniteConjugacyCoverage
2 import PaperX.AbsoluteFrobeniusWitnesses
3 import PaperX.UnramifiedFrobeniusUniqueness
4 import PaperX.NumberFieldWitnessIndependence
5 import PaperX.RestrictionEmbeddingConjugacy
6 import Mathlib.FieldTheory.Galois.Infinite
7 
8 /-! The quotient interface for the remaining arithmetic prime-coverage input.
9 Every open normal subgroup of the actual absolute Galois group is realized by
10 its fixed finite Galois number field. Coverage of samples in all those fields is
11 therefore enough for the existing separation machinery. The arithmetic coverage
12 itself is an explicit premise, not an axiom or a theorem of this module. -/
13 set_option autoImplicit false
14 noncomputable section
15 namespace PaperX.GeneralArithmeticCoverage
16 open PaperX.AbsoluteIntegralFrobenius PaperX.CofiniteConjugacyCoverage
17 
18 /-- The closed subgroup underlying an actual open normal subgroup of G_Q. -/
19 def closedSubgroup (H : OpenNormalSubgroup GQ) : ClosedSubgroup GQ :=
20   ⟨H.toSubgroup, H.toOpenSubgroup.isClosed⟩
21 
22 /-- An open normal subgroup has the same fixing subgroup as its fixed field. -/
23 theorem fixingSubgroup_fixedField (H : OpenNormalSubgroup GQ) :
24     (IntermediateField.fixedField H.toSubgroup).fixingSubgroup = H.toSubgroup :=
25   InfiniteGalois.fixingSubgroup_fixedField (closedSubgroup H)
26 
27 /-- Openness proves that the actual fixed field is finite over Q. -/
28 theorem fixedField_finite (H : OpenNormalSubgroup GQ) :
29     FiniteDimensional ℚ (IntermediateField.fixedField H.toSubgroup) := by
30   apply (InfiniteGalois.isOpen_iff_finite _).mp
31   rw [fixingSubgroup_fixedField H]
32   exact H.toOpenSubgroup.isOpen
33 
34 /-- Normality proves that the actual fixed field is Galois over Q. -/
35 theorem fixedField_isGalois (H : OpenNormalSubgroup GQ) :
36     IsGalois ℚ (IntermediateField.fixedField H.toSubgroup) := by
37   apply (InfiniteGalois.normal_iff_isGalois _).mp
38   rw [fixingSubgroup_fixedField H]
39   infer_instance
40 
41 /-- The fixed field packaged as a finite Galois subfield of the chosen Qbar. -/
42 def fixedFiniteField (H : OpenNormalSubgroup GQ) :
43     FiniteGaloisIntermediateField ℚ Qbar where
44   __ := IntermediateField.fixedField H.toSubgroup
45   finiteDimensional := fixedField_finite H
46   isGalois := fixedField_isGalois H
47 
48 /-- The fixed finite extension is an actual number field. -/
49 theorem fixedFiniteField_numberField (H : OpenNormalSubgroup GQ) :
50     NumberField (fixedFiniteField H) := ⟨⟩
51 
52 /-- The kernel of restriction to the actual fixed field is exactly the starting
53 open normal subgroup. No abstract finite quotient is substituted for the field. -/
54 theorem restriction_fixedFiniteField_ker (H : OpenNormalSubgroup GQ) :
55     (AlgEquiv.restrictNormalHom (fixedFiniteField H)).ker = H.toSubgroup := by
56   rw [IntermediateField.restrictNormalHom_ker]
57   exact fixingSubgroup_fixedField H
58 
59 /-- A purely algebraic coverage condition on the restrictions of a sample family.
60 When applied to Frobenius, the sample must carry its arithmetic witness separately. -/
61 def FiniteFieldCoverage {X : Type*} (s : X → GQ) : Prop :=
62   ∀ (L : FiniteGaloisIntermediateField ℚ Qbar) (bad : Finset X) (σ : Gal(L/ℚ)),
63     ∃ p : X, p ∉ bad ∧ IsConj (AlgEquiv.restrictNormalHom L (s p)) σ
64 
65 /-- Coverage in every finite Galois subfield supplies conjugacy coverage in
66 every open normal quotient, with arbitrary finite exclusions preserved. -/
67 theorem cofiniteQuotientCoverage_of_finiteFieldCoverage
68     {X : Type*} (s : X → GQ) (h : FiniteFieldCoverage s) :
69     CofiniteQuotientCoverage s := by
70   intro bad H g
71   let L := fixedFiniteField H
72   let r : GQ →* Gal(L/ℚ) := AlgEquiv.restrictNormalHom L
73   obtain ⟨p, hp, hc⟩ := h L bad (r g)
74   obtain ⟨c, hc⟩ := isConj_iff.mp hc
75   obtain ⟨k, hk⟩ := AlgEquiv.restrictNormalHom_surjective Qbar c
76   refine ⟨⟨p, hp⟩, k, ?_⟩
77   change g⁻¹ * (k * s p * k⁻¹) ∈ H.toSubgroup
78   rw [← restriction_fixedFiniteField_ker H]
79   change r (g⁻¹ * (k * s p * k⁻¹)) = 1
80   change r k = c at hk
81   change c * r (s p) * c⁻¹ = r g at hc
82   simp only [map_mul, map_inv, hk, hc, inv_mul_cancel]
83 
84 /-- Conversely, open-normal quotient coverage gives conjugacy coverage in every
85 actual finite Galois subfield. Thus the field interface adds no stronger algebraic
86 or representation-theoretic premise. -/
87 theorem finiteFieldCoverage_of_cofiniteQuotientCoverage
88     {X : Type*} (s : X → GQ) (h : CofiniteQuotientCoverage s) :
89     FiniteFieldCoverage s := by
90   intro L bad σ
91   let r : GQ →* Gal(L/ℚ) := AlgEquiv.restrictNormalHom L
92   have hr : IsOpen (r.ker : Set GQ) :=
93     (isOpen_discrete ({1} : Set Gal(L/ℚ))).preimage
94       (InfiniteGalois.restrictNormalHom_continuous L.toIntermediateField)
95   let H : OpenNormalSubgroup GQ := ⟨⟨r.ker, hr⟩, inferInstance⟩
96   obtain ⟨g, hg⟩ := AlgEquiv.restrictNormalHom_surjective Qbar σ
97   obtain ⟨p, k, hk⟩ := h bad H g
98   refine ⟨p.val, p.property, isConj_iff.mpr ⟨r k, ?_⟩⟩
99   change r (g⁻¹ * (k * s p.val * k⁻¹)) = 1 at hk
100   change r g = σ at hg
101   simp only [map_mul, map_inv, hg] at hk
102   exact (inv_mul_eq_one.mp hk).symm
103 
104 /-- The exact algebraic equivalence between the finite-field arithmetic input
105 and the quotient interface used by the separator. -/
106 theorem finiteFieldCoverage_iff_cofiniteQuotientCoverage
107     {X : Type*} (s : X → GQ) :
108     FiniteFieldCoverage s ↔ CofiniteQuotientCoverage s :=
109   ⟨cofiniteQuotientCoverage_of_finiteFieldCoverage s,
110     finiteFieldCoverage_of_cofiniteQuotientCoverage s⟩
111 
112 section ArithmeticWitnesses
113 open PaperX.AbsoluteFrobeniusWitnesses PaperX.UnramifiedFrobeniusUniqueness
114 
115 local instance (L : FiniteGaloisIntermediateField ℚ Qbar) : NumberField L := ⟨⟩
116 
117 /-- Finite-field coverage with the actual discriminant primes excluded. The
118 exclusion depends on the finite extension, as arithmetic unramifiedness does. -/
119 def UnramifiedFiniteFieldCoverage (s : RationalPrime → GQ) : Prop :=
120   ∀ (L : FiniteGaloisIntermediateField ℚ Qbar) (bad : Finset RationalPrime)
121     (σ : Gal(L/ℚ)), ∃ p : RationalPrime, p ∉ bad ∧
122       p.val ∉ discriminantPrimes L ∧ IsConj (AlgEquiv.restrictNormalHom L (s p)) σ
123 
124 /-- Arbitrary finite avoidance allows the actual discriminant primes to be
125 excluded separately for each finite extension. -/
126 theorem unramifiedFiniteFieldCoverage_of_finiteFieldCoverage
127     (s : RationalPrime → GQ) (h : FiniteFieldCoverage s) :
128     UnramifiedFiniteFieldCoverage s := by
129   classical
130   intro L bad σ
131   obtain ⟨p, hp, hc⟩ := h L (bad ∪ (discriminantPrimes L).subtype Nat.Prime) σ
132   refine ⟨p, (Finset.notMem_union.mp hp).1, ?_, hc⟩
133   exact fun hmem => (Finset.notMem_union.mp hp).2 (Finset.mem_subtype.mpr hmem)
134 
135 /-- The discriminant-avoiding arithmetic formulation is exactly equivalent to
136 the quotient-coverage condition already required by the separator. -/
137 theorem unramifiedFiniteFieldCoverage_iff_cofiniteQuotientCoverage
138     (s : RationalPrime → GQ) :
139     UnramifiedFiniteFieldCoverage s ↔ CofiniteQuotientCoverage s := by
140   constructor
141   · intro h
142     apply cofiniteQuotientCoverage_of_finiteFieldCoverage s
143     intro L bad σ
144     obtain ⟨p, hp, _, hc⟩ := h L bad σ
145     exact ⟨p, hp, hc⟩
146   · intro h
147     exact unramifiedFiniteFieldCoverage_of_finiteFieldCoverage s
148       (finiteFieldCoverage_of_cofiniteQuotientCoverage s h)
149 
150 /-- The remaining arithmetic input, expressed using actual absolute Frobenius
151 witnesses at rational primes and actual finite normal number fields. This is a
152 proposition to be proved, not an existence or coverage axiom. -/
153 def ArithmeticCoverage (w : (p : RationalPrime) → Witness p.val) : Prop :=
154   UnramifiedFiniteFieldCoverage (fun p => (w p).element)
155 
156 /-- Canonical restriction to a finite normal subfield gives the same Frobenius
157 conjugacy class for every actual absolute witness outside its discriminant. -/
158 theorem canonicalRestriction_witnesses_isConj
159     (L : FiniteGaloisIntermediateField ℚ Qbar) (p : RationalPrime)
160     (u v : Witness p.val) (hp : p.val ∉ discriminantPrimes L) :
161     IsConj (AlgEquiv.restrictNormalHom L u.element)
162       (AlgEquiv.restrictNormalHom L v.element) := by
163   let : Fact p.val.Prime := ⟨p.property⟩
164   have h : IsConj (AbsoluteGaloisRestriction.restriction L u.element)
165       (AbsoluteGaloisRestriction.restriction L v.element) :=
166     isConj_iff.mpr
167       (NumberFieldWitnessIndependence.restricted_witnesses_conjugate L p.val u v hp)
168   exact (RestrictionEmbeddingConjugacy.restriction_isConj L.toIntermediateField u.element).symm.trans
169     (h.trans (RestrictionEmbeddingConjugacy.restriction_isConj L.toIntermediateField v.element))
170 
171 /-- The arithmetic prime-coverage obligation without a preselected global
172 Frobenius family: each occurrence may supply its own actual absolute witness.
173 The prime must avoid both the given finite set and this field's discriminant. -/
174 def ExistentialArithmeticCoverage : Prop :=
175   ∀ (L : FiniteGaloisIntermediateField ℚ Qbar) (bad : Finset RationalPrime)
176     (σ : Gal(L/ℚ)), ∃ p : RationalPrime, p ∉ bad ∧
177       p.val ∉ discriminantPrimes L ∧ ∃ u : Witness p.val,
178         IsConj (AlgEquiv.restrictNormalHom L u.element) σ
179 
180 /-- Actual prime coverage is independent of every global witness choice.
181 This uses derived unramifiedness and conjugacy, rather than assuming that the
182 chosen primes or Frobenius lifts agree. -/
183 theorem existentialArithmeticCoverage_iff_arithmeticCoverage
184     (w : (p : RationalPrime) → Witness p.val) :
185     ExistentialArithmeticCoverage ↔ ArithmeticCoverage w := by
186   constructor
187   · intro h L bad σ
188     obtain ⟨p, hp, hdisc, u, hu⟩ := h L bad σ
189     exact ⟨p, hp, hdisc,
190       (canonicalRestriction_witnesses_isConj L p (w p) u hdisc).trans hu⟩
191   · intro h L bad σ
192     obtain ⟨p, hp, hdisc, hc⟩ := h L bad σ
193     exact ⟨p, hp, hdisc, w p, hc⟩
194 
195 /-- Once actual arithmetic coverage is supplied, the chosen witness family
196 satisfies precisely the general separator's quotient hypothesis. -/
197 theorem cofiniteQuotientCoverage_of_arithmeticCoverage
198     (w : (p : RationalPrime) → Witness p.val) (h : ArithmeticCoverage w) :
199     CofiniteQuotientCoverage (fun p => (w p).element) :=
200   (unramifiedFiniteFieldCoverage_iff_cofiniteQuotientCoverage _).mp h
201 
202 /-- The same conditional conclusion applies to the witness family whose
203 existence was derived from integral closure and residue Frobenius. -/
204 theorem chosenWitness_coverage (h : ArithmeticCoverage chosenWitness) :
205     CofiniteQuotientCoverage (fun p => (chosenWitness p).element) :=
206   cofiniteQuotientCoverage_of_arithmeticCoverage chosenWitness h
207 
208 /-- The choice-free arithmetic obligation supplies cofinite quotient coverage
209 for every actual global Frobenius witness family. -/
210 theorem cofiniteQuotientCoverage_of_existentialArithmeticCoverage
211     (h : ExistentialArithmeticCoverage) (w : (p : RationalPrime) → Witness p.val) :
212     CofiniteQuotientCoverage (fun p => (w p).element) :=
213   cofiniteQuotientCoverage_of_arithmeticCoverage w
214     ((existentialArithmeticCoverage_iff_arithmeticCoverage w).mp h)
215 
216 /-- Actual Frobenius samples with the arithmetic coverage input give the
217 conjugacy density needed on each pair of coefficient-prime good sets. -/
218 theorem arithmetic_dense_good_overlap
219     (w : (p : RationalPrime) → Witness p.val) (h : ArithmeticCoverage w)
220     (good₁ good₂ : RationalPrime → Prop)
221     (h₁ : Set.Finite {p | ¬ good₁ p}) (h₂ : Set.Finite {p | ¬ good₂ p})
222     (bad : Finset RationalPrime) :
223     DenseRange (fun z : {p : RationalPrime // good₁ p ∧ good₂ p ∧ p ∉ bad} × GQ =>
224       z.2 * (w z.1).element * z.2⁻¹) :=
225   dense_good_overlap _ (cofiniteQuotientCoverage_of_arithmeticCoverage w h)
226     good₁ good₂ h₁ h₂ bad
227 
228 end ArithmeticWitnesses
229 end PaperX.GeneralArithmeticCoverage

Back to source controls