Source: ProCGroups.InverseSystems.CategoricalLimits
1import ProCGroups.InverseSystems.Basic
2import Mathlib.Topology.Category.TopCat.Limits.Basic
3import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
5/-!
6# Categorical inverse limits
8This file connects the concrete compatible-family inverse limit used by `ProCGroups` with
9mathlib's categorical limit API. Since the index and the stages may live in unrelated universes,
10each stage is moved to their common universe with `ULift`; the public comparison formulas make
11that lift explicit.
12-/
14open CategoryTheory CategoryTheory.Limits Opposite
15open scoped Topology
17namespace ProCGroups
18namespace InverseSystems
19namespace InverseSystem
21universe u v
23variable {I : Type u} [Preorder I] (S : InverseSystem.{u, v} (I := I))
25/-! ## Topological spaces -/
27/-- A transition map after moving both stages to the common index/stage universe. -/
28def topCatTransition {i j : I} (hij : i ≤ j) :
29 TopCat.of (ULift.{u} (S.X j)) ⟶ TopCat.of (ULift.{u} (S.X i)) :=
30 TopCat.ofHom
31 { toFun := fun x => ULift.up (S.map hij x.down)
32 continuous_toFun :=
33 continuous_uliftUp.comp ((S.continuous_map hij).comp continuous_uliftDown) }
35/-- The contravariant diagram of topological spaces associated to an inverse system. -/
36def topCatDiagram : Iᵒᵖ ⥤ TopCat.{max u v} where
37 obj i := TopCat.of (ULift.{u} (S.X (unop i)))
38 map f := S.topCatTransition (leOfHom f.unop)
39 map_id i := by
40 apply ConcreteCategory.hom_ext
41 intro x
42 apply ULift.ext
43 exact S.map_id_apply (unop i) x.down
44 map_comp f g := by
45 apply ConcreteCategory.hom_ext
46 intro x
47 apply ULift.ext
48 exact (S.map_comp_apply (leOfHom g.unop) (leOfHom f.unop) x.down).symm
50/-- A concrete projection, with its codomain moved to the common universe. -/
51def topCatProjection (i : I) :
52 TopCat.of S.inverseLimit ⟶ TopCat.of (ULift.{u} (S.X i)) :=
53 TopCat.ofHom
54 { toFun := fun x => ULift.up (S.projection i x)
55 continuous_toFun := continuous_uliftUp.comp (S.continuous_projection i) }
57/-- The concrete compatible-family inverse limit as a cone in `TopCat`. -/
58def topCatCone : Cone S.topCatDiagram where
59 pt := TopCat.of S.inverseLimit
60 π :=
61 { app := fun i => S.topCatProjection (unop i)
62 naturality := by
63 intro i j f
64 apply ConcreteCategory.hom_ext
65 intro x
66 apply ULift.ext
67 exact (S.projection_compatible x (unop j) (unop i) (leOfHom f.unop)).symm }
69/-- A categorical cone supplies a compatible family of maps into the original, unlifted stages. -/
70private theorem compatibleMapsOfTopCatCone (c : Cone S.topCatDiagram) :
71 S.CompatibleMaps (fun i (x : c.pt) => (c.π.app (op i) x).down) := by
72 intro i j hij
73 funext x
74 exact congrArg ULift.down (ConcreteCategory.congr_hom (c.w (homOfLE hij).op) x)
76/-- The concrete compatible-family cone is a limit cone in `TopCat`. -/
77def topCatConeIsLimit : IsLimit S.topCatCone where
78 lift c := TopCat.ofHom
79 { toFun := S.inverseLimitLift
80 (fun i (x : c.pt) => (c.π.app (op i) x).down)
81 (S.compatibleMapsOfTopCatCone c)
82 continuous_toFun := S.continuous_inverseLimitLift
83 (fun i (x : c.pt) => (c.π.app (op i) x).down)
84 (fun i => by
85 change Continuous (fun x : c.pt => (c.π.app (op i) x).down)
86 exact continuous_uliftDown.comp (c.π.app (op i)).hom.continuous)
87 (S.compatibleMapsOfTopCatCone c) }
88 fac c i := by
89 apply ConcreteCategory.hom_ext
90 intro x
91 apply ULift.ext
92 rfl
93 uniq c f hf := by
94 apply ConcreteCategory.hom_ext
95 intro x
96 apply S.ext
97 intro i
98 exact congrArg ULift.down (ConcreteCategory.congr_hom (hf (op i)) x)
100/-- The canonical categorical isomorphism from the concrete inverse limit to mathlib's chosen
101limit object in `TopCat`. -/
102noncomputable def topCatIsoLimit :
103 S.topCatCone.pt ≅ limit S.topCatDiagram :=
104 S.topCatConeIsLimit.conePointUniqueUpToIso (limit.isLimit _)
106/-- The concrete inverse limit is canonically homeomorphic to mathlib's categorical limit in
107`TopCat`. -/
108noncomputable def homeomorphTopCatLimit :
109 S.inverseLimit ≃ₜ (limit S.topCatDiagram : TopCat.{max u v}) :=
110 TopCat.homeoOfIso S.topCatIsoLimit
112/-- The canonical homeomorphism commutes with every lifted inverse-limit projection. -/
113@[simp] theorem limitπ_homeomorphTopCatLimit_apply (i : I) (x : S.inverseLimit) :
114 limit.π S.topCatDiagram (op i) (S.homeomorphTopCatLimit x) =
115 ULift.up (S.projection i x) := by
116 exact ConcreteCategory.congr_hom
117 (S.topCatConeIsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) (op i)) x
119/-! ## Profinite groups -/
121section ProfiniteGroups
123variable [∀ i, Group (S.X i)] [IsGroupSystem S]
124variable [∀ i, IsTopologicalGroup (S.X i)]
125variable [∀ i, CompactSpace (S.X i)] [∀ i, TotallyDisconnectedSpace (S.X i)]
127local instance (i : I) : TotallyDisconnectedSpace (ULift.{u} (S.X i)) :=
128 Homeomorph.ulift.symm.totallyDisconnectedSpace
130/-- A transition map of a profinite group inverse system, lifted to the common universe. -/
131def transitionContinuousMonoidHom {i j : I} (hij : i ≤ j) :
132 ULift.{u} (S.X j) →ₜ* ULift.{u} (S.X i) where
133 toFun := fun x => ULift.up (S.map hij x.down)
134 map_one' := by
135 apply ULift.ext
136 exact IsGroupSystem.map_one (S := S) hij
137 map_mul' := by
138 intro x y
139 apply ULift.ext
140 exact IsGroupSystem.map_mul (S := S) hij x.down y.down
141 continuous_toFun :=
142 continuous_uliftUp.comp ((S.continuous_map hij).comp continuous_uliftDown)
144/-- A projection of a profinite group inverse limit, lifted to the common universe. -/
145def projectionContinuousMonoidHom (i : I) :
146 S.inverseLimit →ₜ* ULift.{u} (S.X i) where
147 toFun := fun x => ULift.up (S.projection i x)
148 map_one' := by
149 apply ULift.ext
150 exact projection_one (S := S) i
151 map_mul' := by
152 intro x y
153 apply ULift.ext
154 exact projection_mul (S := S) i x y
155 continuous_toFun := continuous_uliftUp.comp (S.continuous_projection i)
157/-- The contravariant diagram in `ProfiniteGrp` associated to a profinite group inverse system. -/
158def profiniteGrpDiagram : Iᵒᵖ ⥤ ProfiniteGrp.{max u v} where
159 obj i := ProfiniteGrp.of (ULift.{u} (S.X (unop i)))
160 map f := ProfiniteGrp.ofHom (S.transitionContinuousMonoidHom (leOfHom f.unop))
161 map_id i := by
162 apply ConcreteCategory.hom_ext
163 intro x
164 apply ULift.ext
165 exact S.map_id_apply (unop i) x.down
166 map_comp f g := by
167 apply ConcreteCategory.hom_ext
168 intro x
169 apply ULift.ext
170 exact (S.map_comp_apply (leOfHom g.unop) (leOfHom f.unop) x.down).symm
172/-- The concrete compatible-family inverse limit as a cone in `ProfiniteGrp`. -/
173def profiniteGrpCone : Cone S.profiniteGrpDiagram where
174 pt := ProfiniteGrp.of S.inverseLimit
175 π :=
176 { app := fun i => ProfiniteGrp.ofHom (S.projectionContinuousMonoidHom (unop i))
177 naturality := by
178 intro i j f
179 apply ConcreteCategory.hom_ext
180 intro x
181 apply ULift.ext
182 exact (S.projection_compatible x (unop j) (unop i) (leOfHom f.unop)).symm }
184/-- A cone in `ProfiniteGrp` supplies compatible maps into the original, unlifted stages. -/
185private theorem compatibleMapsOfProfiniteGrpCone (c : Cone S.profiniteGrpDiagram) :
186 S.CompatibleMaps (fun i (x : c.pt) => (c.π.app (op i) x).down) := by
187 intro i j hij
188 funext x
189 exact congrArg ULift.down (ConcreteCategory.congr_hom (c.w (homOfLE hij).op) x)
191/-- The concrete compatible-family cone is a limit cone in `ProfiniteGrp`. -/
192def profiniteGrpConeIsLimit : IsLimit S.profiniteGrpCone where
193 lift c := ProfiniteGrp.ofHom
194 { toFun := S.inverseLimitLift
195 (fun i (x : c.pt) => (c.π.app (op i) x).down)
196 (S.compatibleMapsOfProfiniteGrpCone c)
197 map_one' := by
198 apply S.ext
199 intro i
200 change (c.π.app (op i) 1).down = 1
201 exact congrArg ULift.down (c.π.app (op i)).hom.map_one
202 map_mul' := by
203 intro x y
204 apply S.ext
205 intro i
206 change (c.π.app (op i) (x * y)).down =
207 (c.π.app (op i) x).down * (c.π.app (op i) y).down
208 exact congrArg ULift.down ((c.π.app (op i)).hom.map_mul x y)
209 continuous_toFun := S.continuous_inverseLimitLift
210 (fun i (x : c.pt) => (c.π.app (op i) x).down)
211 (fun i => by
212 change Continuous (fun x : c.pt => (c.π.app (op i) x).down)
213 exact continuous_uliftDown.comp (c.π.app (op i)).hom.continuous_toFun)
214 (S.compatibleMapsOfProfiniteGrpCone c) }
215 fac c i := by
216 apply ConcreteCategory.hom_ext
217 intro x
218 apply ULift.ext
219 rfl
220 uniq c f hf := by
221 apply ConcreteCategory.hom_ext
222 intro x
223 apply S.ext
224 intro i
225 exact congrArg ULift.down (ConcreteCategory.congr_hom (hf (op i)) x)
227/-- The canonical isomorphism in `ProfiniteGrp` from the concrete inverse limit to mathlib's
228chosen categorical limit. -/
229noncomputable def profiniteGrpIsoLimit :
230 S.profiniteGrpCone.pt ≅ limit S.profiniteGrpDiagram :=
231 S.profiniteGrpConeIsLimit.conePointUniqueUpToIso (limit.isLimit _)
233/-- The concrete inverse limit is canonically continuously and multiplicatively equivalent to
234mathlib's categorical limit in `ProfiniteGrp`. -/
235noncomputable def continuousMulEquivProfiniteGrpLimit :
236 S.inverseLimit ≃ₜ* (limit S.profiniteGrpDiagram : ProfiniteGrp.{max u v}) :=
237 { CompHausLike.homeoOfIso
238 ((forget₂ ProfiniteGrp Profinite).mapIso S.profiniteGrpIsoLimit) with
239 map_mul' := S.profiniteGrpIsoLimit.hom.hom.map_mul }
241/-- The canonical continuous multiplicative equivalence commutes with every lifted projection. -/
242@[simp] theorem limitπ_continuousMulEquivProfiniteGrpLimit_apply
243 (i : I) (x : S.inverseLimit) :
244 limit.π S.profiniteGrpDiagram (op i)
245 (S.continuousMulEquivProfiniteGrpLimit x) = ULift.up (S.projection i x) := by
246 exact ConcreteCategory.congr_hom
247 (S.profiniteGrpConeIsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) (op i)) x
249end ProfiniteGroups
251end InverseSystem
252end InverseSystems
253end ProCGroups