CyclotomicSystemSeparation.lean

1 import PaperX.CyclotomicPrimeCoverage
2 import PaperX.CompatibleSystemSeparation
3 import Mathlib.Data.Finset.Preimage
4 
5 /-! Arithmetic prime separators for representations of a fixed finite cyclotomic
6 Galois group. Prime coverage survives arbitrary finite exclusions by the proved
7 Dirichlet theorem. The existing Krull topology is discrete for this number-field
8 extension, so continuity of the representation characters is automatic.
9 The automorphisms use the arithmetic p-power Frobenius convention established
10 in `CyclotomicPrimeCoverage`; they are not elements of the full absolute Galois group. -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperX.CyclotomicSystemSeparation
14 open PaperX.CyclotomicPrimeCoverage PaperX.CofiniteConjugacyCoverage
15 open PaperX.CompatibleSystemRigidity PaperX.FiniteSeparation
16 
17 variable (n : ℕ) [NeZero n] (L : Type*) [Field L] [NumberField L]
18   [IsCyclotomicExtension {n} ℚ L]
19 
20 /-- Every finite deletion of permitted rational primes still covers the actual
21 finite cyclotomic Galois group, hence every one of its open normal quotients. -/
22 theorem primeSample_cofiniteQuotientCoverage (forbidden : Finset ℕ) :
23     CofiniteQuotientCoverage (primeSample n L forbidden) := by
24   classical
25   intro bad H σ
26   obtain ⟨p, hpgt, hσ⟩ := exists_prime_with_automorphism n L forbidden σ
27     ((bad.image Subtype.val).sup id)
28   have hp : p ∉ bad := by
29     intro hm
30     have hle : p.val ≤ (bad.image Subtype.val).sup id :=
31       Finset.le_sup (f := id) (Finset.mem_image.mpr ⟨p, hm, rfl⟩)
32     exact (not_lt_of_ge hle) hpgt
33   refine ⟨⟨p, hp⟩, 1, ?_⟩
34   simp [hσ]
35 
36 /-- Density on any cofinite good-prime set is a consequence of arithmetic prime
37 existence for this extension, not an additional sampling hypothesis. -/
38 theorem dense_good_prime_samples (good : PermittedPrime n ∅ → Prop)
39     (hgood : Set.Finite {p | ¬ good p}) :
40     DenseRange (fun q : {p : PermittedPrime n ∅ // good p} × Gal(L/ℚ) =>
41       q.2 * primeSample n L ∅ q.1 * q.2⁻¹) :=
42   dense_on_cofinite _ (primeSample_cofiniteQuotientCoverage n L ∅) good hgood
43 
44 section Systems
45 variable {Λ I E : Type*} [Field E] [Fintype I] [DecidableEq I]
46 variable {K : Λ → Type*} [∀ l, Field (K l)] [∀ l, CharZero (K l)]
47   [∀ l, TopologicalSpace (K l)] [∀ l, IsTopologicalRing (K l)] [∀ l, T2Space (K l)]
48 variable {W : Λ → I → Type*} [∀ l i, AddCommGroup (W l i)]
49   [∀ l i, Module (K l) (W l i)] [∀ l i, FiniteDimensional (K l) (W l i)]
50 variable (ρ : (l : Λ) → (i : I) → Representation (K l) Gal(L/ℚ) (W l i))
51 variable [∀ l i, (ρ l i).IsIrreducible]
52 variable (emb : (l : Λ) → E →+* K l) (t : I → PermittedPrime n ∅ → E)
53 variable (good : Λ → PermittedPrime n ∅ → Prop)
54 variable (hgood : ∀ l, Set.Finite {p | ¬ good l p})
55 variable (compat : ∀ l i p, good l p →
56   (ρ l i).character (primeSample n L ∅ p) = emb l (t i p))
57 variable (hne : ∀ i j, MemberwiseEquiv ρ i j → i = j)
58 
59 include hgood compat hne in
60 /-- Pairwise componentwise nonisomorphic systems on the fixed cyclotomic Galois
61 group have a common algebraic prime separator. Its determinant remains nonzero
62 under every coefficient embedding. Each actual trace comparison retains its own
63 member's good-prime condition. No coverage or character-continuity hypothesis is supplied. -/
64 theorem finite_prime_system_separator (l₀ : Λ) (bad : Finset (PermittedPrime n ∅)) :
65     ∃ v : I → PermittedPrime n ∅, Function.Injective v ∧
66       (∀ i, good l₀ (v i)) ∧ (∀ i, v i ∉ bad) ∧
67       (sampleMatrix t v).det ≠ 0 ∧
68       (∀ l, ((emb l).mapMatrix (sampleMatrix t v)).det ≠ 0) ∧
69       ∀ l j i, good l (v j) →
70         (emb l).mapMatrix (sampleMatrix t v) j i =
71           (ρ l i).character (primeSample n L ∅ (v j)) := by
72   exact PaperX.CompatibleSystemSeparation.finite_system_separator ρ
73     (fun _ _ => continuous_of_discreteTopology) emb t good hgood
74     (primeSample n L ∅) (primeSample_cofiniteQuotientCoverage n L ∅) compat hne l₀ bad
75 
76 include hgood compat hne in
77 /-- Exclusions can be stated directly as a finite set of rational primes.
78 The selected underlying natural numbers are pairwise distinct. -/
79 theorem finite_prime_system_separator_avoiding (l₀ : Λ) (forbidden : Finset ℕ) :
80     ∃ v : I → PermittedPrime n ∅, Function.Injective (fun i => (v i).val) ∧
81       (∀ i, good l₀ (v i)) ∧ (∀ i, (v i).val ∉ forbidden) ∧
82       (sampleMatrix t v).det ≠ 0 ∧
83       (∀ l, ((emb l).mapMatrix (sampleMatrix t v)).det ≠ 0) ∧
84       ∀ l j i, good l (v j) →
85         (emb l).mapMatrix (sampleMatrix t v) j i =
86           (ρ l i).character (primeSample n L ∅ (v j)) := by
87   classical
88   let bad : Finset (PermittedPrime n ∅) :=
89     forbidden.preimage Subtype.val Subtype.val_injective.injOn
90   obtain ⟨v, hv, hg, hb, hd, hdl, ht⟩ :=
91     finite_prime_system_separator n L ρ emb t good hgood compat hne l₀ bad
92   refine ⟨v, Subtype.val_injective.comp hv, hg, ?_, hd, hdl, ht⟩
93   intro i hp
94   exact hb i (Finset.mem_preimage.mpr hp)
95 
96 end Systems
97 
98 /-- The conductor-four instance uses Mathlib's actual cyclotomic field over ℚ. -/
99 def quarticSample (p : PermittedPrime 4 ∅) : Gal(CyclotomicField 4 ℚ/ℚ) := by
100   let : IsCyclotomicExtension {4} ℚ (CyclotomicField 4 ℚ) :=
101     CyclotomicField.isCyclotomicExtension 4 ℚ
102   exact primeSample 4 (CyclotomicField 4 ℚ) ∅ p
103 
104 /-- Concrete arithmetic coverage for the actual conductor-four field survives
105 arbitrary finite deletions of permitted rational primes. -/
106 theorem quartic_cofinite_coverage : CofiniteQuotientCoverage quarticSample := by
107   let : IsCyclotomicExtension {4} ℚ (CyclotomicField 4 ℚ) :=
108     CyclotomicField.isCyclotomicExtension 4 ℚ
109   exact primeSample_cofiniteQuotientCoverage 4 (CyclotomicField 4 ℚ) ∅
110 
111 /-- Every automorphism of the conductor-four field occurs at arbitrarily large
112 actual rational primes, with the previously fixed arithmetic convention. -/
113 theorem exists_large_quartic_sample (σ : Gal(CyclotomicField 4 ℚ/ℚ)) (B : ℕ) :
114     ∃ p : PermittedPrime 4 ∅, B < p.val ∧ quarticSample p = σ := by
115   let : IsCyclotomicExtension {4} ℚ (CyclotomicField 4 ℚ) :=
116     CyclotomicField.isCyclotomicExtension 4 ℚ
117   exact exists_prime_with_automorphism 4 (CyclotomicField 4 ℚ) ∅ σ B
118 
119 end PaperX.CyclotomicSystemSeparation

Back to source controls