CompletionReflection.lean

1 import RealizationBoundaries.DiagonalAutomorphisms
2 import RealizationBoundaries.CompletionConsequences
3 
4 /-!
5 # The induced completion map and reflection for a supplied rank-one map
6 
7 The maps below act on Mathlib's canonical completions. They are constructed from
8 the already checked comparison equivalences and the derived diagonal. Their
9 extension property and uniqueness are proved, identifying them as the induced
10 maps, independently of any alternate implementation of the completion functor.
11 -/
12 set_option autoImplicit false
13 set_option backward.isDefEq.respectTransparency false
14 noncomputable section
15 namespace RealizationBoundaries
16 
17 /-- The actual continuous extension to the canonical profinite completions. -/
18 def completionHom (U V : Submodule ℚ TailSpace) (f : preimage U →+ preimage V) :
19     CanonicalCompletion U →ₜ+ CanonicalCompletion V where
20   toAddMonoidHom := (ambientToCompletion V).comp
21     ((diagonal (homDiagonal U V f)).comp (completionToAmbient U))
22   continuous_toFun := (ambientToCompletion_continuous V).comp
23     ((diagonal_continuous _).comp (completionToAmbient_continuous U))
24 
25 /-- This extension agrees with the supplied original homomorphism on every canonical point. -/
26 @[simp] theorem completionHom_eta (U V : Submodule ℚ TailSpace)
27     (f : preimage U →+ preimage V) (x : preimage U) :
28     completionHom U V f
29       (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage U)) x) =
30       ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage V)) (f x) := by
31   change ambientToCompletion V
32     (diagonal (homDiagonal U V f)
33       (completionToAmbient U
34         (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage U)) x))) = _
35   rw [completionToAmbient_eta, ← hom_eq_diagonal U V f x]
36   exact ambientToCompletion_subtype V (f x)
37 
38 /-- The coordinate formula on the entire completion, not just on its dense subgroup. -/
39 theorem completionHom_coordinates (U V : Submodule ℚ TailSpace)
40     (f : preimage U →+ preimage V) (x : CanonicalCompletion U) :
41     profiniteCompletionEquiv V (completionHom U V f x) =
42       diagonal (homDiagonal U V f) (profiniteCompletionEquiv U x) :=
43   completionToAmbient_ambientToCompletion V _
44 
45 /-- Density makes this the unique continuous extension of the original map. -/
46 theorem completionHom_unique (U V : Submodule ℚ TailSpace)
47     (f : preimage U →+ preimage V) (g : CanonicalCompletion U →ₜ+ CanonicalCompletion V)
48     (hg : ∀ x : preimage U,
49       g (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage U)) x) =
50         ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage V)) (f x)) :
51     g = completionHom U V f := by
52   have he : (fun x => g x) = (fun x => completionHom U V f x) := by
53     apply (ProfiniteAddGrp.ProfiniteCompletion.denseRange
54       (AddGrpCat.of (preimage U))).equalizer g.continuous_toFun
55         (completionHom U V f).continuous_toFun
56     funext x
57     exact (hg x).trans (completionHom_eta U V f x).symm
58   exact ContinuousAddMonoidHom.ext (fun x => congrFun he x)
59 
60 /-- The extension operation respects actual composition. -/
61 theorem completionHom_comp (U V W : Submodule ℚ TailSpace)
62     (f : preimage U →+ preimage V) (g : preimage V →+ preimage W) :
63     completionHom U W (g.comp f) = (completionHom V W g).comp (completionHom U V f) := by
64   symm
65   apply completionHom_unique U W (g.comp f)
66   intro x
67   change completionHom V W g (completionHom U V f
68     (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage U)) x)) = _
69   rw [completionHom_eta, completionHom_eta]
70   rfl
71 
72 /-- Different original homomorphisms remain different after completion. -/
73 theorem completionHom_injective (U V : Submodule ℚ TailSpace) :
74     Function.Injective (completionHom U V) := by
75   intro f g h
76   apply AddMonoidHom.ext
77   intro x
78   apply preimage_eta_injective V
79   calc
80     _ = completionHom U V f
81         (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage U)) x) :=
82       (completionHom_eta U V f x).symm
83     _ = completionHom U V g
84         (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage U)) x) := by rw [h]
85     _ = _ := completionHom_eta U V g x
86 
87 /-- A nonzero diagonal provides an actual topological additive equivalence of completions. -/
88 def completionEquivOfNonzeroDiagonal (U V : Submodule ℚ TailSpace)
89     (f : preimage U →+ preimage V) (hn : ∀ p, homDiagonal U V f p ≠ 0) :
90     CanonicalCompletion U ≃ₜ+ CanonicalCompletion V :=
91   (profiniteCompletionEquiv U).trans
92     ((diagonalAmbientEquiv (homDiagonal U V f) hn).trans (profiniteCompletionEquiv V).symm)
93 
94 @[simp] theorem completionEquivOfNonzeroDiagonal_apply (U V : Submodule ℚ TailSpace)
95     (f : preimage U →+ preimage V) (hn : ∀ p, homDiagonal U V f p ≠ 0)
96     (x : CanonicalCompletion U) :
97     completionEquivOfNonzeroDiagonal U V f hn x = completionHom U V f x := rfl
98 
99 /-- Bijectivity of the induced map is exactly the nonzero-coordinate condition. -/
100 theorem completionHom_bijective_iff (U V : Submodule ℚ TailSpace)
101     (f : preimage U →+ preimage V) :
102     Function.Bijective (completionHom U V f) ↔ ∀ p, homDiagonal U V f p ≠ 0 := by
103   constructor
104   · intro hf
105     apply (hom_injective_iff_diagonal_nonzero U V f).mp
106     intro x y hxy
107     apply preimage_eta_injective U
108     apply hf.1
109     rw [completionHom_eta, completionHom_eta, hxy]
110   · intro hn
111     exact (completionEquivOfNonzeroDiagonal U V f hn).bijective
112 
113 /-- Isomorphism here includes continuity in both directions and equality with the induced map. -/
114 theorem completionHom_isomorphism_iff (U V : Submodule ℚ TailSpace)
115     (f : preimage U →+ preimage V) :
116     (∃ e : CanonicalCompletion U ≃ₜ+ CanonicalCompletion V,
117       ∀ x, e x = completionHom U V f x) ↔ ∀ p, homDiagonal U V f p ≠ 0 := by
118   constructor
119   · rintro ⟨e, he⟩
120     apply (completionHom_bijective_iff U V f).mp
121     constructor
122     · intro x y hxy
123       exact e.injective ((he x).trans (hxy.trans (he y).symm))
124     · intro y
125       obtain ⟨x, hx⟩ := e.surjective y
126       exact ⟨x, (he x).symm.trans hx⟩
127   · intro hn
128     exact ⟨completionEquivOfNonzeroDiagonal U V f hn, fun _ => rfl⟩
129 
130 /-- Monograph Proposition 9.4: reflection for an already supplied rank-one homomorphism. -/
131 theorem selector_completion_reflection (S T : Set Prime) (hS : S.Infinite)
132     (f : selectorGroup S →+ selectorGroup T) :
133     Function.Bijective (completionHom (selectorLine S) (selectorLine T) f) ↔
134       Function.Bijective f := by
135   rw [completionHom_bijective_iff, selector_hom_bijective_iff S T hS]
136 
137 /-- The reflection statement in terms of actual original and completed isomorphisms. -/
138 theorem paired_completion_reflects_isomorphisms (a b : ℕ → Bool)
139     (f : pairedGroup a →+ pairedGroup b) :
140     (∃ e : CanonicalCompletion (selectorLine (pairedSelector a)) ≃ₜ+
141         CanonicalCompletion (selectorLine (pairedSelector b)),
142       ∀ x, e x = completionHom (selectorLine (pairedSelector a))
143         (selectorLine (pairedSelector b)) f x) ↔
144     (∃ e : pairedGroup a ≃+ pairedGroup b, e.toAddMonoidHom = f) := by
145   rw [completionHom_isomorphism_iff]
146   constructor
147   · intro hn
148     exact ⟨selectorEquivOfNonzeroDiagonal _ _ (pairedSelector_infinite a) f hn, rfl⟩
149   · rintro ⟨e, rfl⟩
150     exact (hom_injective_iff_diagonal_nonzero _ _ _).mp e.injective
151 
152 end RealizationBoundaries

Back to source controls