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

ProCGroups/InverseSystems/Basic.lean

1import Mathlib.Topology.Algebra.Ring.Basic
2import Mathlib.Algebra.Module.Pi
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/InverseSystems/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Concrete inverse systems
15This file defines a concrete, calculation-oriented inverse-system wrapper for
16topological spaces and its subtype inverse limit. Categorical diagram bridges
17live in `ProCGroups.InverseSystems.CategoryBridge`.
18-/
20open Set
21open scoped Topology
23namespace ProCGroups
24namespace InverseSystems
26universe u v w
28section
30variable {I : Type u} [Preorder I]
32/-- An inverse system of topological spaces indexed by a preorder. -/
33structure InverseSystem where
34 X : I → Type v
35 topologicalSpace : ∀ i, TopologicalSpace (X i)
36 map : ∀ {i j : I}, i ≤ j → X j → X i
37 continuous_map : ∀ {i j : I} (hij : i ≤ j), Continuous (map hij)
38 map_id : ∀ i, map (le_rfl : i ≤ i) = id
39 map_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
40 map hij ∘ map hjk = map (hij.trans hjk)
42attribute [instance] InverseSystem.topologicalSpace
44namespace InverseSystem
46variable (S : InverseSystem (I := I))
48/-- The transition map along `i ≤ i` is the identity on points. -/
49@[simp] theorem map_id_apply (i : I) (x : S.X i) :
50 S.map (le_rfl : i ≤ i) x = x := by
51 simpa using congrFun (S.map_id i) x
53/-- Transition maps compose pointwise along comparable indices. -/
54@[simp] theorem map_comp_apply {i j k : I} (hij : i ≤ j) (hjk : j ≤ k) (x : S.X k) :
55 S.map hij (S.map hjk x) = S.map (hij.trans hjk) x := by
56 simpa [Function.comp] using congrFun (S.map_comp hij hjk) x
58/-- Compatibility of a family of points in the product. -/
59def Compatible (x : ∀ i, S.X i) : Prop :=
60 ∀ i j, ∀ hij : i ≤ j, S.map hij (x j) = x i
62/-- Compatibility of a family of maps into an inverse system. -/
63def CompatibleMaps {Y : Type w} (ψ : ∀ i, Y → S.X i) : Prop :=
64 ∀ i j, ∀ hij : i ≤ j, S.map hij ∘ ψ j = ψ i
66/-- The inverse limit realized as a subtype of the product. -/
67abbrev inverseLimit : Type _ := {x : ∀ i, S.X i // S.Compatible x}
69/-- The canonical projection from the inverse limit to the `i`-th component. -/
70def projection (i : I) : S.inverseLimit → S.X i := fun x => x.1 i
72/-- Linearity data for an inverse system and its concrete inverse-limit cone.
74This companion predicate packages the scalar-compatibility facts used by Hom-comparison APIs,
75without installing them as global typeclass instances. -/
76def IsLinearSystem {R : Type w} [Semiring R] (S : InverseSystem (I := I))
77 [∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
78 [AddCommMonoid S.inverseLimit] [Module R S.inverseLimit] : Prop :=
79 (∀ {i j : I} (hij : i ≤ j) (r : R) (x : S.X j),
80 S.map hij (r • x) = r • S.map hij x) ∧
81 (∀ i (r : R) (x : S.inverseLimit), S.projection i (r • x) = r • S.projection i x)
85theorem map_smul {R : Type w} [Semiring R] {S : InverseSystem (I := I)}
86 [∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
87 [AddCommMonoid S.inverseLimit] [Module R S.inverseLimit]
88 (hS : IsLinearSystem (R := R) S) {i j : I} (hij : i ≤ j) (r : R) (x : S.X j) :
89 S.map hij (r • x) = r • S.map hij x :=
90 hS.1 hij r x
92theorem projection_smul {R : Type w} [Semiring R] {S : InverseSystem (I := I)}
93 [∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
94 [AddCommMonoid S.inverseLimit] [Module R S.inverseLimit]
95 (hS : IsLinearSystem (R := R) S) (i : I) (r : R) (x : S.inverseLimit) :
96 S.projection i (r • x) = r • S.projection i x :=
97 hS.2 i r x
101/-- Evaluating the canonical projection is evaluation of the underlying compatible family. -/
102@[simp] theorem projection_apply (i : I) (x : S.inverseLimit) :
103 S.projection i x = x.1 i := rfl
105/-- Projections from the inverse limit are compatible with the transition maps. -/
106theorem projection_compatible (x : S.inverseLimit) (i j : I) (hij : i ≤ j) :
107 S.map hij (S.projection j x) = S.projection i x := by
108 exact x.2 i j hij
110/-- The canonical projections form a compatible family of maps. -/
111theorem projection_compatibleMaps : S.CompatibleMaps S.projection := by
112 intro i j hij
113 funext x
114 exact S.projection_compatible x i j hij
116/-- Each canonical projection from an inverse limit is continuous. -/
117theorem continuous_projection (i : I) : Continuous (S.projection i) :=
118 (continuous_apply i).comp continuous_subtype_val
120/-- Two inverse-limit points are equal when all their projections are equal. -/
121@[ext] theorem ext {x y : S.inverseLimit}
122 (h : ∀ i, S.projection i x = S.projection i y) : x = y := by
123 apply Subtype.ext
124 funext i
125 exact h i
127/-- The concrete map induced by a compatible family of maps into the subtype inverse limit. -/
128def inverseLimitLift {Y : Type w} (ψ : ∀ i, Y → S.X i)
129 (hcompat : S.CompatibleMaps ψ) :
130 Y → S.inverseLimit := fun y =>
131 ⟨fun i => ψ i y, by
132 intro i j hij
133 exact congrFun (hcompat i j hij) y⟩
135/-- A canonical projection composed with the lift recovers the corresponding compatible map. -/
136@[simp] theorem projection_comp_inverseLimitLift {Y : Type w} (ψ : ∀ i, Y → S.X i)
137 (hcompat : S.CompatibleMaps ψ) (i : I) :
138 S.projection i ∘ S.inverseLimitLift ψ hcompat = ψ i := rfl
140/-- Applying a canonical projection to the lift of a compatible family. -/
141@[simp] theorem projection_inverseLimitLift_apply {Y : Type w} (ψ : ∀ i, Y → S.X i)
142 (hcompat : S.CompatibleMaps ψ) (i : I) (y : Y) :
143 S.projection i (S.inverseLimitLift ψ hcompat y) = ψ i y := rfl
145/-- A map into the subtype inverse limit is uniquely determined by its projections. -/
146theorem inverseLimitLift_unique {Y : Type w} (ψ : ∀ i, Y → S.X i)
147 (hcompat : S.CompatibleMaps ψ) {f : Y → S.inverseLimit}
148 (hf : ∀ i, S.projection i ∘ f = ψ i) :
149 f = S.inverseLimitLift ψ hcompat := by
150 funext y
151 apply S.ext
152 intro i
153 simpa [Function.comp] using congrFun (hf i) y
155/-- A lift from a topological space is continuous when all of its component maps are continuous. -/
156theorem continuous_inverseLimitLift {Y : Type w} [TopologicalSpace Y] (ψ : ∀ i, Y → S.X i)
157 (hψ : ∀ i, Continuous (ψ i))
158 (hcompat : S.CompatibleMaps ψ) :
159 Continuous (S.inverseLimitLift ψ hcompat) := by
160 exact Continuous.subtype_mk (continuous_pi fun i => hψ i) fun y => by
161 intro i j hij
162 exact congrFun (hcompat i j hij) y
164/-- The universal property of an inverse limit. -/
165structure IsInverseLimit {L : Type w} [TopologicalSpace L] (π : ∀ i, L → S.X i) : Prop where
166 continuous_proj : ∀ i, Continuous (π i)
167 compatible : S.CompatibleMaps π
169 ∀ {Y : Type w} [TopologicalSpace Y] (ψ : ∀ i, Y → S.X i)
170 (_hψ : ∀ i, Continuous (ψ i)) (_hcompat : S.CompatibleMaps ψ),
171 ∃! f : Y → L, Continuous f ∧ ∀ i, π i ∘ f = ψ i
175variable {S}
176variable {L : Type w} [TopologicalSpace L] {π : ∀ i, L → S.X i}
178/-- The map supplied by the inverse-limit universal property. -/
179noncomputable def lift (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
180 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
181 Y → L :=
182 Classical.choose (ExistsUnique.exists (hπ.existsUnique_lift ψ hψ hcompat))
184/-- The universal-property lift is continuous and has the prescribed projections. -/
185theorem lift_spec (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
186 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
187 Continuous (hπ.lift ψ hψ hcompat) ∧
188 ∀ i, π i ∘ hπ.lift ψ hψ hcompat = ψ i :=
189 Classical.choose_spec (ExistsUnique.exists (hπ.existsUnique_lift ψ hψ hcompat))
191/-- The universal-property lift is continuous. -/
192theorem continuous_lift (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
193 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
194 Continuous (hπ.lift ψ hψ hcompat) :=
195 (hπ.lift_spec ψ hψ hcompat).1
197/-- The universal-property lift has the prescribed `i`-th projection. -/
198theorem fac (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
199 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
200 (i : I) :
201 π i ∘ hπ.lift ψ hψ hcompat = ψ i :=
202 (hπ.lift_spec ψ hψ hcompat).2 i
204/-- The universal-property lift is the unique continuous map with the prescribed projections. -/
205theorem uniq (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
206 (ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
207 {f : Y → L} (hf : Continuous f) (hfac : ∀ i, π i ∘ f = ψ i) :
208 f = hπ.lift ψ hψ hcompat := by
209 rcases hπ.existsUnique_lift ψ hψ hcompat with ⟨g, hg, huniq⟩
210 have hchosen : hπ.lift ψ hψ hcompat = g := huniq _ (hπ.lift_spec ψ hψ hcompat)
211 exact (huniq _ ⟨hf, hfac⟩).trans hchosen.symm
213/-- Lifting the projection family of an inverse limit gives the identity map. -/
214theorem lift_self (hπ : S.IsInverseLimit π) :
215 hπ.lift (Y := L) π hπ.continuous_proj hπ.compatible = id := by
216 symm
217 exact hπ.uniq (Y := L) π hπ.continuous_proj hπ.compatible continuous_id fun _ => rfl
219/-- Inverse limits are unique up to unique homeomorphism. -/
220noncomputable def homeomorph {L' : Type w} [TopologicalSpace L'] {π' : ∀ i, L' → S.X i}
221 (hπ : S.IsInverseLimit π) (hπ' : S.IsInverseLimit π') :
222 L ≃ₜ L' where
223 toFun := hπ'.lift (Y := L) π hπ.continuous_proj hπ.compatible
224 invFun := hπ.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible
225 left_inv := by
226 intro x
227 let f : L → L' := hπ'.lift (Y := L) π hπ.continuous_proj hπ.compatible
228 let g : L' → L := hπ.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible
229 have hgf : g ∘ f = hπ.lift (Y := L) π hπ.continuous_proj hπ.compatible := by
230 exact hπ.uniq (Y := L) π hπ.continuous_proj hπ.compatible
231 ((hπ.continuous_lift (Y := L') π' hπ'.continuous_proj hπ'.compatible).comp
232 (hπ'.continuous_lift (Y := L) π hπ.continuous_proj hπ.compatible))
233 (by
234 intro i
235 calc
236 π i ∘ (g ∘ f) = (π i ∘ g) ∘ f := by rfl
237 _ = π' i ∘ f := by
238 rw [hπ.fac (Y := L') π' hπ'.continuous_proj hπ'.compatible i]
239 _ = π i := by
240 simpa [Function.comp] using
241 hπ'.fac (Y := L) π hπ.continuous_proj hπ.compatible i)
242 calc
243 g (f x) = hπ.lift (Y := L) π hπ.continuous_proj hπ.compatible x := congrFun hgf x
244 _ = x := by
245 simpa using congrFun hπ.lift_self x
246 right_inv := by
247 intro x
248 let f : L → L' := hπ'.lift (Y := L) π hπ.continuous_proj hπ.compatible
249 let g : L' → L := hπ.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible
250 have hfg : f ∘ g = hπ'.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible := by
251 exact hπ'.uniq (Y := L') π' hπ'.continuous_proj hπ'.compatible
252 ((hπ'.continuous_lift (Y := L) π hπ.continuous_proj hπ.compatible).comp
253 (hπ.continuous_lift (Y := L') π' hπ'.continuous_proj hπ'.compatible))
254 (by
255 intro i
256 calc
257 π' i ∘ (f ∘ g) = (π' i ∘ f) ∘ g := by rfl
258 _ = π i ∘ g := by
259 rw [hπ'.fac (Y := L) π hπ.continuous_proj hπ.compatible i]
260 _ = π' i := by
261 simpa [Function.comp] using
262 hπ.fac (Y := L') π' hπ'.continuous_proj hπ'.compatible i)
263 calc
264 f (g x) = hπ'.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible x := congrFun hfg x
265 _ = x := by
266 simpa using congrFun hπ'.lift_self x
267 continuous_toFun := hπ'.continuous_lift (Y := L) π hπ.continuous_proj hπ.compatible
268 continuous_invFun := hπ.continuous_lift (Y := L') π' hπ'.continuous_proj hπ'.compatible
272/-- The subtype model carries the inverse-limit universal property. -/
273theorem isInverseLimit_projection : S.IsInverseLimit S.projection := by
274 refine ⟨S.continuous_projection, S.projection_compatibleMaps, ?_⟩
275 intro Y _ ψ hψ hcompat
276 refine ⟨S.inverseLimitLift ψ hcompat, ?_, ?_⟩
277 · exact ⟨S.continuous_inverseLimitLift ψ hψ hcompat,
278 fun i => S.projection_comp_inverseLimitLift ψ hcompat i⟩
279 · intro f hf
280 exact S.inverseLimitLift_unique ψ hcompat hf.2
282/-- The inverse limit is a closed subspace of the product. -/
283theorem isClosed_setOf_compatible [∀ i, T2Space (S.X i)] :
284 IsClosed {x : ∀ i, S.X i | S.Compatible x} := by
285 simp only [Compatible, setOf_forall]
286 refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun hij => ?_
287 exact isClosed_eq ((S.continuous_map hij).comp (continuous_apply j)) (continuous_apply i)
289/-- The inverse limit of compact Hausdorff stages is compact. -/
290instance instCompactSpaceInverseLimit [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)] :
291 CompactSpace S.inverseLimit := by
292 let hs : IsClosed {x : ∀ i, S.X i | S.Compatible x} := S.isClosed_setOf_compatible
293 simpa [InverseSystem.inverseLimit] using hs.isClosedEmbedding_subtypeVal.compactSpace
295/-- Inverse limits of Hausdorff spaces are Hausdorff. -/
296theorem t2Space_inverseLimit [∀ i, T2Space (S.X i)] :
297 T2Space S.inverseLimit := inferInstance
299/-- Inverse limits of totally disconnected spaces are totally disconnected. -/
300theorem totallyDisconnectedSpace_inverseLimit [∀ i, TotallyDisconnectedSpace (S.X i)] :
301 TotallyDisconnectedSpace S.inverseLimit := inferInstance
303/-- A surjective projection from a compact inverse limit to a Hausdorff stage is a quotient map. -/
304theorem isQuotientMap_projection_of_surjective [∀ i, CompactSpace (S.X i)]
305 [∀ i, T2Space (S.X i)] {i : I} (hsurj : Function.Surjective (S.projection i)) :
306 Topology.IsQuotientMap (S.projection i) :=
307 IsQuotientMap.of_surjective_continuous hsurj (S.continuous_projection i)
311section GroupSystems
313variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
315/-- A group-valued inverse system whose transition maps are group homomorphisms. -/
316class IsGroupSystem (S : InverseSystem (I := I)) [∀ i, Group (S.X i)] : Prop where
317 map_one : ∀ {i j : I} (hij : i ≤ j), S.map hij 1 = 1
318 map_mul : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
319 S.map hij (x * y) = S.map hij x * S.map hij y
320 map_inv : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
321 S.map hij x⁻¹ = (S.map hij x)⁻¹
323variable [∀ i, Group (S.X i)] [IsGroupSystem S]
325/-- The identity element of a group-valued inverse limit is defined coordinatewise. -/
326instance instOneInverseLimit : One S.inverseLimit where
327 one := ⟨fun i => 1, by
328 intro i j hij
329 simpa using IsGroupSystem.map_one (S := S) hij⟩
331/-- Multiplication in a group-valued inverse limit is defined coordinatewise. -/
332instance instMulInverseLimit : Mul S.inverseLimit where
333 mul x y := ⟨fun i => S.projection i x * S.projection i y, by
334 intro i j hij
335 calc
336 S.map hij (S.projection j x * S.projection j y)
337 = S.map hij (S.projection j x) * S.map hij (S.projection j y) := by
338 simpa using IsGroupSystem.map_mul (S := S) hij (S.projection j x)
339 (S.projection j y)
340 _ = S.projection i x * S.projection i y := by
341 rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩
343/-- Inversion in a group-valued inverse limit is defined coordinatewise. -/
344instance instInvInverseLimit : Inv S.inverseLimit where
345 inv x := ⟨fun i => (S.projection i x)⁻¹, by
346 intro i j hij
347 calc
348 S.map hij ((S.projection j x)⁻¹) = (S.map hij (S.projection j x))⁻¹ := by
349 simpa using IsGroupSystem.map_inv (S := S) hij (S.projection j x)
350 _ = (S.projection i x)⁻¹ := by rw [S.projection_compatible x i j hij]⟩
352/-- The projection of the identity element is the identity at each stage. -/
353@[simp] theorem projection_one (i : I) : S.projection i (1 : S.inverseLimit) = 1 := rfl
355/-- Projection commutes with multiplication in a group-valued inverse system. -/
356@[simp] theorem projection_mul (i : I) (x y : S.inverseLimit) :
357 S.projection i (x * y) = S.projection i x * S.projection i y := rfl
359/-- Projection commutes with inversion in a group-valued inverse system. -/
360@[simp] theorem projection_inv (i : I) (x : S.inverseLimit) :
361 S.projection i x⁻¹ = (S.projection i x)⁻¹ := rfl
363/-- A group-valued inverse limit inherits a group structure coordinatewise. -/
364instance instGroupInverseLimit : Group S.inverseLimit where
365 one := 1
366 mul := (· * ·)
367 inv := Inv.inv
368 mul_assoc x y z := by
369 apply S.ext
370 intro i
371 change ((x.1 i * y.1 i) * z.1 i) = (x.1 i * (y.1 i * z.1 i))
372 simp only [mul_assoc]
373 one_mul x := by
374 apply S.ext
375 intro i
376 change 1 * x.1 i = x.1 i
377 simp only [one_mul]
378 mul_one x := by
379 apply S.ext
380 intro i
381 change x.1 i * 1 = x.1 i
382 simp only [mul_one]
383 inv_mul_cancel x := by
384 apply S.ext
385 intro i
386 change (x.1 i)⁻¹ * x.1 i = 1
387 simp only [inv_mul_cancel]
389/-- An inverse limit of topological group stages is a topological group. -/
390instance instIsTopologicalGroupInverseLimit [∀ i, IsTopologicalGroup (S.X i)] :
391 IsTopologicalGroup S.inverseLimit where
392 continuous_mul := by
393 exact Continuous.subtype_mk
394 (continuous_pi fun i =>
395 ((S.continuous_projection i).comp continuous_fst).mul
396 ((S.continuous_projection i).comp continuous_snd))
397 (fun xy => by
398 intro i j hij
399 change S.map hij (S.projection j xy.1 * S.projection j xy.2) =
400 S.projection i xy.1 * S.projection i xy.2
401 rw [IsGroupSystem.map_mul (S := S) hij,
402 S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
403 continuous_inv := by
404 exact Continuous.subtype_mk
405 (continuous_pi fun i => continuous_inv.comp (S.continuous_projection i))
406 (fun x => by
407 intro i j hij
408 change S.map hij ((S.projection j x)⁻¹) = (S.projection i x)⁻¹
409 rw [IsGroupSystem.map_inv (S := S) hij, S.projection_compatible x i j hij])
411/-- The canonical projections from a group-valued inverse limit are homomorphisms. -/
412def projectionHom (i : I) : S.inverseLimit →* S.X i where
413 toFun := S.projection i
414 map_one' := projection_one (S := S) i
415 map_mul' := by
416 intro x y
417 exact projection_mul (S := S) i x y
419/-- Evaluating the projection homomorphism is the same as evaluating the projection. -/
420@[simp] theorem projectionHom_apply (i : I) (x : S.inverseLimit) :
421 projectionHom (S := S) i x = S.projection i x := rfl
423end GroupSystems
425section AddGroupSystems
427variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
429/-- An additive-group-valued inverse system whose transition maps are additive homomorphisms. -/
430class IsAddGroupSystem (S : InverseSystem (I := I)) [∀ i, AddCommGroup (S.X i)] : Prop where
431 map_zero : ∀ {i j : I} (hij : i ≤ j), S.map hij 0 = 0
432 map_add : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
433 S.map hij (x + y) = S.map hij x + S.map hij y
434 map_neg : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
435 S.map hij (-x) = -S.map hij x
437variable [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S]
439/-- A module-valued inverse system whose transition maps are linear over a fixed semiring. -/
440class IsModuleSystem (R : Type w) [Semiring R] (S : InverseSystem (I := I))
441 [∀ i, AddCommGroup (S.X i)] [∀ i, Module R (S.X i)] : Prop where
442 map_smul : ∀ {i j : I} (hij : i ≤ j) (r : R) (x : S.X j),
443 S.map hij (r • x) = r • S.map hij x
445/-- The zero element of an additive-group-valued inverse limit is defined coordinatewise. -/
446instance instZeroAddInverseLimit : Zero S.inverseLimit where
447 zero := ⟨fun i => 0, by
448 intro i j hij
449 simpa using IsAddGroupSystem.map_zero (S := S) hij⟩
451/-- Addition in an additive-group-valued inverse limit is defined coordinatewise. -/
452instance instAddAddInverseLimit : Add S.inverseLimit where
453 add x y := ⟨fun i => S.projection i x + S.projection i y, by
454 intro i j hij
455 calc
456 S.map hij (S.projection j x + S.projection j y)
457 = S.map hij (S.projection j x) + S.map hij (S.projection j y) := by
458 simpa using IsAddGroupSystem.map_add (S := S) hij (S.projection j x)
459 (S.projection j y)
460 _ = S.projection i x + S.projection i y := by
461 rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩
463/-- Negation in an additive-group-valued inverse limit is defined coordinatewise. -/
464instance instNegAddInverseLimit : Neg S.inverseLimit where
465 neg x := ⟨fun i => -S.projection i x, by
466 intro i j hij
467 calc
468 S.map hij (-S.projection j x) = -S.map hij (S.projection j x) := by
469 simpa using IsAddGroupSystem.map_neg (S := S) hij (S.projection j x)
470 _ = -S.projection i x := by rw [S.projection_compatible x i j hij]⟩
472/-- Subtraction in an additive-group-valued inverse limit is defined coordinatewise. -/
473instance instSubAddInverseLimit : Sub S.inverseLimit where
474 sub x y := ⟨fun i => S.projection i x - S.projection i y, by
475 intro i j hij
476 change S.map hij (S.projection j x - S.projection j y) =
477 S.projection i x - S.projection i y
478 rw [sub_eq_add_neg, IsAddGroupSystem.map_add, IsAddGroupSystem.map_neg,
479 S.projection_compatible x i j hij, S.projection_compatible y i j hij, sub_eq_add_neg]⟩
481instance instSMulNatAddInverseLimit : SMul ℕ S.inverseLimit where
482 smul n x := ⟨fun i => n • S.projection i x, by
483 intro i j hij
484 change S.map hij (n • S.projection j x) = n • S.projection i x
485 induction n with
486 | zero =>
487 simp only [InverseSystem.projection_apply, zero_nsmul, IsAddGroupSystem.map_zero]
488 | succ n ihn =>
489 rw [succ_nsmul, succ_nsmul]
490 calc
491 S.map hij (n • S.projection j x + S.projection j x)
492 = S.map hij (n • S.projection j x) + S.map hij (S.projection j x) := by
493 exact IsAddGroupSystem.map_add (S := S) hij (n • S.projection j x)
494 (S.projection j x)
495 _ = n • S.projection i x + S.projection i x := by
496 rw [ihn, S.projection_compatible x i j hij]⟩
498instance instSMulIntAddInverseLimit : SMul ℤ S.inverseLimit where
499 smul n x := ⟨fun i => n • S.projection i x, by
500 intro i j hij
501 change S.map hij (n • S.projection j x) = n • S.projection i x
502 let f : S.X j →+ S.X i :=
503 { toFun := S.map hij
504 map_zero' := IsAddGroupSystem.map_zero (S := S) hij
505 map_add' := IsAddGroupSystem.map_add (S := S) hij }
506 calc
507 S.map hij (n • S.projection j x) = f (n • S.projection j x) := rfl
508 _ = n • f (S.projection j x) := f.map_zsmul (S.projection j x) n
509 _ = n • S.projection i x := by
510 change n • S.map hij (S.projection j x) = n • S.projection i x
511 rw [S.projection_compatible x i j hij]⟩
513/-- The projection of zero is zero at each stage. -/
514@[simp] theorem projection_zero (i : I) : S.projection i (0 : S.inverseLimit) = 0 := rfl
516/-- Projection commutes with addition in an additive inverse system. -/
517@[simp] theorem projection_add (i : I) (x y : S.inverseLimit) :
518 S.projection i (x + y) = S.projection i x + S.projection i y := rfl
520/-- Projection commutes with negation in an additive inverse system. -/
521@[simp] theorem projection_neg (i : I) (x : S.inverseLimit) :
522 S.projection i (-x) = -S.projection i x := rfl
524/-- Projection commutes with subtraction in an additive inverse system. -/
525@[simp] theorem projection_sub (i : I) (x y : S.inverseLimit) :
526 S.projection i (x - y) = S.projection i x - S.projection i y := rfl
528/-- An additive-group-valued inverse limit inherits an additive commutative group structure. -/
529instance instAddCommGroupAddInverseLimit : AddCommGroup S.inverseLimit := by
530 let f : S.inverseLimit → ∀ i, S.X i := Subtype.val
531 apply Subtype.val_injective.addCommGroup f rfl (fun _ _ => rfl) (fun _ => rfl)
532 (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
534section ModuleSystems
536variable {R : Type w} [Semiring R]
537variable [∀ i, Module R (S.X i)] [IsModuleSystem (I := I) R S]
539/-- Scalar multiplication on a module-valued inverse limit is defined coordinatewise. -/
540instance instSMulInverseLimitOfIsModuleSystem : SMul R S.inverseLimit where
541 smul r x := ⟨fun i => r • S.projection i x, by
542 intro i j hij
543 change S.map hij (r • S.projection j x) = r • S.projection i x
544 rw [IsModuleSystem.map_smul (S := S) hij, S.projection_compatible x i j hij]⟩
547/-- Projection commutes with scalar multiplication in a module-valued inverse system. -/
548@[simp] theorem projection_smul_of_isModuleSystem (i : I) (r : R) (x : S.inverseLimit) :
549 S.projection i (r • x) = r • S.projection i x :=
550 rfl
552/-- A module-valued inverse limit inherits a module structure coordinatewise. -/
553instance instModuleInverseLimitOfIsModuleSystem : Module R S.inverseLimit := by
554 let f : S.inverseLimit →+ ∀ i, S.X i :=
555 { toFun := Subtype.val
556 map_zero' := rfl
557 map_add' := fun _ _ => rfl }
558 exact Function.Injective.module R f Subtype.val_injective (fun _ _ => rfl)
560/-- Scalar multiplication on a module-valued inverse limit is continuous when it is continuous
561stagewise. -/
563 [TopologicalSpace R] [∀ i, ContinuousSMul R (S.X i)] :
564 ContinuousSMul R S.inverseLimit where
565 continuous_smul := by
566 exact Continuous.subtype_mk
567 (continuous_pi fun i =>
568 continuous_fst.smul ((S.continuous_projection i).comp continuous_snd))
569 (fun p => by
570 intro i j hij
571 change S.map hij (p.1 • S.projection j p.2) = p.1 • S.projection i p.2
572 rw [IsModuleSystem.map_smul (S := S) hij, S.projection_compatible p.2 i j hij])
574end ModuleSystems
576/-- An inverse limit of topological additive groups is a topological additive group. -/
577instance instIsTopologicalAddGroupAddInverseLimit [∀ i, IsTopologicalAddGroup (S.X i)] :
578 IsTopologicalAddGroup S.inverseLimit where
579 continuous_add := by
580 exact Continuous.subtype_mk
581 (continuous_pi fun i =>
582 ((S.continuous_projection i).comp continuous_fst).add
583 ((S.continuous_projection i).comp continuous_snd))
584 (fun xy => by
585 intro i j hij
586 change S.map hij (S.projection j xy.1 + S.projection j xy.2) =
587 S.projection i xy.1 + S.projection i xy.2
588 rw [IsAddGroupSystem.map_add (S := S) hij,
589 S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
590 continuous_neg := by
591 exact Continuous.subtype_mk
592 (continuous_pi fun i => continuous_neg.comp (S.continuous_projection i))
593 (fun x => by
594 intro i j hij
595 change S.map hij (-S.projection j x) = -S.projection i x
596 rw [IsAddGroupSystem.map_neg (S := S) hij, S.projection_compatible x i j hij])
598/-- The canonical projections from an additive inverse limit are additive homomorphisms. -/
599def projectionAddHom (i : I) : S.inverseLimit →+ S.X i where
600 toFun := S.projection i
601 map_zero' := projection_zero (S := S) i
602 map_add' := by
603 intro x y
604 exact projection_add (S := S) i x y
606/-- Evaluating the projection additive homomorphism is projection evaluation. -/
607@[simp] theorem projectionAddHom_apply (i : I) (x : S.inverseLimit) :
608 projectionAddHom (S := S) i x = S.projection i x := rfl
610end AddGroupSystems
612section RingSystems
614variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))
616/-- A ring-valued inverse system whose transition maps are ring homomorphisms. -/
617class IsRingSystem (S : InverseSystem (I := I)) [∀ i, Ring (S.X i)] : Prop where
618 map_zero : ∀ {i j : I} (hij : i ≤ j), S.map hij 0 = 0
619 map_one : ∀ {i j : I} (hij : i ≤ j), S.map hij 1 = 1
620 map_add : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
621 S.map hij (x + y) = S.map hij x + S.map hij y
622 map_mul : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
623 S.map hij (x * y) = S.map hij x * S.map hij y
625variable [∀ i, Ring (S.X i)] [IsRingSystem S]
627/-- A transition map in a ring-valued inverse system, bundled as a ring homomorphism. -/
628def mapRingHom {i j : I} (hij : i ≤ j) : S.X j →+* S.X i where
629 toFun := S.map hij
630 map_zero' := IsRingSystem.map_zero (S := S) hij
631 map_one' := IsRingSystem.map_one (S := S) hij
632 map_add' := IsRingSystem.map_add (S := S) hij
633 map_mul' := IsRingSystem.map_mul (S := S) hij
635@[simp]
636theorem mapRingHom_apply {i j : I} (hij : i ≤ j) (x : S.X j) :
637 mapRingHom (S := S) hij x = S.map hij x := rfl
640 map_zero := IsRingSystem.map_zero (S := S)
641 map_add := IsRingSystem.map_add (S := S)
642 map_neg := by
643 intro i j hij x
644 exact (mapRingHom (S := S) hij).map_neg x
646/-- Multiplication in a ring-valued inverse limit is defined coordinatewise. -/
647instance instMulRingInverseLimit : Mul S.inverseLimit where
648 mul x y := ⟨fun i => S.projection i x * S.projection i y, by
649 intro i j hij
650 calc
651 S.map hij (S.projection j x * S.projection j y)
652 = S.map hij (S.projection j x) * S.map hij (S.projection j y) := by
653 exact IsRingSystem.map_mul (S := S) hij (S.projection j x)
654 (S.projection j y)
655 _ = S.projection i x * S.projection i y := by
656 rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩
658/-- The unit in a ring-valued inverse limit is defined coordinatewise. -/
659instance instOneRingInverseLimit : One S.inverseLimit where
660 one := ⟨fun i => 1, by
661 intro i j hij
662 exact IsRingSystem.map_one (S := S) hij⟩
664/-- Natural powers in a ring-valued inverse limit are defined coordinatewise. -/
665instance instPowNatRingInverseLimit : Pow S.inverseLimit ℕ where
666 pow x n := ⟨fun i => S.projection i x ^ n, by
667 intro i j hij
668 change S.map hij (S.projection j x ^ n) = S.projection i x ^ n
669 rw [← mapRingHom_apply (S := S) hij, map_pow, mapRingHom_apply,
670 S.projection_compatible x i j hij]⟩
672/-- Natural-number casts in a ring-valued inverse limit are defined coordinatewise. -/
673instance instNatCastRingInverseLimit : NatCast S.inverseLimit where
674 natCast n := ⟨fun _ => n, by
675 intro i j hij
676 change S.map hij (Nat.cast n) = Nat.cast n
677 exact map_natCast (mapRingHom (S := S) hij) n⟩
679/-- Integer casts in a ring-valued inverse limit are defined coordinatewise. -/
680instance instIntCastRingInverseLimit : IntCast S.inverseLimit where
681 intCast n := ⟨fun _ => n, by
682 intro i j hij
683 change S.map hij (Int.cast n) = Int.cast n
684 exact map_intCast (mapRingHom (S := S) hij) n⟩
686@[simp]
687theorem projection_ring_one (i : I) : S.projection i (1 : S.inverseLimit) = 1 := rfl
689@[simp]
690theorem projection_ring_mul (i : I) (x y : S.inverseLimit) :
691 S.projection i (x * y) = S.projection i x * S.projection i y := rfl
693@[simp]
694theorem projection_ring_pow (i : I) (x : S.inverseLimit) (n : ℕ) :
695 S.projection i (x ^ n) = S.projection i x ^ n := rfl
697@[simp]
698theorem projection_ring_natCast (i : I) (n : ℕ) :
699 S.projection i (Nat.cast n : S.inverseLimit) = Nat.cast n := rfl
701@[simp]
702theorem projection_ring_intCast (i : I) (n : ℤ) :
703 S.projection i (Int.cast n : S.inverseLimit) = Int.cast n := rfl
705/-- A ring-valued inverse limit inherits a ring structure coordinatewise. -/
706instance instRingInverseLimit : Ring S.inverseLimit :=
707 Function.Injective.ring
708 (fun x : S.inverseLimit => (x : ∀ i, S.X i))
709 Subtype.val_injective
710 (by funext i; rfl)
711 (by funext i; rfl)
712 (by intro x y; funext i; rfl)
713 (by intro x y; funext i; rfl)
714 (by intro x; funext i; rfl)
715 (by intro x y; funext i; rfl)
716 (by intro n x; funext i; rfl)
717 (by intro n x; funext i; rfl)
718 (by intro x n; funext i; rfl)
719 (by intro n; funext i; rfl)
720 (by intro n; funext i; rfl)
722/-- Multiplication on a ring-valued inverse limit is continuous when it is continuous stagewise. -/
723instance instContinuousMulRingInverseLimit [∀ i, ContinuousMul (S.X i)] :
724 ContinuousMul S.inverseLimit where
725 continuous_mul := by
726 exact Continuous.subtype_mk
727 (continuous_pi fun i =>
728 ((S.continuous_projection i).comp continuous_fst).mul
729 ((S.continuous_projection i).comp continuous_snd))
730 (fun xy => by
731 intro i j hij
732 change S.map hij (S.projection j xy.1 * S.projection j xy.2) =
733 S.projection i xy.1 * S.projection i xy.2
734 rw [IsRingSystem.map_mul (S := S) hij,
735 S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
737/-- An inverse limit of topological rings is a topological ring. -/
738instance instIsTopologicalRingRingInverseLimit [∀ i, IsTopologicalRing (S.X i)] :
739 IsTopologicalRing S.inverseLimit := by
740 letI : IsTopologicalAddGroup S.inverseLimit :=
742 letI : ContinuousMul S.inverseLimit := instContinuousMulRingInverseLimit S
743 letI : IsTopologicalSemiring S.inverseLimit := IsTopologicalSemiring.mk
744 exact IsTopologicalRing.mk
746/-- The canonical projection from a ring-valued inverse limit, bundled as a ring homomorphism. -/
747def projectionRingHom (i : I) : S.inverseLimit →+* S.X i where
748 toFun := S.projection i
749 map_zero' := projection_zero (S := S) i
750 map_one' := projection_ring_one (S := S) i
751 map_add' := by
752 intro x y
753 exact projection_add (S := S) i x y
754 map_mul' := by
755 intro x y
756 exact projection_ring_mul (S := S) i x y
758@[simp]
759theorem projectionRingHom_apply (i : I) (x : S.inverseLimit) :
760 projectionRingHom (S := S) i x = S.projection i x := rfl
762/-- The ring-valued transition from `j` to `i` composed with the `j`-th projection is the
763`i`-th projection. -/
764theorem mapRingHom_comp_projectionRingHom {i j : I} (hij : i ≤ j) :
765 (mapRingHom (S := S) hij).comp (projectionRingHom (S := S) j) =
766 projectionRingHom (S := S) i := by
767 apply RingHom.ext
768 intro x
769 exact S.projection_compatible x i j hij
771end RingSystems
773end
774end InverseSystems
775end ProCGroups