ProCGroups/InverseSystems/ProfiniteLimits.lean
1import ProCGroups.Profinite.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/InverseSystems/ProfiniteLimits.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Inverse systems and inverse limits
14Defines inverse systems of topological groups and proves lift, projection, exactness, quotient, stagewise isomorphism, and finite-stage factorization results.
15-/
17open scoped Topology Pointwise
19namespace ProCGroups
21universe u v
23section
25variable {G : Type u} [Group G] [TopologicalSpace G]
27/-- The projection from a group-valued inverse limit to one component, viewed as a homomorphism. -/
28def inverseLimitProjectionHom {I : Type v} [Preorder I]
29 (S : InverseSystems.InverseSystem (I := I))
30 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S] (i : I) :
31 S.inverseLimit →* S.X i where
32 toFun := S.projection i
33 map_one' := rfl
34 map_mul' := by
35 intro x y
36 rfl
38/-- The kernel of a projection from an inverse limit of discrete groups is open normal. -/
39def inverseLimitProjectionKer {I : Type v} [Preorder I]
40 (S : InverseSystems.InverseSystem (I := I))
41 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
42 [∀ i, DiscreteTopology (S.X i)] (i : I) :
43 OpenNormalSubgroup S.inverseLimit where
44 toOpenSubgroup :=
45 { toSubgroup := (inverseLimitProjectionHom S i).ker
46 isOpen' := by
47 change IsOpen {x : S.inverseLimit | inverseLimitProjectionHom S i x = 1}
48 simpa [inverseLimitProjectionHom] using
49 (isOpen_discrete ({1} : Set (S.X i))).preimage (S.continuous_projection i) }
50 isNormal' := by
51 change ((inverseLimitProjectionHom S i).ker).Normal
52 infer_instance
54/-- Membership in the kernel of an inverse-limit projection is membership in the kernel at that finite stage. -/
55@[simp] theorem mem_inverseLimitProjectionKer {I : Type v} [Preorder I]
56 {S : InverseSystems.InverseSystem (I := I)}
57 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
58 [∀ i, DiscreteTopology (S.X i)]
59 {i : I} {x : S.inverseLimit} :
60 x ∈ inverseLimitProjectionKer S i ↔ S.projection i x = 1 :=
61 Iff.rfl
63/-- In an inverse limit of discrete groups, every open neighborhood of `1` contains the kernel of
66 {I : Type v} [Preorder I]
67 (S : InverseSystems.InverseSystem (I := I)) [Nonempty I]
68 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
69 [∀ i, DiscreteTopology (S.X i)]
70 (hdir : Directed (· ≤ ·) (id : I → I))
71 {W : Set S.inverseLimit} (hW : IsOpen W) (h1W : (1 : S.inverseLimit) ∈ W) :
72 ∃ i : I,
73 (((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
74 Subgroup S.inverseLimit) : Set S.inverseLimit) ⊆ W := by
75 rcases S.exists_projection_preimage_subset hdir hW h1W with ⟨i, V, -, h1V, hVW⟩
76 refine ⟨i, ?_⟩
77 intro x hx
78 have hxker : S.projection i x = 1 := (mem_inverseLimitProjectionKer (S := S) (i := i)).1 hx
79 have hV1 : (1 : S.X i) ∈ V := h1V
80 have hxV : x ∈ S.projection i ⁻¹' V := by
81 change S.projection i x ∈ V
82 rw [hxker]
83 exact hV1
84 exact hVW hxV
86/-- The projection kernels form a fundamental system of open neighborhoods of `1` in the inverse
87limit. -/
89 {I : Type v} [Preorder I]
90 (S : InverseSystems.InverseSystem (I := I)) [Nonempty I]
91 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
92 [∀ i, DiscreteTopology (S.X i)]
93 (hdir : Directed (· ≤ ·) (id : I → I)) :
94 (∀ i : I,
95 IsOpen ((((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
96 Subgroup S.inverseLimit) : Set S.inverseLimit)) ∧
97 (1 : S.inverseLimit) ∈ (((inverseLimitProjectionKer S i :
98 OpenNormalSubgroup S.inverseLimit) : Subgroup S.inverseLimit) : Set S.inverseLimit)) ∧
99 ∀ W : Set S.inverseLimit, IsOpen W → (1 : S.inverseLimit) ∈ W →
100 ∃ i : I,
101 ((((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
102 Subgroup S.inverseLimit) : Set S.inverseLimit)) ⊆ W := by
103 refine ⟨?_, ?_⟩
104 · intro i
105 refine ⟨openNormalSubgroup_isOpen (G := S.inverseLimit) (inverseLimitProjectionKer S i), ?_⟩
106 change ((1 : S.inverseLimit).1 i) = 1
107 rfl
108 · intro W hW h1W
109 exact exists_inverseLimitProjectionKer_sub_open_nhds_of_one S hdir hW h1W
111end
113end ProCGroups