ClassSpines.lean

1 import PaperXII.ClassCompanions
2 
3 /-! Frobenius polynomials and inertia triviality pass from conjugacy-class
4 forests to actual continuous adic and local-field representations.
5 Every finite-level specification below starts at positive precision. -/
6 set_option autoImplicit false
7 namespace PaperXII.ClassSpines
8 
9 open ContinuousMonoidHom Matrix
10 open AdicMatrixGroups AdicCompanions ContinuousClasses ClassCompanions AdicSpines
11 open PaperX.ClassInvariants
12 
13 variable {R Γ ι : Type} [CommRing R] [Group Γ] [TopologicalSpace Γ]
14     [Fintype ι] [DecidableEq ι] (I : Ideal R)
15 
16 /-- Entire prescribed polynomials survive class completion from positive precisions. -/
17 theorem class_spine_preserved [IsHausdorff I R]
18     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
19     (ρ : AdicRealization I (Framed I C))
20     {Ω : Type} (frob : Ω → Γ) (good : Ω → Prop) (P : Ω → Polynomial R)
21     (hspec : ∀ n, 0 < n → ∀ c, C n c → ∀ v, good v →
22       classCharpoly c (frob v) = (P v).map (quotientMap I n)) :
23     ∀ v, good v → (ρ.val (frob v)).val.charpoly = P v := by
24   apply spine_preserved I (Framed I C) ρ frob good P
25   intro n σ hσ v hv
26   cases n with
27   | zero =>
28     let _ := coeff_zero_subsingleton I
29     exact Subsingleton.elim _ _
30   | succ n => exact hspec (n + 1) (Nat.succ_pos n) (classOfRep σ) hσ v hv
31 
32 /-- Positive-precision class triviality gives actual trivial inertia action. -/
33 theorem class_unramified_preserved [IsHausdorff I R]
34     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
35     (ρ : AdicRealization I (Framed I C)) (H : Subgroup Γ)
36     (hspec : ∀ n, 0 < n → ∀ c, C n c → ClassTrivial H c) :
37     ∀ g, g ∈ H → ρ.val g = 1 := by
38   apply unramified_preserved I (Framed I C) ρ H
39   intro n σ hσ
40   cases n with
41   | zero =>
42     let _ := coeff_zero_subsingleton I
43     intro g _
44     exact Subsingleton.elim _ _
45   | succ n =>
46     exact (classTrivial_classOfRep H σ).mp
47       (hspec (n + 1) (Nat.succ_pos n) (classOfRep σ) hσ)
48 
49 /-- A finite occupied class forest gives a continuous integral realization with
50 its residual class, complete Frobenius polynomials, and declared inertia triviality. -/
51 theorem class_realization_with_spine [IsAdicComplete I R]
52     (hI : I.FG) [Finite (R ⧸ I)]
53     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
54     (hC : ∀ n c, C (n + 1) c → C n (classStep I n c))
55     (finiteC : ∀ n, 0 < n → Finite {c // C n c})
56     (hc : ∀ n, 0 < n → ∀ c, C n c → ClassContinuous c)
57     (hne : ∀ n, 0 < n → ∃ c, C n c)
58     (root : LevelClass (Γ := Γ) (ι := ι) I 1) (hroot : ∀ c, C 1 c → c = root)
59     {Ω : Type} (frob : Ω → Γ) (good : Ω → Prop) (P : Ω → Polynomial R)
60     (hspec : ∀ n, 0 < n → ∀ c, C n c → ∀ v, good v →
61       classCharpoly c (frob v) = (P v).map (quotientMap I n))
62     (H : Subgroup Γ) (hH : ∀ n, 0 < n → ∀ c, C n c → ClassTrivial H c) :
63     ∃ ρ : AdicRealization I (Framed I C),
64       classOfRep (reduceRep I 1 ρ.val) = root ∧
65       (∀ v, good v → (ρ.val (frob v)).val.charpoly = P v) ∧
66       ∀ g, g ∈ H → ρ.val g = 1 := by
67   obtain ⟨ρ⟩ := exists_class_realization_positive I hI C hC finiteC hc hne
68   exact ⟨ρ, hroot _ (ρ.property 1),
69     class_spine_preserved I C ρ frob good P hspec,
70     class_unramified_preserved I C ρ H hH⟩
71 
72 /-- Simultaneous continuous local-field realizations from positive finite class forests.
73 Coherent frames are constructed. Local integrality and coefficient-map continuity
74 remain explicit hypotheses, as do finiteness and occupancy of admissible classes. -/
75 theorem simultaneous_class_spine
76     {Λ Ω L : Type} [Field L] (O K : Λ → Type)
77     [∀ l, CommRing (O l)] [∀ l, Field (K l)] [∀ l, TopologicalSpace (K l)]
78     (J : ∀ l, Ideal (O l)) [∀ l, IsAdicComplete (J l) (O l)]
79     (hJ : ∀ l, (J l).FG) [∀ l, Finite (O l ⧸ J l)]
80     (C : ∀ l n, LevelClass (Γ := Γ) (ι := ι) (J l) n → Prop)
81     (hC : ∀ l n c, C l (n + 1) c → C l n (classStep (J l) n c))
82     (finiteC : ∀ l n, 0 < n → Finite {c // C l n c})
83     (hc : ∀ l n, 0 < n → ∀ c, C l n c → ClassContinuous c)
84     (hne : ∀ l n, 0 < n → ∃ c, C l n c)
85     (root : ∀ l, LevelClass (Γ := Γ) (ι := ι) (J l) 1)
86     (hroot : ∀ l c, C l 1 c → c = root l)
87     (inc : ∀ l, O l →+* K l)
88     (hinc : ∀ l, @Continuous (O l) (K l) (J l).adicTopology inferInstance (inc l))
89     (emb : ∀ l, L →+* K l) (frob : Ω → Γ) (good : Λ → Ω → Prop)
90     (P : Ω → Polynomial L) (localP : ∀ l, Ω → Polynomial (O l))
91     (hmatch : ∀ l v, good l v → (localP l v).map (inc l) = (P v).map (emb l))
92     (hspec : ∀ l n, 0 < n → ∀ c, C l n c → ∀ v, good l v →
93       classCharpoly c (frob v) = (localP l v).map (quotientMap (J l) n))
94     (H : Λ → Subgroup Γ)
95     (hH : ∀ l n, 0 < n → ∀ c, C l n c → ClassTrivial (H l) c) :
96     ∃ ρ : ∀ l, AdicRealization (J l) (Framed (J l) (C l)),
97       (∀ l, classOfRep (reduceRep (J l) 1 (ρ l).val) = root l) ∧
98       (∀ l v, good l v →
99         (fieldRep (J l) (inc l) (hinc l) (ρ l).val (frob v)).val.charpoly =
100           (P v).map (emb l)) ∧
101       ∀ l g, g ∈ H l → fieldRep (J l) (inc l) (hinc l) (ρ l).val g = 1 := by
102   classical
103   let ρ : ∀ l, AdicRealization (J l) (Framed (J l) (C l)) := fun l ↦
104     Classical.choice (exists_class_realization_positive (J l) (hJ l) (C l)
105       (hC l) (finiteC l) (hc l) (hne l))
106   refine ⟨ρ, fun l ↦ hroot l _ ((ρ l).property 1), ?_, ?_⟩
107   · intro l v hv
108     exact fieldRep_charpoly (J l) (inc l) (hinc l) (emb l) (ρ l).val (frob v)
109       (localP l v) (P v)
110       (class_spine_preserved (J l) (C l) (ρ l) frob (good l) (localP l) (hspec l) v hv)
111       (hmatch l v hv)
112   · intro l
113     exact fieldRep_unramified (J l) (inc l) (hinc l) (ρ l).val (H l)
114       (class_unramified_preserved (J l) (C l) (ρ l) (H l) (hH l))
115 
116 end PaperXII.ClassSpines

Back to source controls