ClassificationConsequences.lean

1 import RealizationBoundaries.HomomorphismObstruction
2 import RealizationBoundaries.NormalFormTransport
3 import RealizationBoundaries.CompletionConsequences
4 
5 /-!
6 # Finite-change controls and a canonical completion reconstruction obstruction
7 
8 The example of a changed marked point is distinguished from a changed abstract
9 group. The completion counterexample compares objects; it does not assert that
10 an already supplied homomorphism becomes invertible without being invertible.
11 -/
12 set_option autoImplicit false
13 set_option backward.isDefEq.respectTransparency false
14 noncomputable section
15 namespace RealizationBoundaries
16 
17 def toggleBit (a : ℕ → Bool) (k : ℕ) : ℕ → Bool :=
18   fun n => if n = k then !(a n) else a n
19 
20 theorem toggleBit_disagreement (a : ℕ → Bool) (k : ℕ) :
21     {n : ℕ | a n ≠ toggleBit a k n} = {k} := by
22   ext n
23   by_cases hn : n = k
24   · subst n
25     cases a k <;> simp [toggleBit]
26   · simp [toggleBit, hn]
27 
28 theorem toggleBit_ne (a : ℕ → Bool) (k : ℕ) : a ≠ toggleBit a k := by
29   intro h
30   have hk := congrFun h k
31   cases ha : a k <;> simp [toggleBit, ha] at hk
32 
33 /-- One changed bit leaves the original ambient subgroup literally unchanged. -/
34 theorem toggleBit_group_eq (a : ℕ → Bool) (k : ℕ) :
35     pairedGroup a = pairedGroup (toggleBit a k) := by
36   apply pairedGroup_eq_of_finite_disagreement
37   rw [toggleBit_disagreement]
38   exact Set.finite_singleton k
39 
40 /-- Yet no isomorphism of these groups preserves the prescribed marked elements. -/
41 theorem toggleBit_not_marked_isomorphic (a : ℕ → Bool) (k : ℕ) :
42     ¬ ∃ e : pairedGroup a ≃+ pairedGroup (toggleBit a k),
43       e (markedElement (pairedSelector a)) = markedElement (pairedSelector (toggleBit a k)) := by
44   rw [pairedGroup_marked_isomorphic_iff]
45   exact toggleBit_ne a k
46 
47 /-- A concrete two-object witness: the constant selectors disagree at every index. -/
48 theorem constant_selectors_infinite_disagreement :
49     {n : ℕ | (fun _ : ℕ => false) n ≠ (fun _ : ℕ => true) n}.Infinite := by
50   simpa using (Set.infinite_univ : (Set.univ : Set ℕ).Infinite)
51 
52 theorem constant_groups_not_isomorphic :
53     ¬ Nonempty (pairedGroup (fun _ => false) ≃+ pairedGroup (fun _ => true)) := by
54   rw [pairedGroup_isomorphic_iff]
55   exact constant_selectors_infinite_disagreement
56 
57 /-- All actual canonical completions are isomorphic as topological additive groups. -/
58 def pairedCommonCompletionEquiv (a b : ℕ → Bool) :
59     CanonicalCompletion (selectorLine (pairedSelector a)) ≃ₜ+
60       CanonicalCompletion (selectorLine (pairedSelector b)) :=
61   commonCompletionEquiv _ _
62 
63 /-- Same canonical completion, but no isomorphism of the original groups. -/
64 theorem completion_object_counterexample :
65     ∃ a b : ℕ → Bool,
66       Nonempty (CanonicalCompletion (selectorLine (pairedSelector a)) ≃ₜ+
67         CanonicalCompletion (selectorLine (pairedSelector b))) ∧
68       ¬ Nonempty (pairedGroup a ≃+ pairedGroup b) :=
69   ⟨(fun _ => false), (fun _ => true),
70     ⟨pairedCommonCompletionEquiv _ _⟩, constant_groups_not_isomorphic⟩
71 
72 /-- No assignment of groups can both respect isomorphism of these canonical
73 completions and recover every original paired group. No computability is assumed.
74 The assignment is allowed arbitrary selector-indexed outputs, making the obstruction
75 stronger than restricting a priori to a particular algorithm or description language. -/
76 theorem no_completion_invariant_reconstruction (R : (ℕ → Bool) → Type*)
77     [∀ a, AddGroup (R a)]
78     (invariant : ∀ a b,
79       Nonempty (CanonicalCompletion (selectorLine (pairedSelector a)) ≃ₜ+
80         CanonicalCompletion (selectorLine (pairedSelector b))) → Nonempty (R a ≃+ R b))
81     (recovers : ∀ a, Nonempty (R a ≃+ pairedGroup a)) : False := by
82   obtain ⟨ea⟩ := recovers (fun _ => false)
83   obtain ⟨eb⟩ := recovers (fun _ => true)
84   obtain ⟨er⟩ := invariant (fun _ => false) (fun _ => true) ⟨pairedCommonCompletionEquiv _ _⟩
85   exact constant_groups_not_isomorphic ⟨(ea.symm.trans er).trans eb⟩
86 
87 /-- The coordinate identity between completions cannot lift to a group homomorphism
88 when the selectors disagree infinitely. This is an explicit map-level nonfullness witness. -/
89 theorem no_lift_of_commonCompletionEquiv (a b : ℕ → Bool)
90     (h : {n : ℕ | a n ≠ b n}.Infinite) :
91     ¬ ∃ f : pairedGroup a →+ pairedGroup b, ∀ x : pairedGroup a,
92       pairedCommonCompletionEquiv a b
93         (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (pairedGroup a)) x) =
94       ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (pairedGroup b)) (f x) := by
95   rintro ⟨f, hf⟩
96   apply no_injective_hom_of_infinite_disagreement a b h f
97   intro x y hxy
98   have hη := congrArg (ProfiniteAddGrp.ProfiniteCompletion.etaFn
99     (AddGrpCat.of (pairedGroup b))) hxy
100   exact (preimage_eta_injective (selectorLine (pairedSelector a)))
101     ((pairedCommonCompletionEquiv a b).injective ((hf x).trans (hη.trans (hf y).symm)))
102 
103 end RealizationBoundaries

Back to source controls