CyclotomicAbsoluteSeparation.lean

1 import PaperX.CyclotomicAbsoluteSamples
2 import PaperX.CyclotomicSystemSeparation
3 import PaperX.SurjectiveRepresentationPullback
4 
5 /-! Prime separators for actual absolute-Galois representations obtained from
6 one fixed cyclotomic quotient. Values agree at every global lift of the finite
7 arithmetic Frobenius. This statement does not turn arbitrary choices of such
8 lifts into a dense sample in the full absolute Galois group. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.CyclotomicAbsoluteSeparation
12 open PaperX.CyclotomicPrimeCoverage PaperX.CyclotomicAbsoluteSamples
13 open PaperX.CompatibleSystemRigidity PaperX.FiniteSeparation
14 open PaperX.SurjectiveRepresentationPullback
15 
16 variable (n : ℕ) [NeZero n] (L : Type*) [Field L] [NumberField L]
17   [IsCyclotomicExtension {n} ℚ L]
18 
19 omit [NeZero n] in
20 /-- Pullback through the actual finite restriction is continuous for any
21 chosen topology on the coefficient endomorphisms. -/
22 theorem pullback_action_continuous {K V : Type*} [Field K] [AddCommGroup V]
23     [Module K V] [TopologicalSpace (Module.End K V)]
24     (ρ : Representation K Gal(L/ℚ) V) :
25     Continuous (fun γ : Field.absoluteGaloisGroup ℚ => (ρ.comp (restrictionMap n L)) γ) :=
26   (continuous_of_discreteTopology : Continuous (fun σ : Gal(L/ℚ) => ρ σ)).comp
27     (restrictionMap_continuous n L)
28 
29 section Systems
30 variable {Λ I E : Type*} [Field E] [Fintype I] [DecidableEq I]
31 variable {K : Λ → Type*} [∀ l, Field (K l)] [∀ l, CharZero (K l)]
32   [∀ l, TopologicalSpace (K l)] [∀ l, IsTopologicalRing (K l)] [∀ l, T2Space (K l)]
33 variable {W : Λ → I → Type*} [∀ l i, AddCommGroup (W l i)]
34   [∀ l i, Module (K l) (W l i)] [∀ l i, FiniteDimensional (K l) (W l i)]
35 variable (ρ : (l : Λ) → (i : I) → Representation (K l) Gal(L/ℚ) (W l i))
36 variable [∀ l i, Representation.IsIrreducible ((ρ l i).comp (restrictionMap n L))]
37 variable (emb : (l : Λ) → E →+* K l) (t : I → PermittedPrime n ∅ → E)
38 variable (good : Λ → PermittedPrime n ∅ → Prop)
39 variable (hgood : ∀ l, Set.Finite {p | ¬ good l p})
40 variable (compat : ∀ l i p, good l p →
41   Representation.character ((ρ l i).comp (restrictionMap n L)) (liftSample n L p) =
42     emb l (t i p))
43 variable (hne : ∀ i j,
44   MemberwiseEquiv (fun l i => (ρ l i).comp (restrictionMap n L)) i j → i = j)
45 
46 include hgood compat hne in
47 /-- Distinct actual absolute-Galois systems factoring through the fixed field
48 admit a common algebraic separator at distinct permitted rational primes.
49 The ordinary trace identity holds for every lift of the finite Frobenius and
50 retains each member's good-prime condition. -/
51 theorem finite_absolute_system_separator (l₀ : Λ) (forbidden : Finset ℕ) :
52     ∃ v : I → PermittedPrime n ∅, Function.Injective (fun i => (v i).val) ∧
53       (∀ i, good l₀ (v i)) ∧ (∀ i, (v i).val ∉ forbidden) ∧
54       (sampleMatrix t v).det ≠ 0 ∧
55       (∀ l, ((emb l).mapMatrix (sampleMatrix t v)).det ≠ 0) ∧
56       ∀ l j i (γ : Field.absoluteGaloisGroup ℚ),
57         restrictionMap n L γ = primeSample n L ∅ (v j) → good l (v j) →
58         (emb l).mapMatrix (sampleMatrix t v) j i =
59           Representation.character ((ρ l i).comp (restrictionMap n L)) γ := by
60   let : ∀ l i, (ρ l i).IsIrreducible := fun l i =>
61     (isIrreducible_iff (restrictionMap n L) (restrictionMap_surjective n L) (ρ l i)).mp
62       inferInstance
63   have hc : ∀ l i p, good l p →
64       (ρ l i).character (primeSample n L ∅ p) = emb l (t i p) := by
65     intro l i p hp
66     simpa only [character_pullback, restriction_liftSample] using compat l i p hp
67   have hn : ∀ i j, MemberwiseEquiv ρ i j → i = j := by
68     intro i j hij
69     exact hne i j ((memberwiseEquiv_iff (restrictionMap n L)
70       (restrictionMap_surjective n L) ρ i j).mpr hij)
71   obtain ⟨v, hv, hg, hb, hd, hdl, ht⟩ :=
72     PaperX.CyclotomicSystemSeparation.finite_prime_system_separator_avoiding
73       n L ρ emb t good hgood hc hn l₀ forbidden
74   refine ⟨v, hv, hg, hb, hd, hdl, ?_⟩
75   intro l j i γ hγ hp
76   rw [pullback_character_on_lift n L (ρ l i) (v j) γ hγ]
77   exact ht l j i hp
78 
79 end Systems
80 end PaperX.CyclotomicAbsoluteSeparation

Back to source controls