CyclotomicAbsoluteArithmeticSeparation.lean

1 import PaperX.CyclotomicAbsoluteSeparation
2 import PaperX.AbsoluteIntegralFrobenius
3 import PaperX.CyclotomicIntegralFrobenius
4 
5 /-! Arithmetic separators with actual absolute-Galois Frobenius witnesses.
6 The common cyclotomic factorization remains explicit. Prime ideals and
7 decomposition elements belong to the integral closure of Z in Qbar. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.CyclotomicAbsoluteArithmeticSeparation
11 open PaperX.CyclotomicPrimeCoverage PaperX.CyclotomicAbsoluteSamples
12 open PaperX.CompatibleSystemRigidity PaperX.FiniteSeparation
13 open PaperX.AbsoluteIntegralFrobenius
14 open scoped Pointwise
15 
16 variable (n : ℕ) [NeZero n] (L : Type*) [Field L] [NumberField L]
17   [IsCyclotomicExtension {n} ℚ L]
18 
19 variable {Λ I E : Type*} [Field E] [Fintype I] [DecidableEq I]
20 variable {K : Λ → Type*} [∀ l, Field (K l)] [∀ l, CharZero (K l)]
21   [∀ l, TopologicalSpace (K l)] [∀ l, IsTopologicalRing (K l)] [∀ l, T2Space (K l)]
22 variable {W : Λ → I → Type*} [∀ l i, AddCommGroup (W l i)]
23   [∀ l i, Module (K l) (W l i)] [∀ l i, FiniteDimensional (K l) (W l i)]
24 variable (ρ : (l : Λ) → (i : I) → Representation (K l) Gal(L/ℚ) (W l i))
25 variable [∀ l i, Representation.IsIrreducible ((ρ l i).comp (restrictionMap n L))]
26 variable (emb : (l : Λ) → E →+* K l) (t : I → PermittedPrime n ∅ → E)
27 variable (good : Λ → PermittedPrime n ∅ → Prop)
28 variable (hgood : ∀ l, Set.Finite {p | ¬ good l p})
29 variable (compat : ∀ l i p, good l p →
30   Representation.character ((ρ l i).comp (restrictionMap n L)) (liftSample n L p) =
31     emb l (t i p))
32 variable (hne : ∀ i j,
33   MemberwiseEquiv (fun l i => (ρ l i).comp (restrictionMap n L)) i j → i = j)
34 
35 include hgood compat hne in
36 /-- Actual arithmetic Frobenius witnesses realize a common invertible trace
37 matrix for absolute-Galois systems factoring through the fixed cyclotomic field.
38 Neither absolute Frobenius witnesses nor quotient coverage are assumed. -/
39 theorem finite_arithmetic_system_separator (l₀ : Λ) (forbidden : Finset ℕ) :
40     ∃ (v : I → PermittedPrime n ∅)
41       (Q : I → Ideal IntegralClosure) (γ : I → GQ),
42       Function.Injective (fun i => (v i).val) ∧
43       (∀ i, good l₀ (v i)) ∧ (∀ i, (v i).val ∉ forbidden) ∧
44       (sampleMatrix t v).det ≠ 0 ∧
45       (∀ l, ((emb l).mapMatrix (sampleMatrix t v)).det ≠ 0) ∧
46       (∀ j, (Q j).IsMaximal ∧ (Q j).LiesOver (Ideal.span {((v j).val : ℤ)}) ∧
47         γ j ∈ MulAction.stabilizer GQ (Q j) ∧
48         ∀ x : IntegralClosure, Ideal.Quotient.mk (Q j) (γ j • x) =
49           (Ideal.Quotient.mk (Q j) x) ^ (v j).val) ∧
50       (∀ j, restrictionMap n L (γ j) = primeSample n L ∅ (v j)) ∧
51       (∀ l i j (δ : GQ), δ ∈ (Q j).inertia GQ →
52         ((ρ l i).comp (restrictionMap n L)) δ = 1) ∧
53       ∀ l j i, good l (v j) →
54         (emb l).mapMatrix (sampleMatrix t v) j i =
55           Representation.character ((ρ l i).comp (restrictionMap n L)) (γ j) := by
56   classical
57   obtain ⟨v, hv, hg, hb, hd, hdl, ht⟩ :=
58     PaperX.CyclotomicAbsoluteSeparation.finite_absolute_system_separator
59       n L ρ emb t good hgood compat hne l₀ forbidden
60   have witnesses : ∀ j : I, ∃ Q : Ideal IntegralClosure,
61       Q.IsMaximal ∧ Q.LiesOver (Ideal.span {((v j).val : ℤ)}) ∧
62       ∃ σ : MulAction.stabilizer GQ Q,
63         ∀ x : IntegralClosure, Ideal.Quotient.mk Q (σ.val • x) =
64           (Ideal.Quotient.mk Q x) ^ (v j).val := by
65     intro j
66     let : Fact (v j).val.Prime := ⟨(v j).property.1⟩
67     exact exists_frobenius (v j).val
68   choose Q hQ hQp σ hσ using witnesses
69   let γ : I → GQ := fun j => (σ j).val
70   have hr : ∀ j, restrictionMap n L (γ j) = primeSample n L ∅ (v j) := by
71     intro j
72     let : (Q j).IsMaximal := hQ j
73     let : (Q j).LiesOver (Ideal.span {((v j).val : ℤ)}) := hQp j
74     let : Fact (v j).val.Prime := ⟨(v j).property.1⟩
75     exact PaperX.CyclotomicIntegralFrobenius.restriction_eq_primePower_of_residue
76       n L (Q j) (v j).val (v j).property.2.1 (γ j) (hσ j)
77   refine ⟨v, Q, γ, hv, hg, hb, hd, hdl, ?_, hr, ?_, ?_⟩
78   · intro j
79     exact ⟨hQ j, hQp j, (σ j).property, hσ j⟩
80   · intro l i j δ hδ
81     let : (Q j).IsMaximal := hQ j
82     let : (Q j).LiesOver (Ideal.span {((v j).val : ℤ)}) := hQp j
83     let : Fact (v j).val.Prime := ⟨(v j).property.1⟩
84     exact PaperX.CyclotomicIntegralFrobenius.pullback_trivial_on_inertia
85       n L (Q j) (v j).val (v j).property.2.1 (ρ l i) δ hδ
86   · intro l j i hp
87     exact ht l j i (γ j) (hr j) hp
88 
89 end PaperX.CyclotomicAbsoluteArithmeticSeparation

Back to source controls