Source: ProCGroups.InverseSystems.ProfiniteLimits
1import ProCGroups.InverseSystems.CofinalityAndDensity
2import ProCGroups.Profinite.Basic
4/-!
5# Projection kernels in profinite inverse limits
7For inverse systems of finite discrete groups, the canonical projections are bundled as group
8homomorphisms. Their kernels are open normal subgroups, and under the usual directedness and
9surjectivity assumptions these kernels form a fundamental system of neighborhoods of one in
10the inverse limit.
11-/
13open scoped Topology Pointwise
15namespace ProCGroups
17universe u v
19section
21variable {G : Type u} [Group G] [TopologicalSpace G]
23/--
24The projection from a group-valued inverse limit to one component is viewed as a homomorphism.
25-/
26def inverseLimitProjectionHom {I : Type v} [Preorder I]
27 (S : InverseSystems.InverseSystem (I := I))
28 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S] (i : I) :
29 S.inverseLimit →* S.X i where
30 toFun := S.projection i
31 map_one' := rfl
32 map_mul' := by
33 intro x y
34 rfl
36/-- The kernel of a projection from an inverse limit of discrete groups is open normal. -/
37def inverseLimitProjectionKer {I : Type v} [Preorder I]
38 (S : InverseSystems.InverseSystem (I := I))
39 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
40 [∀ i, DiscreteTopology (S.X i)] (i : I) :
41 OpenNormalSubgroup S.inverseLimit where
42 toOpenSubgroup :=
43 { toSubgroup := (inverseLimitProjectionHom S i).ker
44 isOpen' := by
45 change IsOpen (S.projection i ⁻¹' ({1} : Set (S.X i)))
46 exact
47 (isOpen_discrete ({1} : Set (S.X i))).preimage
48 (S.continuous_projection i) }
49 isNormal' := by
50 change ((inverseLimitProjectionHom S i).ker).Normal
51 infer_instance
53/--
54Membership in the kernel of an inverse-limit projection is membership in the kernel at that
55finite stage.
56-/
57@[simp] theorem mem_inverseLimitProjectionKer {I : Type v} [Preorder I]
58 {S : InverseSystems.InverseSystem (I := I)}
59 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
60 [∀ i, DiscreteTopology (S.X i)]
61 {i : I} {x : S.inverseLimit} :
62 x ∈ inverseLimitProjectionKer S i ↔ S.projection i x = 1 :=
63 Iff.rfl
65/--
66In an inverse limit of discrete groups, every open neighborhood of \(1\) contains the kernel of
67one projection map.
68-/
69theorem exists_inverseLimitProjectionKer_sub_open_nhds_of_one
70 {I : Type v} [Preorder I]
71 (S : InverseSystems.InverseSystem (I := I)) [Nonempty I]
72 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
73 [∀ i, DiscreteTopology (S.X i)]
74 (hdir : Directed (· ≤ ·) (id : I → I))
75 {W : Set S.inverseLimit} (hW : IsOpen W) (h1W : (1 : S.inverseLimit) ∈ W) :
76 ∃ i : I,
77 (((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
78 Subgroup S.inverseLimit) : Set S.inverseLimit) ⊆ W := by
79 rcases S.exists_projection_preimage_subset hdir hW h1W with ⟨i, V, -, h1V, hVW⟩
80 refine ⟨i, ?_⟩
81 intro x hx
82 have hxker : S.projection i x = 1 := (mem_inverseLimitProjectionKer (S := S) (i := i)).1 hx
83 have hV1 : (1 : S.X i) ∈ V := h1V
84 have hxV : x ∈ S.projection i ⁻¹' V := by
85 change S.projection i x ∈ V
86 rw [hxker]
87 exact hV1
88 exact hVW hxV
90/--
91The projection kernels form a fundamental system of open neighborhoods of 1 in the inverse
92limit.
93-/
94theorem inverseLimitProjectionKer_fundamentalSystemAtOne
95 {I : Type v} [Preorder I]
96 (S : InverseSystems.InverseSystem (I := I)) [Nonempty I]
97 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
98 [∀ i, DiscreteTopology (S.X i)]
99 (hdir : Directed (· ≤ ·) (id : I → I)) :
100 (∀ i : I,
101 IsOpen ((((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
102 Subgroup S.inverseLimit) : Set S.inverseLimit)) ∧
103 (1 : S.inverseLimit) ∈ (((inverseLimitProjectionKer S i :
104 OpenNormalSubgroup S.inverseLimit) : Subgroup S.inverseLimit) : Set S.inverseLimit)) ∧
105 ∀ W : Set S.inverseLimit, IsOpen W → (1 : S.inverseLimit) ∈ W →
106 ∃ i : I,
107 ((((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
108 Subgroup S.inverseLimit) : Set S.inverseLimit)) ⊆ W := by
109 refine ⟨?_, ?_⟩
110 · intro i
111 refine ⟨openNormalSubgroup_isOpen (G := S.inverseLimit) (inverseLimitProjectionKer S i), ?_⟩
112 change ((1 : S.inverseLimit).1 i) = 1
113 rfl
114 · intro W hW h1W
115 exact exists_inverseLimitProjectionKer_sub_open_nhds_of_one S hdir hW h1W
117end
119end ProCGroups