ProfiniteCompletion.lean

1 import RealizationBoundaries.FiniteTargets
2 import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
3 
4 /-!
5 # The actual profinite-completion identification
6 
7 The completion here is Mathlib's limit over ALL finite-index normal additive
8 subgroups. It is not a newly named copy of the desired product. Both comparison
9 maps are constructed and their inverse laws are proved using dense ranges.
10 -/
11 set_option autoImplicit false
12 set_option backward.isDefEq.respectTransparency false
13 noncomputable section
14 open CategoryTheory
15 namespace RealizationBoundaries
16 
17 abbrev CanonicalCompletion (W : Submodule ℚ TailSpace) :=
18   ProfiniteAddGrp.ProfiniteCompletion.completion (AddGrpCat.of (preimage W))
19 
20 abbrev CompletionIndex (W : Submodule ℚ TailSpace) :=
21   FiniteIndexNormalAddSubgroup (preimage W)
22 
23 def quotientProjection (W : Submodule ℚ TailSpace) (K : CompletionIndex W) :
24     preimage W →+ (preimage W ⧸ K.toAddSubgroup) := QuotientAddGroup.mk' K.toAddSubgroup
25 
26 def quotientTransition (W : Submodule ℚ TailSpace) {K L : CompletionIndex W} (h : K ≤ L) :
27     (preimage W ⧸ K.toAddSubgroup) →+ (preimage W ⧸ L.toAddSubgroup) :=
28   QuotientAddGroup.map _ _ (AddMonoidHom.id _) h
29 
30 @[simp] theorem quotientTransition_projection (W : Submodule ℚ TailSpace)
31     {K L : CompletionIndex W} (h : K ≤ L) :
32     (quotientTransition W h).comp (quotientProjection W K) = quotientProjection W L := by
33   ext x
34   rfl
35 
36 /-- Assemble the extended quotient maps into a point of the genuine inverse limit. -/
37 def ambientToCompletion (W : Submodule ℚ TailSpace) : Ambient →+ CanonicalCompletion W where
38   toFun x := ⟨fun K => finiteTargetExtension W _ (quotientProjection W K) x, by
39     intro K L f
40     change quotientTransition W f.le
41       (finiteTargetExtension W _ (quotientProjection W K) x) =
42         finiteTargetExtension W _ (quotientProjection W L) x
43     have h := finiteTargetExtension_natural W _ _
44       (quotientProjection W K) (quotientTransition W f.le)
45     rw [quotientTransition_projection] at h
46     exact (DFunLike.congr_fun h x).symm⟩
47   map_zero' := by
48     apply Subtype.ext
49     funext K
50     exact map_zero (finiteTargetExtension W _ (quotientProjection W K))
51   map_add' x y := by
52     apply Subtype.ext
53     funext K
54     exact map_add (finiteTargetExtension W _ (quotientProjection W K)) x y
55 
56 theorem ambientToCompletion_continuous (W : Submodule ℚ TailSpace) :
57     Continuous (ambientToCompletion W) := by
58   apply continuous_induced_rng.mpr
59   apply continuous_pi
60   intro K
61   let : TopologicalSpace (preimage W ⧸ K.toAddSubgroup) := ⊥
62   exact finiteTargetExtension_continuous W _ (quotientProjection W K)
63 
64 @[simp] theorem ambientToCompletion_subtype (W : Submodule ℚ TailSpace) (x : preimage W) :
65     ambientToCompletion W x.val =
66       ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage W)) x := by
67   apply Subtype.ext
68   funext K
69   exact finiteTargetExtension_subtype W _ (quotientProjection W K) x
70 
71 /-- The individual prime coordinate, as a homomorphism on the actual dense subgroup. -/
72 def primeCoordinate (W : Submodule ℚ TailSpace) (p : Prime) : preimage W →+ Coordinate p where
73   toFun x := x.val p
74   map_zero' := rfl
75   map_add' _ _ := rfl
76 
77 /-- Its kernel is an actual finite-index normal subgroup in the completion diagram. -/
78 def primeCoordinateIndex (W : Submodule ℚ TailSpace) (p : Prime) : CompletionIndex W :=
79   FiniteIndexNormalAddSubgroup.ofAddSubgroup (primeCoordinate W p).ker
80 
81 /-- Read one prime coordinate from Mathlib's actual profinite completion. -/
82 def completionCoordinate (W : Submodule ℚ TailSpace) (p : Prime) :
83     CanonicalCompletion W →+ Coordinate p where
84   toFun x := QuotientAddGroup.lift (primeCoordinate W p).ker (primeCoordinate W p) le_rfl
85     (x.val (primeCoordinateIndex W p))
86   map_zero' := map_zero _
87   map_add' x y := map_add _ (x.val (primeCoordinateIndex W p))
88     (y.val (primeCoordinateIndex W p))
89 
90 theorem completionCoordinate_continuous (W : Submodule ℚ TailSpace) (p : Prime) :
91     Continuous (completionCoordinate W p) := by
92   let : TopologicalSpace (preimage W ⧸ (primeCoordinate W p).ker) := ⊥
93   let : DiscreteTopology (preimage W ⧸ (primeCoordinate W p).ker) := ⟨rfl⟩
94   exact (continuous_of_discreteTopology : Continuous
95     (QuotientAddGroup.lift (primeCoordinate W p).ker (primeCoordinate W p) le_rfl)).comp
96       ((continuous_apply (primeCoordinateIndex W p)).comp continuous_subtype_val)
97 
98 @[simp] theorem completionCoordinate_eta (W : Submodule ℚ TailSpace) (p : Prime)
99     (x : preimage W) : completionCoordinate W p
100       (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage W)) x) = x.val p := rfl
101 
102 /-- The comparison map from the actual profinite completion to the fixed product. -/
103 def completionToAmbient (W : Submodule ℚ TailSpace) : CanonicalCompletion W →+ Ambient where
104   toFun x p := completionCoordinate W p x
105   map_zero' := by funext p; exact map_zero (completionCoordinate W p)
106   map_add' x y := by funext p; exact map_add (completionCoordinate W p) x y
107 
108 theorem completionToAmbient_continuous (W : Submodule ℚ TailSpace) :
109     Continuous (completionToAmbient W) :=
110   continuous_pi fun p => completionCoordinate_continuous W p
111 
112 @[simp] theorem completionToAmbient_eta (W : Submodule ℚ TailSpace) (x : preimage W) :
113     completionToAmbient W
114       (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage W)) x) = x.val := rfl
115 
116 /-- The comparison is an inverse on the entire ambient product, not just on H_W. -/
117 theorem completionToAmbient_ambientToCompletion (W : Submodule ℚ TailSpace) (x : Ambient) :
118     completionToAmbient W (ambientToCompletion W x) = x := by
119   have heq : (fun y => completionToAmbient W (ambientToCompletion W y)) = id := by
120     apply (preimage_denseRange W).equalizer
121       ((completionToAmbient_continuous W).comp (ambientToCompletion_continuous W)) continuous_id
122     funext y
123     simp
124   exact congrFun heq x
125 
126 /-- The reverse inverse law uses the dense canonical map into Mathlib's completion. -/
127 theorem ambientToCompletion_completionToAmbient (W : Submodule ℚ TailSpace)
128     (x : CanonicalCompletion W) : ambientToCompletion W (completionToAmbient W x) = x := by
129   have heq : (fun y => ambientToCompletion W (completionToAmbient W y)) = id := by
130     apply (ProfiniteAddGrp.ProfiniteCompletion.denseRange (AddGrpCat.of (preimage W))).equalizer
131       ((ambientToCompletion_continuous W).comp (completionToAmbient_continuous W)) continuous_id
132     funext y
133     simp
134   exact congrFun heq x
135 
136 /-- Monograph completion theorem: the canonical profinite completion is topologically
137 and additively isomorphic to P, with the canonical embedding respected. -/
138 def profiniteCompletionEquiv (W : Submodule ℚ TailSpace) : CanonicalCompletion W ≃ₜ+ Ambient where
139   toFun := completionToAmbient W
140   invFun := ambientToCompletion W
141   left_inv := ambientToCompletion_completionToAmbient W
142   right_inv := completionToAmbient_ambientToCompletion W
143   map_add' := map_add (completionToAmbient W)
144   continuous_toFun := completionToAmbient_continuous W
145   continuous_invFun := ambientToCompletion_continuous W
146 
147 @[simp] theorem profiniteCompletionEquiv_eta (W : Submodule ℚ TailSpace) (x : preimage W) :
148     profiniteCompletionEquiv W
149       (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage W)) x) = x.val := rfl
150 
151 /-- The canonical map is a topological embedding for the induced product topology. -/
152 theorem completion_eta_isEmbedding (W : Submodule ℚ TailSpace) :
153     Topology.IsEmbedding (ProfiniteAddGrp.ProfiniteCompletion.etaFn
154       (AddGrpCat.of (preimage W))) := by
155   have heq : ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of (preimage W)) =
156       (profiniteCompletionEquiv W).symm ∘ (fun x : preimage W => x.val) := by
157     funext x
158     exact (ambientToCompletion_subtype W x).symm
159   rw [heq]
160   exact (profiniteCompletionEquiv W).symm.toHomeomorph.isEmbedding.comp
161     Topology.IsEmbedding.subtypeVal
162 
163 /-- The full profinite topology is the initial topology of the canonical map into
164 the limit of all finite quotient groups. -/
165 @[instance_reducible] def fullProfiniteTopology (W : Submodule ℚ TailSpace) : TopologicalSpace (preimage W) :=
166   TopologicalSpace.induced (ProfiniteAddGrp.ProfiniteCompletion.etaFn
167     (AddGrpCat.of (preimage W))) inferInstance
168 
169 /-- No topology from the finite quotients is missing from the induced product topology. -/
170 theorem fullProfiniteTopology_eq (W : Submodule ℚ TailSpace) :
171     fullProfiniteTopology W = (inferInstance : TopologicalSpace (preimage W)) :=
172   (completion_eta_isEmbedding W).isInducing.eq_induced.symm
173 
174 end RealizationBoundaries

Back to source controls