Yamaguchi Lean 4 Library
Source: ProCGroups.InverseSystems.Basic
ProCGroups/InverseSystems/Basic/Source

Source: ProCGroups.InverseSystems.Basic

1import Mathlib.Topology.Algebra.Ring.Basic
2import Mathlib.Algebra.Module.Pi
4/-!
5# Concrete inverse systems and their limits
7This module defines preorder-indexed inverse systems of topological spaces and realizes their
8inverse limit as the subtype of compatible families. It proves the topological universal
9property and equips limits of group, additive-group, module, and ring systems with their
10coordinatewise algebraic structures and canonical projection homomorphisms.
11-/
13open Set
14open scoped Topology
16namespace ProCGroups
17namespace InverseSystems
19universe u v w z
21section
23variable {I : Type u} [Preorder I]
25/-- An inverse system of topological spaces indexed by a preorder. -/
26structure InverseSystem where
27 /-- The topological space assigned to each index of the system. -/
28 X : I → Type v
29 /-- The chosen topology on every stage; this field supplies the stagewise topology instance. -/
30 topologicalSpace : ∀ i, TopologicalSpace (X i)
31 /-- The contravariant transition map from stage `j` to stage `i` whenever `i ≤ j`. -/
32 map : ∀ {i j : I}, i ≤ j → X j → X i
33 /-- Every transition map is continuous for the chosen stage topologies. -/
34 continuous_map : ∀ {i j : I} (hij : i ≤ j), Continuous (map hij)
35 /-- Transition along a reflexive comparison is the identity map. -/
36 map_id : ∀ i, map (le_rfl : i ≤ i) = id
37 /-- Transition maps compose according to transitivity of the indexing preorder. -/
38 map_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
39 map hij ∘ map hjk = map (hij.trans hjk)
41attribute [instance] InverseSystem.topologicalSpace
43namespace InverseSystem
45variable (S : InverseSystem.{u, v} (I := I))
47/-- The transition map along \(i \le i\) is the identity on points. -/
48@[simp] theorem map_id_apply (i : I) (x : S.X i) :
49 S.map (le_rfl : i ≤ i) x = x := by
50 simpa using congrFun (S.map_id i) x
52/--
53Following the transition from `k` to `j` by the transition from `j` to `i` agrees pointwise with
54the direct transition from `k` to `i`.
55-/
56@[simp] theorem map_comp_apply {i j k : I} (hij : i ≤ j) (hjk : j ≤ k) (x : S.X k) :
57 S.map hij (S.map hjk x) = S.map (hij.trans hjk) x := by
58 simpa [Function.comp] using congrFun (S.map_comp hij hjk) x
60/-- Compatibility of a family of points in the product. -/
61def Compatible (x : ∀ i, S.X i) : Prop :=
62 ∀ i j, ∀ hij : i ≤ j, S.map hij (x j) = x i
64/-- Compatibility of a family of maps into an inverse system. -/
65def CompatibleMaps {Y : Type w} (ψ : ∀ i, Y → S.X i) : Prop :=
66 ∀ i j, ∀ hij : i ≤ j, S.map hij ∘ ψ j = ψ i
68/-- The inverse limit realized as a subtype of the product. -/
69abbrev inverseLimit : Type _ := {x : ∀ i, S.X i // S.Compatible x}
71/-- The canonical projection from the inverse limit to the \(i\)-th component. -/
72def projection (i : I) : S.inverseLimit → S.X i := fun x => x.1 i
74/--
75Linearity data for an inverse system and its concrete inverse-limit cone. This companion
76predicate packages the scalar-compatibility facts used by Hom-comparison formulations, without
77installing them as global typeclass instances.
78-/
79def IsLinearSystem {R : Type w} [Semiring R] (S : InverseSystem (I := I))
80 [∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
81 [AddCommMonoid S.inverseLimit] [Module R S.inverseLimit] : Prop :=
82 (∀ {i j : I} (hij : i ≤ j) (r : R) (x : S.X j),
83 S.map hij (r • x) = r • S.map hij x) ∧
84 (∀ i (r : R) (x : S.inverseLimit), S.projection i (r • x) = r • S.projection i x)
86namespace IsLinearSystem
88/-- Maps in a linear inverse system commute with scalar multiplication. -/
89theorem map_smul {R : Type w} [Semiring R] {S : InverseSystem (I := I)}
90 [∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
91 [AddCommMonoid S.inverseLimit] [Module R S.inverseLimit]
92 (hS : IsLinearSystem (R := R) S) {i j : I} (hij : i ≤ j) (r : R) (x : S.X j) :
93 S.map hij (r • x) = r • S.map hij x :=
94 hS.1 hij r x
96/-- The finite-stage projection commutes with scalar multiplication by coefficients. -/
97theorem projection_smul {R : Type w} [Semiring R] {S : InverseSystem (I := I)}
98 [∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
99 [AddCommMonoid S.inverseLimit] [Module R S.inverseLimit]
100 (hS : IsLinearSystem (R := R) S) (i : I) (r : R) (x : S.inverseLimit) :
101 S.projection i (r • x) = r • S.projection i x :=
102 hS.2 i r x
104end IsLinearSystem
106/-- Applying a projection to an inverse-limit element returns its corresponding stage coordinate. -/
107@[simp] theorem projection_apply (i : I) (x : S.inverseLimit) :
108 S.projection i x = x.1 i := rfl
110/-- Projections from the inverse limit are compatible with the transition maps. -/
111theorem projection_compatible (x : S.inverseLimit) (i j : I) (hij : i ≤ j) :
112 S.map hij (S.projection j x) = S.projection i x := by
113 exact x.2 i j hij
115/-- The canonical projections form a compatible family of maps. -/
116theorem projection_compatibleMaps : S.CompatibleMaps S.projection := by
117 intro i j hij
118 funext x
119 exact S.projection_compatible x i j hij
121/-- Each canonical projection from an inverse limit is continuous. -/
122theorem continuous_projection (i : I) : Continuous (S.projection i) :=
123 (continuous_apply i).comp continuous_subtype_val
125/-- Two inverse-limit points are equal when all their projections are equal. -/
126@[ext] theorem ext {x y : S.inverseLimit}
127 (h : ∀ i, S.projection i x = S.projection i y) : x = y := by
128 apply Subtype.ext
129 funext i
130 exact h i
132/-- The concrete map induced by a compatible family of maps into the subtype inverse limit. -/
133def inverseLimitLift {Y : Type w} (ψ : ∀ i, Y → S.X i)
134 (hcompat : S.CompatibleMaps ψ) :
135 Y → S.inverseLimit := fun y =>
136 ⟨fun i => ψ i y, by
137 intro i j hij
138 exact congrFun (hcompat i j hij) y⟩
140/-- Composing a canonical projection with the lift recovers the corresponding compatible map. -/
141@[simp] theorem projection_comp_inverseLimitLift {Y : Type w} (ψ : ∀ i, Y → S.X i)
142 (hcompat : S.CompatibleMaps ψ) (i : I) :
143 S.projection i ∘ S.inverseLimitLift ψ hcompat = ψ i := rfl
145/-- Applying a projection to an inverse-limit lift returns the corresponding stage map value. -/
146@[simp] theorem projection_inverseLimitLift_apply {Y : Type w} (ψ : ∀ i, Y → S.X i)
147 (hcompat : S.CompatibleMaps ψ) (i : I) (y : Y) :
148 S.projection i (S.inverseLimitLift ψ hcompat y) = ψ i y := rfl
150/-- A map into the subtype inverse limit is uniquely determined by its projections. -/
151theorem inverseLimitLift_unique {Y : Type w} (ψ : ∀ i, Y → S.X i)
152 (hcompat : S.CompatibleMaps ψ) {f : Y → S.inverseLimit}
153 (hf : ∀ i, S.projection i ∘ f = ψ i) :
154 f = S.inverseLimitLift ψ hcompat := by
155 funext y
156 apply S.ext
157 intro i
158 exact
159 (congrFun (hf i) y).trans
160 (S.projection_inverseLimitLift_apply ψ hcompat i y).symm
162/-- A lift from a topological space is continuous when all of its component maps are continuous. -/
163theorem continuous_inverseLimitLift {Y : Type w} [TopologicalSpace Y] (ψ : ∀ i, Y → S.X i)
164 (hψ : ∀ i, Continuous (ψ i))
165 (hcompat : S.CompatibleMaps ψ) :
166 Continuous (S.inverseLimitLift ψ hcompat) := by
167 exact Continuous.subtype_mk (continuous_pi fun i => hψ i) fun y => by
168 intro i j hij
169 exact congrFun (hcompat i j hij) y
171/-- The universal property of an inverse limit. -/
172structure IsInverseLimit {L : Type w} [TopologicalSpace L] (π : ∀ i, L → S.X i) : Prop where
173 /-- Each leg of the proposed limiting cone is continuous. -/
174 continuous_proj : ∀ i, Continuous (π i)
175 /-- The cone legs commute with every transition map of the inverse system. -/
176 compatible : S.CompatibleMaps π
177 /--
178 Every continuous compatible cone, including one in the designated larger source universe,
179 factors through `L` by a unique continuous map.
180 -/
181 existsUnique_lift :
182 ∀ {Y : Type max u v w} [TopologicalSpace Y] (ψ : ∀ i, Y → S.X i)
183 (_hψ : ∀ i, Continuous (ψ i)) (_hcompat : S.CompatibleMaps ψ),
184 ∃! f : Y → L, Continuous f ∧ ∀ i, π i ∘ f = ψ i
186namespace IsInverseLimit
188variable {S : InverseSystem.{u, v} (I := I)}
189variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
191/-- The large-universe universal property induces the usual universal property for sources in
192the carrier universe. The `ULift` is essential: universe levels cannot themselves be quantified
193inside a structure field. -/
194theorem existsUnique_lift_sameUniverse (hπ : S.IsInverseLimit π)
195 {Y : Type w} [TopologicalSpace Y]
196 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i))
197 (hcompat : S.CompatibleMaps ψ) :
198 ∃! f : Y → L, Continuous f ∧ ∀ i, π i ∘ f = ψ i := by
199 let ψ' : ∀ i, ULift.{max u v} Y → S.X i :=
200 fun i y => ψ i y.down
201 have hψ' : ∀ i, Continuous (ψ' i) :=
202 fun i => (hψ i).comp continuous_uliftDown
203 have hcompat' : S.CompatibleMaps ψ' := by
204 intro i j hij
205 funext y
206 simpa [ψ', Function.comp_apply] using congrFun (hcompat i j hij) y.down
207 obtain ⟨f, hf, huniq⟩ := hπ.existsUnique_lift ψ' hψ' hcompat'
208 refine ⟨f ∘ ULift.up, ?_, ?_⟩
209 · refine ⟨hf.1.comp continuous_uliftUp, ?_⟩
210 intro i
211 funext y
212 simpa [ψ', Function.comp_apply] using congrFun (hf.2 i) (ULift.up y)
213 · intro g hg
214 have hg' : Continuous (g ∘ ULift.down) ∧
215 ∀ i, π i ∘ (g ∘ ULift.down) = ψ' i := by
216 constructor
217 · exact hg.1.comp continuous_uliftDown
218 · intro i
219 funext y
220 simpa [ψ', Function.comp_apply] using congrFun (hg.2 i) y.down
221 have hgf : g ∘ ULift.down = f := huniq (g ∘ ULift.down) hg'
222 funext y
223 simpa [Function.comp_apply] using congrFun hgf (ULift.up y)
225/-- A compatible family of maps to the stages lifts uniquely to a map into the inverse limit. -/
226noncomputable def lift (hπ : S.IsInverseLimit π)
227 {Y : Type w} [TopologicalSpace Y]
228 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
229 Y → L :=
230 Classical.choose (ExistsUnique.exists
231 (hπ.existsUnique_lift_sameUniverse ψ hψ hcompat))
233/-- The universal-property lift is continuous and has the prescribed projections. -/
234theorem lift_spec (hπ : S.IsInverseLimit π)
235 {Y : Type w} [TopologicalSpace Y]
236 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
237 Continuous (hπ.lift ψ hψ hcompat) ∧
238 ∀ i, π i ∘ hπ.lift ψ hψ hcompat = ψ i :=
239 Classical.choose_spec (ExistsUnique.exists
240 (hπ.existsUnique_lift_sameUniverse ψ hψ hcompat))
242/-- The lift into the inverse limit is continuous when all coordinate maps are continuous. -/
243theorem continuous_lift (hπ : S.IsInverseLimit π)
244 {Y : Type w} [TopologicalSpace Y]
245 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
246 Continuous (hπ.lift ψ hψ hcompat) :=
247 (hπ.lift_spec ψ hψ hcompat).1
249/-- The universal-property lift has the prescribed i-th projection. -/
250theorem fac (hπ : S.IsInverseLimit π)
251 {Y : Type w} [TopologicalSpace Y]
252 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
253 (i : I) :
254 π i ∘ hπ.lift ψ hψ hcompat = ψ i :=
255 (hπ.lift_spec ψ hψ hcompat).2 i
257/-- The universal-property lift is the unique continuous map with the prescribed projections. -/
258theorem uniq (hπ : S.IsInverseLimit π)
259 {Y : Type w} [TopologicalSpace Y]
260 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
261 {f : Y → L} (hf : Continuous f) (hfac : ∀ i, π i ∘ f = ψ i) :
262 f = hπ.lift ψ hψ hcompat :=
263 (hπ.existsUnique_lift_sameUniverse ψ hψ hcompat).unique ⟨hf, hfac⟩
264 (hπ.lift_spec ψ hψ hcompat)
266/-- Lifting the projection family of an inverse limit gives the identity map. -/
267theorem lift_self (hπ : S.IsInverseLimit π) :
268 hπ.lift (Y := L) π hπ.continuous_proj hπ.compatible = id := by
269 symm
270 exact hπ.uniq (Y := L) π hπ.continuous_proj hπ.compatible continuous_id fun _ => rfl
272/-- The large-universe universal property also supplies the comparison map from the concrete
273compatible-family model; this is a theorem, not duplicate structure data. -/
274theorem existsUnique_lift_from_inverseLimit (hπ : S.IsInverseLimit π) :
275 ∃! f : S.inverseLimit → L,
276 Continuous f ∧ ∀ i, π i ∘ f = S.projection i := by
277 let ψ' : ∀ i, ULift.{w} S.inverseLimit → S.X i :=
278 fun i x => S.projection i x.down
279 have hψ' : ∀ i, Continuous (ψ' i) :=
280 fun i => (S.continuous_projection i).comp continuous_uliftDown
281 have hcompat' : S.CompatibleMaps ψ' := by
282 intro i j hij
283 funext x
284 simpa [ψ', Function.comp_apply] using
285 congrFun (S.projection_compatibleMaps i j hij) x.down
286 obtain ⟨f, hf, huniq⟩ := hπ.existsUnique_lift ψ' hψ' hcompat'
287 refine ⟨f ∘ ULift.up, ?_, ?_⟩
288 · refine ⟨hf.1.comp continuous_uliftUp, ?_⟩
289 intro i
290 funext x
291 simpa [ψ', Function.comp_apply] using congrFun (hf.2 i) (ULift.up x)
292 · intro g hg
293 have hg' : Continuous (g ∘ ULift.down) ∧
294 ∀ i, π i ∘ (g ∘ ULift.down) = ψ' i := by
295 constructor
296 · exact hg.1.comp continuous_uliftDown
297 · intro i
298 funext x
299 simpa [ψ', Function.comp_apply] using congrFun (hg.2 i) x.down
300 have hgf : g ∘ ULift.down = f := huniq (g ∘ ULift.down) hg'
301 funext x
302 simpa [Function.comp_apply] using congrFun hgf (ULift.up x)
304/-- The lift from the concrete compatible-family inverse limit. -/
305noncomputable def liftFromInverseLimit (hπ : S.IsInverseLimit π) :
306 S.inverseLimit → L :=
307 Classical.choose (ExistsUnique.exists hπ.existsUnique_lift_from_inverseLimit)
309/-- The concrete inverse-limit lift is continuous and has the prescribed projections. -/
310theorem liftFromInverseLimit_spec (hπ : S.IsInverseLimit π) :
311 Continuous hπ.liftFromInverseLimit ∧
312 ∀ i, π i ∘ hπ.liftFromInverseLimit = S.projection i :=
313 Classical.choose_spec (ExistsUnique.exists hπ.existsUnique_lift_from_inverseLimit)
315/-- Every abstract inverse-limit cone is canonically homeomorphic to the concrete compatible-family
316model. Factoring comparison through this model makes the construction independent of the
317carrier's universe. -/
318noncomputable def homeomorphToInverseLimit (hπ : S.IsInverseLimit π) :
319 L ≃ₜ S.inverseLimit where
320 toFun := S.inverseLimitLift π hπ.compatible
321 invFun := hπ.liftFromInverseLimit
322 left_inv := by
323 intro x
324 let f : L → S.inverseLimit := S.inverseLimitLift π hπ.compatible
325 let g : S.inverseLimit → L := hπ.liftFromInverseLimit
326 have hgf : g ∘ f = id := by
327 exact (hπ.existsUnique_lift_sameUniverse π hπ.continuous_proj hπ.compatible).unique
328 (by
329 refine ⟨hπ.liftFromInverseLimit_spec.1.comp
330 (S.continuous_inverseLimitLift π hπ.continuous_proj hπ.compatible), ?_⟩
331 intro i
332 calc
333 π i ∘ (g ∘ f) = (π i ∘ g) ∘ f := by rfl
334 _ = S.projection i ∘ f := by
335 rw [hπ.liftFromInverseLimit_spec.2 i]
336 _ = π i := S.projection_comp_inverseLimitLift π hπ.compatible i)
337 ⟨continuous_id, fun _ => rfl⟩
338 exact congrFun hgf x
339 right_inv := by
340 intro x
341 apply S.ext
342 intro i
343 rw [S.projection_inverseLimitLift_apply]
344 exact congrFun
345 (hπ.liftFromInverseLimit_spec.2 i) x
346 continuous_toFun :=
347 S.continuous_inverseLimitLift π hπ.continuous_proj hπ.compatible
348 continuous_invFun := hπ.liftFromInverseLimit_spec.1
350/-- Inverse limits are unique up to unique homeomorphism. -/
351noncomputable def homeomorph {L' : Type z} [TopologicalSpace L'] {π' : ∀ i, L' → S.X i}
352 (hπ : S.IsInverseLimit π) (hπ' : S.IsInverseLimit π') :
353 L ≃ₜ L' :=
354 hπ.homeomorphToInverseLimit.trans hπ'.homeomorphToInverseLimit.symm
356end IsInverseLimit
358/-- The subtype model carries the inverse-limit universal property. -/
359theorem isInverseLimit_projection : S.IsInverseLimit S.projection := by
360 refine ⟨S.continuous_projection, S.projection_compatibleMaps, ?_⟩
361 intro Y _ ψ hψ hcompat
362 refine ⟨S.inverseLimitLift ψ hcompat, ?_, ?_⟩
363 · exact ⟨S.continuous_inverseLimitLift ψ hψ hcompat,
364 fun i => S.projection_comp_inverseLimitLift ψ hcompat i⟩
365 · intro f hf
366 exact S.inverseLimitLift_unique ψ hcompat hf.2
368/-- The inverse limit is a closed subspace of the product. -/
369theorem isClosed_setOf_compatible [∀ i, T2Space (S.X i)] :
370 IsClosed {x : ∀ i, S.X i | S.Compatible x} := by
371 simp only [Compatible, setOf_forall]
372 refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun hij => ?_
373 exact isClosed_eq ((S.continuous_map hij).comp (continuous_apply j)) (continuous_apply i)
375/--
376The constructed object carries the compact space structure inherited from its profinite
377construction.
378-/
379instance instCompactSpaceInverseLimit [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)] :
380 CompactSpace S.inverseLimit := by
381 let hs : IsClosed {x : ∀ i, S.X i | S.Compatible x} := S.isClosed_setOf_compatible
382 exact hs.isClosedEmbedding_subtypeVal.compactSpace
384/-- Inverse limits of Hausdorff spaces are Hausdorff. -/
385theorem t2Space_inverseLimit [∀ i, T2Space (S.X i)] :
386 T2Space S.inverseLimit := inferInstance
388/-- Inverse limits of totally disconnected spaces are totally disconnected. -/
389theorem totallyDisconnectedSpace_inverseLimit [∀ i, TotallyDisconnectedSpace (S.X i)] :
390 TotallyDisconnectedSpace S.inverseLimit := inferInstance
392/-- A surjective projection from a compact inverse limit to a Hausdorff stage is a quotient map. -/
393theorem isQuotientMap_projection_of_surjective [∀ i, CompactSpace (S.X i)]
394 [∀ i, T2Space (S.X i)] {i : I} (hsurj : Function.Surjective (S.projection i)) :
395 Topology.IsQuotientMap (S.projection i) :=
396 Topology.IsQuotientMap.of_surjective_continuous hsurj (S.continuous_projection i)
398end InverseSystem
400section GroupSystems
402variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
404/-- A group-valued inverse system whose transition maps are group homomorphisms. -/
405class IsGroupSystem (S : InverseSystem (I := I)) [∀ i, Group (S.X i)] : Prop where
406 /-- Transition maps preserve the identity element at every pair of comparable stages. -/
407 map_one : ∀ {i j : I} (hij : i ≤ j), S.map hij 1 = 1
408 /-- Transition maps preserve products at every pair of comparable stages. -/
409 map_mul : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
410 S.map hij (x * y) = S.map hij x * S.map hij y
411 /-- Transition maps preserve inverses at every pair of comparable stages. -/
412 map_inv : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
413 S.map hij x⁻¹ = (S.map hij x)⁻¹
415variable [∀ i, Group (S.X i)] [IsGroupSystem S]
417/-- The unit of the inverse limit is the compatible family of units at all stages. -/
418instance instOneInverseLimit : One S.inverseLimit where
419 one := ⟨fun i => 1, by
420 intro i j hij
421 simpa using IsGroupSystem.map_one (S := S) hij⟩
423/--
424Multiplication on the inverse limit is defined coordinatewise through the stage multiplications.
425-/
426instance instMulInverseLimit : Mul S.inverseLimit where
427 mul x y := ⟨fun i => S.projection i x * S.projection i y, by
428 intro i j hij
429 calc
430 S.map hij (S.projection j x * S.projection j y)
431 = S.map hij (S.projection j x) * S.map hij (S.projection j y) := by
432 simpa using IsGroupSystem.map_mul (S := S) hij (S.projection j x)
433 (S.projection j y)
434 _ = S.projection i x * S.projection i y := by
435 rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩
437/-- The inverse-limit object carries the structure induced coordinatewise from the finite stages. -/
438instance instInvInverseLimit : Inv S.inverseLimit where
439 inv x := ⟨fun i => (S.projection i x)⁻¹, by
440 intro i j hij
441 calc
442 S.map hij ((S.projection j x)⁻¹) = (S.map hij (S.projection j x))⁻¹ := by
443 simpa using IsGroupSystem.map_inv (S := S) hij (S.projection j x)
444 _ = (S.projection i x)⁻¹ := by rw [S.projection_compatible x i j hij]⟩
446/-- The projection of the identity element is the identity at each stage. -/
447@[simp] theorem projection_one (i : I) : S.projection i (1 : S.inverseLimit) = 1 := rfl
449/-- Projection commutes with multiplication in a group-valued inverse system. -/
450@[simp] theorem projection_mul (i : I) (x y : S.inverseLimit) :
451 S.projection i (x * y) = S.projection i x * S.projection i y := rfl
453/-- Projection commutes with inversion in a group-valued inverse system. -/
454@[simp] theorem projection_inv (i : I) (x : S.inverseLimit) :
455 S.projection i x⁻¹ = (S.projection i x)⁻¹ := rfl
457/--
458The constructed carrier inherits its group structure from the coordinatewise group structure of
459the construction.
460-/
461instance instGroupInverseLimit : Group S.inverseLimit where
462 one := 1
463 mul := (· * ·)
464 inv := Inv.inv
465 mul_assoc x y z := by
466 apply S.ext
467 intro i
468 change ((x.1 i * y.1 i) * z.1 i) = (x.1 i * (y.1 i * z.1 i))
469 simp only [mul_assoc]
470 one_mul x := by
471 apply S.ext
472 intro i
473 change 1 * x.1 i = x.1 i
474 simp only [one_mul]
475 mul_one x := by
476 apply S.ext
477 intro i
478 change x.1 i * 1 = x.1 i
479 simp only [mul_one]
480 inv_mul_cancel x := by
481 apply S.ext
482 intro i
483 change (x.1 i)⁻¹ * x.1 i = 1
484 simp only [inv_mul_cancel]
486/-- The object is a topological group with the induced group operations and topology. -/
487instance instIsTopologicalGroupInverseLimit [∀ i, IsTopologicalGroup (S.X i)] :
488 IsTopologicalGroup S.inverseLimit where
489 continuous_mul := by
490 exact Continuous.subtype_mk
491 (continuous_pi fun i =>
492 ((S.continuous_projection i).comp continuous_fst).mul
493 ((S.continuous_projection i).comp continuous_snd))
494 (fun xy => by
495 intro i j hij
496 change S.map hij (S.projection j xy.1 * S.projection j xy.2) =
497 S.projection i xy.1 * S.projection i xy.2
498 rw [IsGroupSystem.map_mul (S := S) hij,
499 S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
500 continuous_inv := by
501 exact Continuous.subtype_mk
502 (continuous_pi fun i => continuous_inv.comp (S.continuous_projection i))
503 (fun x => by
504 intro i j hij
505 change S.map hij ((S.projection j x)⁻¹) = (S.projection i x)⁻¹
506 rw [IsGroupSystem.map_inv (S := S) hij, S.projection_compatible x i j hij])
508/-- The canonical projections from a group-valued inverse limit are homomorphisms. -/
509def projectionHom (i : I) : S.inverseLimit →* S.X i where
510 toFun := S.projection i
511 map_one' := projection_one (S := S) i
512 map_mul' := by
513 intro x y
514 exact projection_mul (S := S) i x y
516/--
517Applying a homomorphic projection to an inverse-limit element returns its corresponding stage
518coordinate.
519-/
520@[simp] theorem projectionHom_apply (i : I) (x : S.inverseLimit) :
521 projectionHom (S := S) i x = S.projection i x := rfl
523end GroupSystems
525section AddGroupSystems
527variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
529/-- An additive-group-valued inverse system whose transition maps are additive homomorphisms. -/
530class IsAddGroupSystem (S : InverseSystem (I := I)) [∀ i, AddCommGroup (S.X i)] : Prop where
531 /-- Transition maps preserve zero at every pair of comparable stages. -/
532 map_zero : ∀ {i j : I} (hij : i ≤ j), S.map hij 0 = 0
533 /-- Transition maps preserve addition at every pair of comparable stages. -/
534 map_add : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
535 S.map hij (x + y) = S.map hij x + S.map hij y
536 /-- Transition maps preserve additive inverses at every pair of comparable stages. -/
537 map_neg : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
538 S.map hij (-x) = -S.map hij x
540variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
542/-- A module-valued inverse system whose transition maps are linear over a fixed semiring. -/
543class IsModuleSystem (R : Type w) [Semiring R] (S : InverseSystem (I := I))
544 [∀ i, AddCommGroup (S.X i)] [∀ i, Module R (S.X i)] : Prop where
545 /-- Transition maps commute with the fixed `R`-scalar action on all stages. -/
546 map_smul : ∀ {i j : I} (hij : i ≤ j) (r : R) (x : S.X j),
547 S.map hij (r • x) = r • S.map hij x
549/--
550The zero element of the inverse limit is the compatible family of zero elements at all stages.
551-/
552instance instZeroAddInverseLimit : Zero S.inverseLimit where
553 zero := ⟨fun i => 0, by
554 intro i j hij
555 simpa using IsAddGroupSystem.map_zero (S := S) hij⟩
557/-- Addition in the additive inverse limit is defined coordinatewise. -/
558instance instAddAddInverseLimit : Add S.inverseLimit where
559 add x y := ⟨fun i => S.projection i x + S.projection i y, by
560 intro i j hij
561 calc
562 S.map hij (S.projection j x + S.projection j y)
563 = S.map hij (S.projection j x) + S.map hij (S.projection j y) := by
564 simpa using IsAddGroupSystem.map_add (S := S) hij (S.projection j x)
565 (S.projection j y)
566 _ = S.projection i x + S.projection i y := by
567 rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩
569/-- Negation on an additive inverse limit is defined coordinatewise through the stage negations. -/
570instance instNegAddInverseLimit : Neg S.inverseLimit where
571 neg x := ⟨fun i => -S.projection i x, by
572 intro i j hij
573 calc
574 S.map hij (-S.projection j x) = -S.map hij (S.projection j x) := by
575 simpa using IsAddGroupSystem.map_neg (S := S) hij (S.projection j x)
576 _ = -S.projection i x := by rw [S.projection_compatible x i j hij]⟩
578/-- Subtraction in the inverse limit is defined coordinatewise through the stage subtractions. -/
579instance instSubAddInverseLimit : Sub S.inverseLimit where
580 sub x y := ⟨fun i => S.projection i x - S.projection i y, by
581 intro i j hij
582 change S.map hij (S.projection j x - S.projection j y) =
583 S.projection i x - S.projection i y
584 rw [sub_eq_add_neg, IsAddGroupSystem.map_add, IsAddGroupSystem.map_neg,
585 S.projection_compatible x i j hij, S.projection_compatible y i j hij, sub_eq_add_neg]⟩
587/-- An additive inverse limit carries natural-number scalar multiplication coordinatewise. -/
588instance instSMulNatAddInverseLimit : SMul ℕ S.inverseLimit where
589 smul n x := ⟨fun i => n • S.projection i x, by
590 intro i j hij
591 change S.map hij (n • S.projection j x) = n • S.projection i x
592 induction n with
593 | zero =>
594 simp only [InverseSystem.projection_apply, zero_nsmul, IsAddGroupSystem.map_zero]
595 | succ n ihn =>
596 rw [succ_nsmul, succ_nsmul]
597 calc
598 S.map hij (n • S.projection j x + S.projection j x)
599 = S.map hij (n • S.projection j x) + S.map hij (S.projection j x) := by
600 exact IsAddGroupSystem.map_add (S := S) hij (n • S.projection j x)
601 (S.projection j x)
602 _ = n • S.projection i x + S.projection i x := by
603 rw [ihn, S.projection_compatible x i j hij]⟩
605/-- An additive inverse limit carries integer scalar multiplication coordinatewise. -/
606instance instSMulIntAddInverseLimit : SMul ℤ S.inverseLimit where
607 smul n x := ⟨fun i => n • S.projection i x, by
608 intro i j hij
609 change S.map hij (n • S.projection j x) = n • S.projection i x
610 let f : S.X j →+ S.X i :=
611 { toFun := S.map hij
612 map_zero' := IsAddGroupSystem.map_zero (S := S) hij
613 map_add' := IsAddGroupSystem.map_add (S := S) hij }
614 calc
615 S.map hij (n • S.projection j x) = f (n • S.projection j x) := rfl
616 _ = n • f (S.projection j x) := f.map_zsmul n (S.projection j x)
617 _ = n • S.projection i x := by
618 change n • S.map hij (S.projection j x) = n • S.projection i x
619 rw [S.projection_compatible x i j hij]⟩
621/-- The projection of zero is zero at each stage. -/
622@[simp] theorem projection_zero (i : I) : S.projection i (0 : S.inverseLimit) = 0 := rfl
624/-- Projection commutes with addition in an additive inverse system. -/
625@[simp] theorem projection_add (i : I) (x y : S.inverseLimit) :
626 S.projection i (x + y) = S.projection i x + S.projection i y := rfl
628/-- Projection commutes with negation in an additive inverse system. -/
629@[simp] theorem projection_neg (i : I) (x : S.inverseLimit) :
630 S.projection i (-x) = -S.projection i x := rfl
632/-- Projection commutes with subtraction in an additive inverse system. -/
633@[simp] theorem projection_sub (i : I) (x y : S.inverseLimit) :
634 S.projection i (x - y) = S.projection i x - S.projection i y := rfl
636/--
637The additive-group structure on an additive inverse limit; kept named rather than global to
638avoid a parent-instance diamond with ring inverse limits.
639-/
640@[reducible] def instAddCommGroupAddInverseLimit : AddCommGroup S.inverseLimit := by
641 let f : S.inverseLimit → ∀ i, S.X i := Subtype.val
642 apply Subtype.val_injective.addCommGroup f rfl (fun _ _ => rfl) (fun _ => rfl)
643 (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
645attribute [local instance] instAddCommGroupAddInverseLimit
647section ModuleSystems
649variable {R : Type w} [Semiring R]
650variable [∀ i, Module R (S.X i)] [IsModuleSystem (I := I) R S]
652/--
653An inverse-limit module carries scalar multiplication by applying the scalar action at every
654stage.
655-/
656instance instSMulInverseLimitOfIsModuleSystem : SMul R S.inverseLimit where
657 smul r x := ⟨fun i => r • S.projection i x, by
658 intro i j hij
659 change S.map hij (r • S.projection j x) = r • S.projection i x
660 rw [IsModuleSystem.map_smul (S := S) hij, S.projection_compatible x i j hij]⟩
662omit [IsAddGroupSystem S] in
663/-- Projection commutes with scalar multiplication in a module-valued inverse system. -/
664@[simp] theorem projection_smul_of_isModuleSystem (i : I) (r : R) (x : S.inverseLimit) :
665 S.projection i (r • x) = r • S.projection i x :=
666 rfl
668/-- The inverse limit is a module when all stages form a compatible module system. -/
669instance instModuleInverseLimitOfIsModuleSystem : Module R S.inverseLimit := by
670 let f : S.inverseLimit →+ ∀ i, S.X i :=
671 { toFun := Subtype.val
672 map_zero' := rfl
673 map_add' := fun _ _ => rfl }
674 exact Function.Injective.module R f Subtype.val_injective (fun _ _ => rfl)
676/-- Scalar multiplication is continuous for the relevant inverse-limit topology. -/
677instance instContinuousSMulInverseLimitOfIsModuleSystem
678 [TopologicalSpace R] [∀ i, ContinuousSMul R (S.X i)] :
679 ContinuousSMul R S.inverseLimit where
680 continuous_smul := by
681 exact Continuous.subtype_mk
682 (continuous_pi fun i =>
683 continuous_fst.smul ((S.continuous_projection i).comp continuous_snd))
684 (fun p => by
685 intro i j hij
686 change S.map hij (p.1 • S.projection j p.2) = p.1 • S.projection i p.2
687 rw [IsModuleSystem.map_smul (S := S) hij, S.projection_compatible p.2 i j hij])
689end ModuleSystems
691/-- The additive inverse-limit object has addition defined coordinatewise on compatible families. -/
692instance instIsTopologicalAddGroupAddInverseLimit [∀ i, IsTopologicalAddGroup (S.X i)] :
693 IsTopologicalAddGroup S.inverseLimit where
694 continuous_add := by
695 exact Continuous.subtype_mk
696 (continuous_pi fun i =>
697 ((S.continuous_projection i).comp continuous_fst).add
698 ((S.continuous_projection i).comp continuous_snd))
699 (fun xy => by
700 intro i j hij
701 change S.map hij (S.projection j xy.1 + S.projection j xy.2) =
702 S.projection i xy.1 + S.projection i xy.2
703 rw [IsAddGroupSystem.map_add (S := S) hij,
704 S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
705 continuous_neg := by
706 exact Continuous.subtype_mk
707 (continuous_pi fun i => continuous_neg.comp (S.continuous_projection i))
708 (fun x => by
709 intro i j hij
710 change S.map hij (-S.projection j x) = -S.projection i x
711 rw [IsAddGroupSystem.map_neg (S := S) hij, S.projection_compatible x i j hij])
713/-- The canonical projections from an additive inverse limit are additive homomorphisms. -/
714def projectionAddHom (i : I) : S.inverseLimit →+ S.X i where
715 toFun := S.projection i
716 map_zero' := projection_zero (S := S) i
717 map_add' := by
718 intro x y
719 exact projection_add (S := S) i x y
721/--
722Applying an additive projection to an inverse-limit element returns its corresponding stage
723coordinate.
724-/
725@[simp] theorem projectionAddHom_apply (i : I) (x : S.inverseLimit) :
726 projectionAddHom (S := S) i x = S.projection i x := rfl
728end AddGroupSystems
730section RingSystems
732variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
734/-- A ring-valued inverse system whose transition maps are ring homomorphisms. -/
735class IsRingSystem (S : InverseSystem (I := I)) [∀ i, Ring (S.X i)] : Prop where
736 /-- Transition maps preserve the additive identity. -/
737 map_zero : ∀ {i j : I} (hij : i ≤ j), S.map hij 0 = 0
738 /-- Transition maps preserve the multiplicative identity. -/
739 map_one : ∀ {i j : I} (hij : i ≤ j), S.map hij 1 = 1
740 /-- Transition maps preserve addition. -/
741 map_add : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
742 S.map hij (x + y) = S.map hij x + S.map hij y
743 /-- Transition maps preserve multiplication. -/
744 map_mul : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
745 S.map hij (x * y) = S.map hij x * S.map hij y
747variable [∀ i, Ring (S.X i)] [IsRingSystem S]
749/-- A transition map in a ring-valued inverse system is bundled as a ring homomorphism. -/
750def mapRingHom {i j : I} (hij : i ≤ j) : S.X j →+* S.X i where
751 toFun := S.map hij
752 map_zero' := IsRingSystem.map_zero (S := S) hij
753 map_one' := IsRingSystem.map_one (S := S) hij
754 map_add' := IsRingSystem.map_add (S := S) hij
755 map_mul' := IsRingSystem.map_mul (S := S) hij
757/--
758The bundled ring homomorphism has the same underlying function as the coordinatewise
759construction.
760-/
761@[simp]
762theorem mapRingHom_apply {i j : I} (hij : i ≤ j) (x : S.X j) :
763 mapRingHom (S := S) hij x = S.map hij x := rfl
765/-- The additive system underlying a ring system. This remains explicit so that importing ring
766systems does not install a second global path to the additive inverse-limit instances. -/
767theorem isAddGroupSystemOfIsRingSystem : IsAddGroupSystem S where
768 map_zero := IsRingSystem.map_zero (S := S)
769 map_add := IsRingSystem.map_add (S := S)
770 map_neg := by
771 intro i j hij x
772 exact (mapRingHom (S := S) hij).map_neg x
774local instance : IsAddGroupSystem S := isAddGroupSystemOfIsRingSystem S
776attribute [local instance] instAddCommGroupAddInverseLimit
778/--
779Ring multiplication on the inverse limit is defined coordinatewise through the stage ring
780multiplications.
781-/
782instance instMulRingInverseLimit : Mul S.inverseLimit where
783 mul x y := ⟨fun i => S.projection i x * S.projection i y, by
784 intro i j hij
785 calc
786 S.map hij (S.projection j x * S.projection j y)
787 = S.map hij (S.projection j x) * S.map hij (S.projection j y) := by
788 exact IsRingSystem.map_mul (S := S) hij (S.projection j x)
789 (S.projection j y)
790 _ = S.projection i x * S.projection i y := by
791 rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩
793/-- The unit of the ring inverse limit is the compatible family of units at all stages. -/
794instance instOneRingInverseLimit : One S.inverseLimit where
795 one := ⟨fun i => 1, by
796 intro i j hij
797 exact IsRingSystem.map_one (S := S) hij⟩
799/-- Powers in the inverse-limit ring are computed at every stage coordinate. -/
800instance instPowNatRingInverseLimit : Pow S.inverseLimit ℕ where
801 pow x n := ⟨fun i => S.projection i x ^ n, by
802 intro i j hij
803 change S.map hij (S.projection j x ^ n) = S.projection i x ^ n
804 rw [← mapRingHom_apply (S := S) hij, map_pow, mapRingHom_apply,
805 S.projection_compatible x i j hij]⟩
807/--
808Natural number casts in a ring inverse limit are computed coordinatewise from finite-stage
809natural number casts.
810-/
811instance instNatCastRingInverseLimit : NatCast S.inverseLimit where
812 natCast n := ⟨fun _ => n, by
813 intro i j hij
814 change S.map hij (Nat.cast n) = Nat.cast n
815 exact map_natCast (mapRingHom (S := S) hij) n⟩
817/--
818Integer casts in a ring inverse limit are computed coordinatewise from finite-stage integer
819casts.
820-/
821instance instIntCastRingInverseLimit : IntCast S.inverseLimit where
822 intCast n := ⟨fun _ => n, by
823 intro i j hij
824 change S.map hij (Int.cast n) = Int.cast n
825 exact map_intCast (mapRingHom (S := S) hij) n⟩
827/-- The inverse-limit projection preserves \(1\). -/
828@[simp]
829theorem projection_ring_one (i : I) : S.projection i (1 : S.inverseLimit) = 1 := rfl
831/-- The inverse-limit projection preserves multiplication. -/
832@[simp]
833theorem projection_ring_mul (i : I) (x y : S.inverseLimit) :
834 S.projection i (x * y) = S.projection i x * S.projection i y := rfl
836/-- The inverse-limit projection preserves powers. -/
837@[simp]
838theorem projection_ring_pow (i : I) (x : S.inverseLimit) (n : ℕ) :
839 S.projection i (x ^ n) = S.projection i x ^ n := rfl
841/-- The inverse-limit projection preserves natural number casts. -/
842@[simp]
843theorem projection_ring_natCast (i : I) (n : ℕ) :
844 S.projection i (Nat.cast n : S.inverseLimit) = Nat.cast n := rfl
846/-- The inverse-limit projection preserves integer casts. -/
847@[simp]
848theorem projection_ring_intCast (i : I) (n : ℤ) :
849 S.projection i (Int.cast n : S.inverseLimit) = Int.cast n := rfl
851/--
852A ring inverse limit is a ring because all operations and axioms are inherited coordinatewise
853from the stage rings.
854-/
855instance instRingInverseLimit : Ring S.inverseLimit :=
856 Function.Injective.ring
857 (fun x : S.inverseLimit => (x : ∀ i, S.X i))
858 Subtype.val_injective
859 (by funext i; rfl)
860 (by funext i; rfl)
861 (by intro x y; funext i; rfl)
862 (by intro x y; funext i; rfl)
863 (by intro x; funext i; rfl)
864 (by intro x y; funext i; rfl)
865 (by intro n x; funext i; rfl)
866 (by intro n x; funext i; rfl)
867 (by intro x n; funext i; rfl)
868 (by intro n; funext i; rfl)
869 (by intro n; funext i; rfl)
871/-- Multiplication in a ring inverse limit is continuous for the inverse-limit topology. -/
872instance instContinuousMulRingInverseLimit [∀ i, ContinuousMul (S.X i)] :
873 ContinuousMul S.inverseLimit where
874 continuous_mul := by
875 exact Continuous.subtype_mk
876 (continuous_pi fun i =>
877 ((S.continuous_projection i).comp continuous_fst).mul
878 ((S.continuous_projection i).comp continuous_snd))
879 (fun xy => by
880 intro i j hij
881 change S.map hij (S.projection j xy.1 * S.projection j xy.2) =
882 S.projection i xy.1 * S.projection i xy.2
883 rw [IsRingSystem.map_mul (S := S) hij,
884 S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
886/--
887A ring inverse limit inherits a topological-ring structure from the compatible stage topological
888rings.
889-/
890instance instIsTopologicalRingRingInverseLimit [∀ i, IsTopologicalRing (S.X i)] :
891 IsTopologicalRing S.inverseLimit := by
892 letI : IsTopologicalAddGroup S.inverseLimit :=
893 instIsTopologicalAddGroupAddInverseLimit S
894 letI : ContinuousMul S.inverseLimit := instContinuousMulRingInverseLimit S
895 letI : IsTopologicalSemiring S.inverseLimit := IsTopologicalSemiring.mk
896 exact IsTopologicalRing.mk
898/-- The canonical projection from a ring-valued inverse limit is bundled as a ring homomorphism. -/
899def projectionRingHom (i : I) : S.inverseLimit →+* S.X i where
900 toFun := S.projection i
901 map_zero' := projection_zero (S := S) i
902 map_one' := projection_ring_one (S := S) i
903 map_add' := by
904 intro x y
905 exact projection_add (S := S) i x y
906 map_mul' := by
907 intro x y
908 exact projection_ring_mul (S := S) i x y
910/--
911The ring-homomorphism projection has the same underlying coordinate map as the finite-stage
912projection.
913-/
914@[simp]
915theorem projectionRingHom_apply (i : I) (x : S.inverseLimit) :
916 projectionRingHom (S := S) i x = S.projection i x := rfl
918/--
919Composing the ring-valued transition from \(j\) to \(i\) with the projection at \(j\) gives the
920projection at \(i\).
921-/
922theorem mapRingHom_comp_projectionRingHom {i j : I} (hij : i ≤ j) :
923 (mapRingHom (S := S) hij).comp (projectionRingHom (S := S) j) =
924 projectionRingHom (S := S) i := by
925 apply RingHom.ext
926 intro x
927 exact S.projection_compatible x i j hij
929end RingSystems
931end
932end InverseSystems
933end ProCGroups