ClassCompanions.lean

1 import PaperXII.ContinuousClasses
2 import Mathlib.RingTheory.Ideal.Quotient.Index
3 
4 /-! Continuous companion completion from actual conjugacy classes.
5 Finite class fibers let compactness choose strictly compatible frames.
6 There is no assumption that conjugating matrices lift through reduction. -/
7 set_option autoImplicit false
8 namespace PaperXII.ClassCompanions
9 
10 open ContinuousMonoidHom Matrix
11 open AdicMatrixGroups AdicCompanions ContinuousClasses
12 open PaperX.RepresentationClasses PaperX.ClassInvariants
13 
14 variable {R Γ ι : Type} [CommRing R] [Group Γ] [TopologicalSpace Γ]
15     [Fintype ι] [DecidableEq ι] (I : Ideal R)
16 
17 /-- Actual conjugacy classes at adic precision n. -/
18 abbrev LevelClass (n : ℕ) := ClassRep (Coeff I n) Γ ι
19 
20 /-- Adjacent reduction of actual conjugacy classes. -/
21 def classStep (n : ℕ) : LevelClass (Γ := Γ) (ι := ι) I (n + 1) →
22     LevelClass (Γ := Γ) (ι := ι) I n :=
23   changeClassCoefficients (coefficientStep I n)
24 
25 /-- Taking classes commutes with the actual continuous reduction map. -/
26 theorem classOfRep_step (n : ℕ) (ρ : Γ →ₜ* GL ι (Coeff I (n + 1))) :
27     classOfRep ((step I n).comp ρ) = classStep I n (classOfRep ρ) := rfl
28 
29 /-- Pull back the class predicate to actual continuous frames. -/
30 def Framed (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
31     (n : ℕ) (ρ : Γ →ₜ* GL ι (Coeff I n)) : Prop := C n (classOfRep ρ)
32 
33 /-- Class admissibility under reduction gives genuine frame admissibility. -/
34 theorem framed_downward (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
35     (hC : ∀ n c, C (n + 1) c → C n (classStep I n c)) :
36     ∀ n ρ, Framed I C (n + 1) ρ → Framed I C n ((step I n).comp ρ) := by
37   intro n ρ hρ
38   exact hC n (classOfRep ρ) hρ
39 
40 /-- Finite coefficients and finitely many classes give finite admissible frame sets. -/
41 theorem framed_finite (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop) (n : ℕ)
42     [Finite (Coeff I n)] [Finite {c // C n c}] :
43     Finite {ρ : Γ →ₜ* GL ι (Coeff I n) // Framed I C n ρ} :=
44   finite_allowed_frames (C n)
45 
46 /-- One admissible continuous class gives one actual admissible continuous frame. -/
47 theorem framed_nonempty (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop) (n : ℕ)
48     (hc : ∀ c, C n c → ClassContinuous c) (hne : ∃ c, C n c) :
49     Nonempty {ρ : Γ →ₜ* GL ι (Coeff I n) // Framed I C n ρ} := by
50   obtain ⟨c, hC⟩ := hne
51   obtain ⟨ρ, hρ⟩ := exists_continuous_representative c (hc c hC)
52   refine ⟨ρ, ?_⟩
53   change C n (classOfRep ρ)
54   rw [hρ]
55   exact hC
56 
57 /-- Finite occupied continuous class levels give a strictly compatible completion.
58 No adic completeness is required for this frame-selection step. -/
59 theorem exists_class_complete
60     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
61     (hC : ∀ n c, C (n + 1) c → C n (classStep I n c))
62     [∀ n, Finite (Coeff I n)] [∀ n, Finite {c // C n c}]
63     (hc : ∀ n c, C n c → ClassContinuous c) (hne : ∀ n, ∃ c, C n c) :
64     Nonempty (InverseLimitRepresentations.Complete (step I) (Framed I C)) := by
65   let _ : ∀ n, Finite {ρ : Γ →ₜ* GL ι (Coeff I n) // Framed I C n ρ} :=
66     fun n ↦ framed_finite I C n
67   exact InverseLimitRepresentations.exists_complete (step I) (Framed I C)
68     (framed_downward I C hC) (fun n ↦ framed_nonempty I C n (hc n) (hne n))
69 
70 /-- Actual continuous integral representations realize finite occupied class forests. -/
71 theorem exists_class_realization [IsAdicComplete I R]
72     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
73     (hC : ∀ n c, C (n + 1) c → C n (classStep I n c))
74     [∀ n, Finite (Coeff I n)] [∀ n, Finite {c // C n c}]
75     (hc : ∀ n c, C n c → ClassContinuous c) (hne : ∀ n, ∃ c, C n c) :
76     Nonempty (AdicRealization I (Framed I C)) := by
77   obtain ⟨c⟩ := exists_class_complete I C hC hc hne
78   exact ⟨fromComplete I (Framed I C) c⟩
79 
80 /-- Fixing a compatible class branch yields a completion over exactly those classes. -/
81 theorem exists_prescribed_complete
82     [∀ n, Finite (Coeff I n)] (c : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n)
83     (hcompat : ∀ n, classStep I n (c (n + 1)) = c n)
84     (hc : ∀ n, ClassContinuous (c n)) :
85     Nonempty (InverseLimitRepresentations.Complete (step I)
86       (Framed I (fun n d ↦ d = c n))) := by
87   let _ : ∀ n, Subsingleton {d // d = c n} :=
88     fun _ ↦ ⟨fun a b ↦ Subtype.ext (a.property.trans b.property.symm)⟩
89   apply exists_class_complete I (fun n d ↦ d = c n)
90   · intro n d hd
91     rw [hd]
92     exact hcompat n
93   · intro n d hd
94     rw [hd]
95     exact hc n
96   · intro n
97     exact ⟨c n, rfl⟩
98 
99 /-- Every prescribed continuous class branch has strictly compatible continuous frames.
100 Neither completeness nor surjectivity of transition maps is assumed. -/
101 theorem prescribed_branch_representatives
102     [∀ n, Finite (Coeff I n)] (c : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n)
103     (hcompat : ∀ n, classStep I n (c (n + 1)) = c n)
104     (hc : ∀ n, ClassContinuous (c n)) :
105     ∃ ρ : ∀ n, Γ →ₜ* GL ι (Coeff I n),
106       (∀ n, (step I n).comp (ρ (n + 1)) = ρ n) ∧
107       ∀ n, classOfRep (ρ n) = c n := by
108   obtain ⟨s⟩ := exists_prescribed_complete I c hcompat hc
109   let hC : ∀ n d, d = c (n + 1) → classStep I n d = c n := by
110     intro n d hd
111     rw [hd]
112     exact hcompat n
113   let b := InverseLimitRepresentations.toBranch (step I)
114     (Framed I (fun n d ↦ d = c n))
115     (framed_downward I _ hC) s
116   exact ⟨fun n ↦ (b.value n).val,
117     fun n ↦ congrArg Subtype.val (b.compatible n), fun n ↦ (b.value n).property⟩
118 
119 /-- A prescribed compatible class branch is realized by an actual continuous adic map. -/
120 theorem prescribed_branch_adic [IsAdicComplete I R]
121     [∀ n, Finite (Coeff I n)] (c : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n)
122     (hcompat : ∀ n, classStep I n (c (n + 1)) = c n)
123     (hc : ∀ n, ClassContinuous (c n)) :
124     ∃ ρ : AdicRep (Γ := Γ) (ι := ι) I, ∀ n, classOfRep (reduceRep I n ρ) = c n := by
125   obtain ⟨s⟩ := exists_prescribed_complete I c hcompat hc
126   exact ⟨realize I (Framed I (fun n d ↦ d = c n)) s,
127     realize_admissible I (Framed I (fun n d ↦ d = c n)) s⟩
128 
129 /-- The declared residual conjugacy class is retained at precision one. -/
130 theorem exists_class_realization_with_root [IsAdicComplete I R]
131     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
132     (hC : ∀ n c, C (n + 1) c → C n (classStep I n c))
133     [∀ n, Finite (Coeff I n)] [∀ n, Finite {c // C n c}]
134     (hc : ∀ n c, C n c → ClassContinuous c) (hne : ∀ n, ∃ c, C n c)
135     (root : LevelClass (Γ := Γ) (ι := ι) I 1) (hroot : ∀ c, C 1 c → c = root) :
136     ∃ ρ : AdicRealization I (Framed I C), classOfRep (reduceRep I 1 ρ.val) = root := by
137   obtain ⟨ρ⟩ := exists_class_realization I C hC hc hne
138   exact ⟨ρ, hroot _ (ρ.property 1)⟩
139 
140 /-- A finitely generated ideal with finite residue gives finite coefficients at every precision. -/
141 theorem finite_coefficients (hI : I.FG) [Finite (R ⧸ I)] (n : ℕ) :
142     Finite (Coeff I n) := Ideal.finite_quotient_pow hI n
143 
144 /-- The auxiliary precision-zero coefficient ring is trivial. -/
145 theorem coeff_zero_subsingleton : Subsingleton (Coeff I 0) := by
146   change Subsingleton (R ⧸ I ^ 0)
147   simp only [pow_zero, Ideal.one_eq_top]
148   infer_instance
149 
150 omit [TopologicalSpace Γ] in
151 /-- Precision zero requires no separate finiteness hypothesis on classes. -/
152 theorem finite_zero_class_level (C : LevelClass (Γ := Γ) (ι := ι) I 0 → Prop) :
153     Finite {c // C c} := by
154   let _ := coeff_zero_subsingleton I
155   let _ : Subsingleton (PaperX.RepresentationLimits.MatrixRep (Coeff I 0) Γ ι) :=
156     ⟨fun a b ↦ by ext g i j; exact Subsingleton.elim _ _⟩
157   let _ : Subsingleton (LevelClass (Γ := Γ) (ι := ι) I 0) := by
158     unfold LevelClass ClassRep
159     infer_instance
160   infer_instance
161 
162 /-- Precision-zero classes are automatically continuous. -/
163 theorem zero_class_continuous (c : LevelClass (Γ := Γ) (ι := ι) I 0) :
164     ClassContinuous c := by
165   let _ := coeff_zero_subsingleton I
166   obtain ⟨ρ, rfl⟩ := classOf_surjective c
167   intro i j g
168   exact Filter.Eventually.of_forall (fun _ ↦ Subsingleton.elim _ _)
169 
170 /-- Positive precision data suffice, matching the manuscript's forest starting at level one. -/
171 theorem exists_class_realization_positive [IsAdicComplete I R]
172     (hI : I.FG) [Finite (R ⧸ I)]
173     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
174     (hC : ∀ n c, C (n + 1) c → C n (classStep I n c))
175     (finiteC : ∀ n, 0 < n → Finite {c // C n c})
176     (hc : ∀ n, 0 < n → ∀ c, C n c → ClassContinuous c)
177     (hne : ∀ n, 0 < n → ∃ c, C n c) :
178     Nonempty (AdicRealization I (Framed I C)) := by
179   let _ : ∀ n, Finite (Coeff I n) := finite_coefficients I hI
180   let _ : ∀ n, Finite {c // C n c} := by
181     intro n
182     cases n with
183     | zero => exact finite_zero_class_level I (C 0)
184     | succ n => exact finiteC (n + 1) (Nat.succ_pos n)
185   apply exists_class_realization I C hC
186   · intro n c h
187     cases n with
188     | zero => exact zero_class_continuous I c
189     | succ n => exact hc (n + 1) (Nat.succ_pos n) c h
190   · intro n
191     cases n with
192     | zero =>
193       obtain ⟨c, h⟩ := hne 1 (by decide)
194       exact ⟨classStep I 0 c, hC 0 c h⟩
195     | succ n => exact hne (n + 1) (Nat.succ_pos n)
196 
197 end PaperXII.ClassCompanions

Back to source controls