CompletionConsequences.lean

1 import RealizationBoundaries.ProfiniteCompletion
2 import RealizationBoundaries.Countability
3 import RealizationBoundaries.PureCorrespondence
4 
5 /-! # Canonical consequences of the checked completion theorem -/
6 set_option autoImplicit false
7 set_option backward.isDefEq.respectTransparency false
8 noncomputable section
9 namespace RealizationBoundaries
10 
11 @[simp] theorem preimage_bot_eq_finiteSupport :
12     preimage (⊥ : Submodule ℚ TailSpace) = finiteSupport := by
13   ext x
14   change quotientMap x ∈ (⊥ : Submodule ℚ TailSpace) ↔ x ∈ finiteSupport
15   rw [Submodule.mem_bot, quotientMap_eq_zero_iff]
16 
17 /-- Transport is along literal subgroup equality, retaining its group structure. -/
18 def completionEquivOfEq (W : Submodule ℚ TailSpace) (H : AddSubgroup Ambient)
19     (h : preimage W = H) :
20     ProfiniteAddGrp.ProfiniteCompletion.completion (AddGrpCat.of H) ≃ₜ+ Ambient :=
21   h ▸ profiniteCompletionEquiv W
22 
23 @[simp] theorem completionEquivOfEq_eta (W : Submodule ℚ TailSpace)
24     (H : AddSubgroup Ambient) (h : preimage W = H) (x : H) :
25     completionEquivOfEq W H h
26       (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of H) x) = x.val := by
27   subst H
28   exact profiniteCompletionEquiv_eta W x
29 
30 /-- Monograph Proposition 2.5, for the original finite-support subgroup. -/
31 def finiteSupportCompletionEquiv :
32     ProfiniteAddGrp.ProfiniteCompletion.completion (AddGrpCat.of finiteSupport) ≃ₜ+ Ambient :=
33   completionEquivOfEq ⊥ finiteSupport preimage_bot_eq_finiteSupport
34 
35 @[simp] theorem finiteSupportCompletionEquiv_eta (x : finiteSupport) :
36     finiteSupportCompletionEquiv
37       (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of finiteSupport) x) = x.val :=
38   completionEquivOfEq_eta _ _ _ x
39 
40 /-- All the completions are isomorphic by the canonical coordinate comparisons. -/
41 def commonCompletionEquiv (V W : Submodule ℚ TailSpace) :
42     CanonicalCompletion V ≃ₜ+ CanonicalCompletion W :=
43   (profiniteCompletionEquiv V).trans (profiniteCompletionEquiv W).symm
44 
45 /-- When the rational subspaces are nested, the comparison is exactly the extension
46 of the original subgroup inclusion, as witnessed on every canonical point. -/
47 theorem commonCompletionEquiv_inclusion (V W : Submodule ℚ TailSpace) (h : V ≤ W)
48     (x : preimage V) : commonCompletionEquiv V W
49       (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage V)) x) =
50       ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage W))
51         ⟨x.val, h x.property⟩ := by
52   exact ambientToCompletion_subtype W ⟨x.val, h x.property⟩
53 
54 /-- The abstract group embeds faithfully in its actual profinite completion. -/
55 theorem preimage_eta_injective (W : Submodule ℚ TailSpace) :
56     Function.Injective (ProfiniteAddGrp.ProfiniteCompletion.etaFn
57       (AddGrpCat.of (preimage W))) := by
58   intro x y h
59   apply Subtype.ext
60   exact congrArg (profiniteCompletionEquiv W) h
61 
62 /-- The official residual-finiteness predicate, rather than a replacement definition. -/
63 theorem preimage_residuallyFinite (W : Submodule ℚ TailSpace) :
64     AddGroup.ResiduallyFinite (preimage W) :=
65   (ProfiniteAddGrp.ProfiniteCompletion.etaFn_injective_iff_residuallyFinite
66     (AddGrpCat.of (preimage W))).mp (preimage_eta_injective W)
67 
68 def pairedCompletionEquiv (a : ℕ → Bool) :
69     ProfiniteAddGrp.ProfiniteCompletion.completion (AddGrpCat.of (pairedGroup a)) ≃ₜ+ Ambient :=
70   profiniteCompletionEquiv (selectorLine (pairedSelector a))
71 
72 /-- D is proper inside every paired-prime group, not just dense in it. -/
73 theorem paired_has_nonfiniteSupport (a : ℕ → Bool) :
74     ∃ x : pairedGroup a, x.val ∉ finiteSupport := by
75   refine ⟨markedElement (pairedSelector a), ?_⟩
76   intro h
77   exact indicator_tail_ne_zero (pairedSelector_infinite a)
78     ((quotientMap_eq_zero_iff _).mpr h)
79 
80 theorem finiteSupport_ne_top : finiteSupport ≠ ⊤ := by
81   intro h
82   obtain ⟨x, hx⟩ := paired_has_nonfiniteSupport (fun _ => false)
83   apply hx
84   rw [h]
85   trivial
86 
87 /-- The inclusion D → G_a is not surjective even though its extension to the
88 canonical completions is the isomorphism `commonCompletionEquiv`. -/
89 theorem finiteSupport_inclusion_not_surjective (a : ℕ → Bool) :
90     ¬ Function.Surjective (fun d : finiteSupport =>
91       (⟨d.val, finiteSupport_le_preimage (selectorLine (pairedSelector a)) d.property⟩ : pairedGroup a)) := by
92   obtain ⟨x, hx⟩ := paired_has_nonfiniteSupport a
93   intro hs
94   obtain ⟨d, hd⟩ := hs x
95   apply hx
96   exact (congrArg Subtype.val hd) ▸ d.property
97 
98 /-- Transport the zero-subspace group to the original named D. -/
99 def bottomFiniteSupportEquiv : preimage (⊥ : Submodule ℚ TailSpace) ≃+ finiteSupport where
100   toFun x := ⟨x.val, preimage_bot_eq_finiteSupport ▸ x.property⟩
101   invFun d := ⟨d.val, finiteSupport_le_preimage ⊥ d.property⟩
102   left_inv _ := rfl
103   right_inv _ := rfl
104   map_add' _ _ := rfl
105 
106 def bottomFiniteHomEquiv (F : Type*) [AddGroup F] :
107     (preimage (⊥ : Submodule ℚ TailSpace) →+ F) ≃ (finiteSupport →+ F) where
108   toFun f := f.comp bottomFiniteSupportEquiv.symm.toAddMonoidHom
109   invFun g := g.comp bottomFiniteSupportEquiv.toAddMonoidHom
110   left_inv f := by ext x; rfl
111   right_inv g := by ext x; rfl
112 
113 /-- Monograph Proposition 4.5: natural finite-target equivalence with the original D. -/
114 def finiteSupportRestrictionEquiv (W : Submodule ℚ TailSpace) (F : Type*)
115     [AddGroup F] [Finite F] : (preimage W →+ F) ≃ (finiteSupport →+ F) := by
116   letI : TopologicalSpace F := ⊥
117   letI : DiscreteTopology F := ⟨rfl⟩
118   exact (finiteTargetHomEquiv W F).symm.trans
119     ((finiteTargetHomEquiv ⊥ F).trans (bottomFiniteHomEquiv F))
120 
121 /-- The forward equivalence is literal restriction along D's inclusion. -/
122 @[simp] theorem finiteSupportRestrictionEquiv_apply (W : Submodule ℚ TailSpace) (F : Type*)
123     [AddGroup F] [Finite F] (f : preimage W →+ F) (d : finiteSupport) :
124     finiteSupportRestrictionEquiv W F f d =
125       f ⟨d.val, finiteSupport_le_preimage W d.property⟩ :=
126   finiteTargetExtension_subtype W F f ⟨d.val, finiteSupport_le_preimage W d.property⟩
127 
128 /-- Naturality in all finite target groups is an equality of homomorphisms. -/
129 theorem finiteSupportRestrictionEquiv_natural (W : Submodule ℚ TailSpace)
130     (F E : Type*) [AddGroup F] [Finite F] [AddGroup E] [Finite E]
131     (f : preimage W →+ F) (g : F →+ E) :
132     finiteSupportRestrictionEquiv W E (g.comp f) =
133       g.comp (finiteSupportRestrictionEquiv W F f) := by
134   ext d
135   simp
136 
137 /-- The extension of D → G_a is an actual isomorphism of their canonical completions. -/
138 def finiteSupportToPairedCompletion (a : ℕ → Bool) :
139     ProfiniteAddGrp.ProfiniteCompletion.completion (AddGrpCat.of finiteSupport) ≃ₜ+
140       ProfiniteAddGrp.ProfiniteCompletion.completion (AddGrpCat.of (pairedGroup a)) :=
141   finiteSupportCompletionEquiv.trans (pairedCompletionEquiv a).symm
142 
143 theorem finiteSupportToPairedCompletion_eta (a : ℕ → Bool) (d : finiteSupport) :
144     finiteSupportToPairedCompletion a
145       (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of finiteSupport) d) =
146       ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (pairedGroup a))
147         ⟨d.val, finiteSupport_le_preimage (selectorLine (pairedSelector a)) d.property⟩ := by
148   change (pairedCompletionEquiv a).symm
149     (finiteSupportCompletionEquiv
150       (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of finiteSupport) d)) = _
151   rw [finiteSupportCompletionEquiv_eta]
152   exact ambientToCompletion_subtype (selectorLine (pairedSelector a))
153     ⟨d.val, finiteSupport_le_preimage (selectorLine (pairedSelector a)) d.property⟩
154 
155 end RealizationBoundaries

Back to source controls