ArithmeticSystemSeparation.lean

1 import PaperX.GeneralArithmeticCoverage
2 import PaperX.CompatibleSystemSeparation
3 
4 /-!
5 # Arithmetic Frobenius coverage to finite compatible-system separation
6 
7 This module composes the existing arithmetic-coverage bridge with the common
8 compatible-system separator.  The only arithmetic existence premise retained is
9 `ExistentialArithmeticCoverage`: prescribed Frobenius conjugacy must occur at an
10 unramified rational prime outside every finite forbidden set.
11 -/
12 
13 set_option autoImplicit false
14 noncomputable section
15 
16 namespace PaperX.ArithmeticSystemSeparation
17 
18 open PaperX.AbsoluteFrobeniusWitnesses
19 open PaperX.AbsoluteIntegralFrobenius
20 open PaperX.GeneralArithmeticCoverage
21 open PaperX.CompatibleSystemRigidity
22 open PaperX.FiniteSeparation PaperX.TraceRecovery
23 
24 variable {Λ I E : Type*} [Field E]
25 variable [Fintype I] [DecidableEq I]
26 variable {K : Λ → Type*} [∀ l, Field (K l)] [∀ l, CharZero (K l)]
27   [∀ l, TopologicalSpace (K l)] [∀ l, IsTopologicalRing (K l)] [∀ l, T2Space (K l)]
28 variable {W : Λ → I → Type*} [∀ l i, AddCommGroup (W l i)]
29   [∀ l i, Module (K l) (W l i)] [∀ l i, FiniteDimensional (K l) (W l i)]
30 variable (ρ : (l : Λ) → (i : I) → Representation (K l) GQ (W l i))
31 variable [∀ l i, (ρ l i).IsIrreducible]
32 variable (hc : ∀ l i, Continuous (ρ l i).character)
33 variable (emb : (l : Λ) → E →+* K l)
34 variable (t : I → RationalPrime → E)
35 variable (good : Λ → RationalPrime → Prop)
36 variable (hgood : ∀ l, Set.Finite {p | ¬ good l p})
37 variable (compat : ∀ l i p, good l p →
38   (ρ l i).character (chosenWitness p).element = emb l (t i p))
39 variable (hne : ∀ i j, MemberwiseEquiv ρ i j → i = j)
40 
41 include hc hgood compat hne in
42 /-- Full finite trace-separator conclusion from the single choice-free
43 prescribed-Frobenius occurrence premise.  All selected rational primes can avoid
44 an arbitrary finite forbidden set. -/
45 theorem finite_arithmetic_system_separator
46     (hcov : ExistentialArithmeticCoverage)
47     (l₀ : Λ) (bad : Finset RationalPrime) :
48     ∃ v : I → RationalPrime, Function.Injective v ∧
49       (∀ i, good l₀ (v i)) ∧ (∀ i, v i ∉ bad) ∧
50       (sampleMatrix t v).det ≠ 0 ∧
51       (∀ l, ((emb l).mapMatrix (sampleMatrix t v)).det ≠ 0) ∧
52       ∀ l j i, good l (v j) →
53         (emb l).mapMatrix (sampleMatrix t v) j i =
54           (ρ l i).character (chosenWitness (v j)).element := by
55   apply PaperX.CompatibleSystemSeparation.finite_system_separator
56     ρ hc emb t good hgood
57     (fun p : RationalPrime => (chosenWitness p).element)
58     (cofiniteQuotientCoverage_of_existentialArithmeticCoverage hcov chosenWitness)
59     compat hne l₀ bad
60 
61 end PaperX.ArithmeticSystemSeparation

Back to source controls