ObservationSystems.lean

1 import RealizationBoundaries.ClassificationConsequences
2 import RealizationBoundaries.CompletionReflection
3 import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
4 import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
5 import Mathlib.CategoryTheory.Filtered.Final
6 import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
7 
8 /-!
9 # Finite observation systems and the completion functor
10 
11 The global faithfulness statements below use Mathlib's actual profinite-completion
12 functor on arbitrary groups, rather than a family-specific coordinate extension.
13 -/
14 set_option autoImplicit false
15 set_option backward.isDefEq.respectTransparency false
16 noncomputable section
17 open CategoryTheory
18 namespace RealizationBoundaries
19 
20 /-- Naturality on actual canonical points for the official completion functor. -/
21 theorem official_completion_map_eta {G H : GrpCat} (f : G ⟶ H) (x : G) :
22     ProfiniteGrp.profiniteCompletion.map f
23       (ProfiniteGrp.ProfiniteCompletion.etaFn G x) =
24       ProfiniteGrp.ProfiniteCompletion.etaFn H (f x) := by
25   exact ConcreteCategory.congr_hom
26     (ProfiniteGrp.ProfiniteCompletion.lift_eta
27       (f ≫ ProfiniteGrp.ProfiniteCompletion.eta H)) x
28 
29 /-- Completion distinguishes maps whenever their target is residually finite.
30 No commutativity, countability, continuity or source residual-finiteness is needed. -/
31 theorem official_completion_map_injective {G H : GrpCat}
32     (hH : Group.ResiduallyFinite H) :
33     Function.Injective (ProfiniteGrp.profiniteCompletion.map (X := G) (Y := H)) := by
34   intro f g h
35   ext x
36   apply (ProfiniteGrp.ProfiniteCompletion.etaFn_injective_iff_residuallyFinite H).mpr hH
37   rw [← official_completion_map_eta f x, ← official_completion_map_eta g x, h]
38 
39 /-- The full category of all residually finite groups and all group homomorphisms. -/
40 def residuallyFiniteObjects : ObjectProperty GrpCat := fun G => Group.ResiduallyFinite G
41 
42 abbrev ResiduallyFiniteGrp := residuallyFiniteObjects.FullSubcategory
43 
44 /-- The restriction of the official profinite-completion functor. -/
45 def residuallyFiniteCompletion : ResiduallyFiniteGrp ⥤ ProfiniteGrp :=
46   residuallyFiniteObjects.ι ⋙ ProfiniteGrp.profiniteCompletion
47 
48 /-- Monograph 9.3, the unrestricted categorical faithfulness assertion. -/
49 instance residuallyFiniteCompletion_faithful : residuallyFiniteCompletion.Faithful where
50   map_injective := by
51     intro X Y f g h
52     apply ObjectProperty.hom_ext
53     exact official_completion_map_injective Y.property h
54 
55 /-- A presentation of the full source category whose objects are the paired groups.
56 Every abstract additive group homomorphism is a morphism. -/
57 abbrev PairedGroupCategory := InducedCategory AddGrpCat
58   (fun a : ℕ → Bool => AddGrpCat.of (pairedGroup a))
59 
60 /-- The family completion functor on actual canonical profinite completions. -/
61 def pairedCompletionFunctor : PairedGroupCategory ⥤ ProfiniteAddGrp where
62   obj a := CanonicalCompletion (selectorLine (pairedSelector a))
63   map f := ProfiniteAddGrp.ofHom (completionHom _ _ f.hom.hom)
64   map_id a := by
65     apply ConcreteCategory.hom_ext
66     intro x
67     have he := completionHom_unique (selectorLine (pairedSelector a))
68       (selectorLine (pairedSelector a)) (AddMonoidHom.id _)
69       (ContinuousAddMonoidHom.id _) (fun _ => rfl)
70     exact congrArg (fun h => h x) he.symm
71   map_comp f g := by
72     apply ConcreteCategory.hom_ext
73     intro x
74     exact congrArg (fun h => h x) (completionHom_comp _ _ _ f.hom.hom g.hom.hom)
75 
76 instance pairedCompletionFunctor_faithful : pairedCompletionFunctor.Faithful where
77   map_injective := by
78     intro a b f g h
79     apply InducedCategory.hom_ext
80     apply AddGrpCat.hom_ext
81     apply completionHom_injective (selectorLine (pairedSelector a))
82       (selectorLine (pairedSelector b))
83     exact congrArg (fun m => m.hom) h
84 
85 /-- The completion morphism given by the common coordinates has no source lift. -/
86 theorem pairedCompletionFunctor_not_full : ¬ pairedCompletionFunctor.Full := by
87   intro hf
88   let : pairedCompletionFunctor.Full := hf
89   let a : PairedGroupCategory := fun _ => false
90   let b : PairedGroupCategory := fun _ => true
91   let g : pairedCompletionFunctor.obj a ⟶ pairedCompletionFunctor.obj b :=
92     ProfiniteAddGrp.ofHom {
93       toAddMonoidHom := (pairedCommonCompletionEquiv a b).toAddMonoidHom
94       continuous_toFun := (pairedCommonCompletionEquiv a b).continuous_toFun
95     }
96   obtain ⟨f, hfg⟩ := pairedCompletionFunctor.map_surjective g
97   apply no_lift_of_commonCompletionEquiv a b constant_selectors_infinite_disagreement
98   refine ⟨f.hom.hom, ?_⟩
99   intro x
100   have h := ConcreteCategory.congr_hom hfg
101     (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (pairedGroup a)) x)
102   exact h.symm.trans (completionHom_eta _ _ f.hom.hom x)
103 
104 /-- Finite sets of primes, ordered in the direction of quotient restriction. -/
105 abbrev CoordinateIndex := OrderDual (Finset Prime)
106 
107 /-- The source-free finite coordinate groups. -/
108 abbrev FiniteCoordinates (s : CoordinateIndex) := (p : {p : Prime // p ∈ s.ofDual}) → Coordinate p.val
109 
110 def finiteCoordinateProjection (W : Submodule ℚ TailSpace) (s : CoordinateIndex) :
111     preimage W →+ FiniteCoordinates s where
112   toFun x p := x.val p.val
113   map_zero' := rfl
114   map_add' _ _ := rfl
115 
116 def finiteCoordinateRestriction {s t : CoordinateIndex} (h : s ≤ t) :
117     FiniteCoordinates s →+ FiniteCoordinates t where
118   toFun x p := x ⟨p.val, h p.property⟩
119   map_zero' := rfl
120   map_add' _ _ := rfl
121 
122 /-- This diagram contains no dense source group or evaluations of named elements. -/
123 def coordinateObservation : CoordinateIndex ⥤ FiniteAddGrp where
124   obj s := FiniteAddGrp.of (FiniteCoordinates s)
125   map f := FiniteAddGrp.ofHom (finiteCoordinateRestriction f.le)
126   map_id _ := by ext; rfl
127   map_comp _ _ := by ext; rfl
128 
129 /-- The actual kernel indexing the corresponding quotient of the original group. -/
130 def finiteCoordinateIndex (W : Submodule ℚ TailSpace) (s : CoordinateIndex) : CompletionIndex W :=
131   FiniteIndexNormalAddSubgroup.ofAddSubgroup (finiteCoordinateProjection W s).ker
132 
133 theorem finiteCoordinateIndex_mono (W : Submodule ℚ TailSpace) :
134     Monotone (finiteCoordinateIndex W) := by
135   intro s t h x hx
136   change finiteCoordinateProjection W t x = 0
137   funext p
138   exact congrFun hx ⟨p.val, h p.property⟩
139 
140 /-- The inclusion of the finite-coordinate quotient subsystem in all finite quotients. -/
141 def coordinateIndexFunctor (W : Submodule ℚ TailSpace) : CoordinateIndex ⥤ CompletionIndex W :=
142   (show CoordinateIndex →o CompletionIndex W from
143     ⟨finiteCoordinateIndex W, finiteCoordinateIndex_mono W⟩).monotone.functor
144 
145 /-- Every finite quotient is dominated by an actual finite-coordinate quotient. -/
146 theorem finiteCoordinateIndex_cofinal (W : Submodule ℚ TailSpace) (K : CompletionIndex W) :
147     ∃ s : CoordinateIndex, finiteCoordinateIndex W s ≤ K := by
148   let F := preimage W ⧸ K.toAddSubgroup
149   let : Fintype F := Fintype.ofFinite F
150   let m := Fintype.card F
151   have hm : 0 < m := Fintype.card_pos
152   let s : CoordinateIndex := OrderDual.toDual ((exceptional_finite hm).toFinset)
153   refine ⟨s, ?_⟩
154   intro x hx
155   have hcoord : coordinateMap W m x = 0 := by
156     funext p
157     exact congrFun hx ⟨p.val, by
158       change p.val ∈ (exceptional_finite hm).toFinset
159       exact (exceptional_finite hm).mem_toFinset.mpr p.property⟩
160   have hk := finite_target_coordinate_kernel W F (quotientProjection W K) hcoord
161   exact (QuotientAddGroup.eq_zero_iff x).mp hk
162 
163 /-- Categorical initiality records genuine cofinal reindexing of this inverse system. -/
164 instance coordinateIndexFunctor_initial (W : Submodule ℚ TailSpace) :
165     (coordinateIndexFunctor W).Initial := by
166   apply (Functor.initial_iff_of_isCofiltered _).mpr
167   constructor
168   · intro K
169     obtain ⟨s, hs⟩ := finiteCoordinateIndex_cofinal W K
170     exact ⟨s, ⟨hs.hom⟩⟩
171   · intro K s f g
172     exact ⟨s, 𝟙 s, Subsingleton.elim _ _⟩
173 
174 /-- Extension by zero proves that these are quotient groups, not just finite targets. -/
175 theorem finiteCoordinateProjection_surjective (W : Submodule ℚ TailSpace) (s : CoordinateIndex) :
176     Function.Surjective (finiteCoordinateProjection W s) := by
177   intro z
178   let x : Ambient := fun p => if hp : p ∈ s.ofDual then z ⟨p, hp⟩ else 0
179   have hx : x ∈ finiteSupport := by
180     apply s.ofDual.finite_toSet.subset
181     intro p hp
182     by_contra hn
183     have hn' : p ∉ s.ofDual := hn
184     exact hp (by simp [x, hn'])
185   refine ⟨⟨x, finiteSupport_le_preimage W hx⟩, ?_⟩
186   funext p
187   change x p.val = z p
188   simp [x, p.property]
189 
190 /-- The canonical quotient-coordinate comparison. -/
191 def finiteCoordinateQuotientEquiv (W : Submodule ℚ TailSpace) (s : CoordinateIndex) :
192     (preimage W ⧸ (finiteCoordinateIndex W s).toAddSubgroup) ≃+ FiniteCoordinates s :=
193   QuotientAddGroup.quotientKerEquivOfSurjective (finiteCoordinateProjection W s)
194     (finiteCoordinateProjection_surjective W s)
195 
196 /-- The genuine all-finite-quotient diagram becomes the common coordinate diagram
197 under the categorically initial finite-coordinate reindexing. -/
198 def coordinateObservationIso (W : Submodule ℚ TailSpace) :
199     coordinateIndexFunctor W ⋙ ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram
200       (AddGrpCat.of (preimage W)) ≅ coordinateObservation :=
201   NatIso.ofComponents (fun s => {
202     hom := FiniteAddGrp.ofHom (finiteCoordinateQuotientEquiv W s).toAddMonoidHom
203     inv := FiniteAddGrp.ofHom (finiteCoordinateQuotientEquiv W s).symm.toAddMonoidHom
204     hom_inv_id := by ext x; exact (finiteCoordinateQuotientEquiv W s).symm_apply_apply x
205     inv_hom_id := by ext x; exact (finiteCoordinateQuotientEquiv W s).apply_symm_apply x
206   }) (by
207     intro s t f
208     ext x
209     refine QuotientAddGroup.induction_on x ?_
210     intro y
211     rfl)
212 
213 /-- Finite quotient kernels form a nonempty cofiltered index category. -/
214 instance completionIndex_cofiltered (W : Submodule ℚ TailSpace) :
215     IsCofiltered (CompletionIndex W) := by
216   let : Nonempty (CompletionIndex W) := ⟨finiteCoordinateIndex W (OrderDual.toDual ∅)⟩
217   infer_instance
218 
219 /-- An unmarked observation contains only a finite-group diagram. In particular
220 there is no source group and no distinguished image of any source element. -/
221 structure FiniteObservation where
222   Index : Type
223   [category : SmallCategory Index]
224   [cofiltered : IsCofiltered Index]
225   diagram : Index ⥤ FiniteAddGrp
226 
227 attribute [instance] FiniteObservation.category FiniteObservation.cofiltered
228 
229 /-- The actual system over all finite-index normal subgroups. -/
230 def allFiniteObservation (W : Submodule ℚ TailSpace) : FiniteObservation where
231   Index := CompletionIndex W
232   diagram := ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram (AddGrpCat.of (preimage W))
233 
234 /-- Isomorphism after a common initial (inverse-system cofinal) reindexing.
235 Every pro-object invariant must respect this explicitly certified comparison. -/
236 def CommonCofinalObservation (A B : FiniteObservation) : Prop :=
237   ∃ (I : Type) (_ : SmallCategory I) (F : I ⥤ A.Index) (G : I ⥤ B.Index),
238     IsCofiltered I ∧ F.Initial ∧ G.Initial ∧ Nonempty (F ⋙ A.diagram ≅ G ⋙ B.diagram)
239 
240 /-- All rational preimages have the same unmarked finite-quotient observation
241 under a source-free, compatible and genuinely cofinal comparison. -/
242 theorem allFiniteObservation_common (U V : Submodule ℚ TailSpace) :
243     CommonCofinalObservation (allFiniteObservation U) (allFiniteObservation V) := by
244   refine ⟨CoordinateIndex, inferInstance, coordinateIndexFunctor U,
245     coordinateIndexFunctor V, inferInstance, coordinateIndexFunctor_initial U,
246     coordinateIndexFunctor_initial V, ?_⟩
247   exact ⟨(coordinateObservationIso U).trans (coordinateObservationIso V).symm⟩
248 
249 /-- An arbitrary decoder invariant under certified pro-object comparisons.
250 No computability or definability restriction is imposed. -/
251 structure ObservationDecoder where
252   decode : FiniteObservation → AddGrpCat
253   invariant : ∀ A B, CommonCofinalObservation A B → Nonempty (decode A ≅ decode B)
254 
255 /-- Monograph 9.1: no isomorphism-invariant decoder of the actual unmarked
256 finite-quotient systems recovers every paired source group. -/
257 theorem no_unmarked_observation_decoder (R : ObservationDecoder)
258     (recovers : ∀ a : ℕ → Bool, Nonempty
259       (R.decode (allFiniteObservation (selectorLine (pairedSelector a))) ≅
260         AddGrpCat.of (pairedGroup a))) : False := by
261   obtain ⟨ea⟩ := recovers (fun _ => false)
262   obtain ⟨eb⟩ := recovers (fun _ => true)
263   obtain ⟨er⟩ := R.invariant _ _ (allFiniteObservation_common _ _)
264   exact constant_groups_not_isomorphic
265     ⟨((ea.symm.trans er).trans eb).addGroupIsoToAddEquiv⟩
266 
267 /-- The source category with D (the zero-subspace preimage) and all paired groups. -/
268 def boundarySubspace : Option (ℕ → Bool) → Submodule ℚ TailSpace
269   | none => ⊥
270   | some a => selectorLine (pairedSelector a)
271 
272 abbrev BoundaryGroupCategory := InducedCategory AddGrpCat
273   (fun i : Option (ℕ → Bool) => AddGrpCat.of (preimage (boundarySubspace i)))
274 
275 /-- Completion on the enlarged full source category. -/
276 def boundaryCompletionFunctor : BoundaryGroupCategory ⥤ ProfiniteAddGrp where
277   obj i := CanonicalCompletion (boundarySubspace i)
278   map f := ProfiniteAddGrp.ofHom (completionHom _ _ f.hom.hom)
279   map_id i := by
280     apply ConcreteCategory.hom_ext
281     intro x
282     have he := completionHom_unique (boundarySubspace i) (boundarySubspace i)
283       (AddMonoidHom.id _) (ContinuousAddMonoidHom.id _) (fun _ => rfl)
284     exact congrArg (fun h => h x) he.symm
285   map_comp f g := by
286     apply ConcreteCategory.hom_ext
287     intro x
288     exact congrArg (fun h => h x) (completionHom_comp _ _ _ f.hom.hom g.hom.hom)
289 
290 /-- The literal inclusion of the zero-subspace preimage, which equals D. -/
291 def bottomToPaired (a : ℕ → Bool) :
292     preimage (⊥ : Submodule ℚ TailSpace) →+ pairedGroup a :=
293   AddSubgroup.inclusion ((preimage_le_iff ⊥ (selectorLine (pairedSelector a))).mpr bot_le)
294 
295 /-- The enlarged full source category contains a proper inclusion. -/
296 theorem bottomToPaired_not_surjective (a : ℕ → Bool) :
297     ¬ Function.Surjective (bottomToPaired a) := by
298   obtain ⟨x, hx⟩ := paired_has_nonfiniteSupport a
299   intro hs
300   obtain ⟨d, hd⟩ := hs x
301   apply hx
302   have hdmem : d.val ∈ finiteSupport := preimage_bot_eq_finiteSupport ▸ d.property
303   exact congrArg Subtype.val hd ▸ hdmem
304 
305 /-- This inclusion's induced map is exactly the common-coordinate equivalence. -/
306 theorem bottomToPaired_completion (a : ℕ → Bool) :
307     completionHom ⊥ (selectorLine (pairedSelector a)) (bottomToPaired a) =
308       { toAddMonoidHom := (commonCompletionEquiv ⊥ (selectorLine (pairedSelector a))).toAddMonoidHom
309         continuous_toFun := (commonCompletionEquiv ⊥ (selectorLine (pairedSelector a))).continuous_toFun } := by
310   symm
311   apply completionHom_unique
312   intro x
313   exact commonCompletionEquiv_inclusion ⊥ (selectorLine (pairedSelector a)) bot_le x
314 
315 /-- The failure to reflect isomorphisms is categorical, on the precise enlarged
316 full source category, and witnessed by the actual inclusion D → G_a. -/
317 theorem boundaryCompletionFunctor_not_reflects_isomorphisms :
318     ¬ boundaryCompletionFunctor.ReflectsIsomorphisms := by
319   intro hreflect
320   let : boundaryCompletionFunctor.ReflectsIsomorphisms := hreflect
321   let a : ℕ → Bool := fun _ => false
322   let i : BoundaryGroupCategory := none
323   let j : BoundaryGroupCategory := some a
324   let f : i ⟶ j := InducedCategory.homMk (AddGrpCat.ofHom (bottomToPaired a))
325   let e := commonCompletionEquiv ⊥ (selectorLine (pairedSelector a))
326   let iso : boundaryCompletionFunctor.obj i ≅ boundaryCompletionFunctor.obj j := {
327     hom := ProfiniteAddGrp.ofHom {
328       toAddMonoidHom := e.toAddMonoidHom
329       continuous_toFun := e.continuous_toFun }
330     inv := ProfiniteAddGrp.ofHom {
331       toAddMonoidHom := e.symm.toAddMonoidHom
332       continuous_toFun := e.symm.continuous_toFun }
333     hom_inv_id := by ext x; exact e.symm_apply_apply x
334     inv_hom_id := by ext x; exact e.apply_symm_apply x
335   }
336   have hmap : boundaryCompletionFunctor.map f = iso.hom := by
337     apply ConcreteCategory.hom_ext
338     intro x
339     exact congrArg (fun h => h x) (bottomToPaired_completion a)
340   have : IsIso (boundaryCompletionFunctor.map f) := hmap.symm ▸ iso.isIso_hom
341   have : IsIso f := isIso_of_reflects_iso f boundaryCompletionFunctor
342   have : IsIso f.hom := (inducedFunctor
343     (fun k : Option (ℕ → Bool) => AddGrpCat.of (preimage (boundarySubspace k)))).map_isIso f
344   exact bottomToPaired_not_surjective a ((AddGrpCat.epi_iff_surjective f.hom).mp inferInstance)
345 
346 end RealizationBoundaries

Back to source controls