Source: ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients
1import ProCGroups.ProC.Quotients.OpenSubgroupSections
3/-!
4# Quotients along descending closed-subgroup systems
6This file constructs the inverse system of left quotients associated with a directed descending
7family of closed subgroups and proves the existence of compatible continuous lifts into its
8limit.
9-/
11open Set
12open scoped Topology Pointwise
14namespace ProCGroups.ProC
16universe u v
18open InverseSystems
20variable {I : Type v} [Preorder I] [Nonempty I]
21variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
22 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
24/-- The infimum of a family of closed subgroups, repackaged as a closed subgroup. -/
25def closedSubgroup_sInf (L : I → ClosedSubgroup G) : ClosedSubgroup G where
26 toSubgroup := iInf fun i => (L i : Subgroup G)
27 isClosed' := by
28 convert isClosed_iInter fun i => (L i).isClosed' using 1
29 ext x
30 simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid,
31 Subgroup.mem_iInf, mem_iInter]
33/-- The infimum subgroup is contained in each term of the family. -/
34theorem closedSubgroup_sInf_le {I : Type v} {G : Type u} [Group G] [TopologicalSpace G]
35 (L : I → ClosedSubgroup G) (i : I) :
36 (closedSubgroup_sInf L : Subgroup G) ≤ (L i : Subgroup G) := by
37 exact iInf_le _ i
39/--
40The inverse system of left quotient spaces attached to a decreasing family of closed subgroups.
41-/
42def descendingClosedSubgroupSystem (L : I → ClosedSubgroup G)
43 (hL : ∀ {i j}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G)) :
44 InverseSystems.InverseSystem (I := I) where
45 X i := G ⧸ (L i : Subgroup G)
46 topologicalSpace i := inferInstance
47 map := fun {i j} hij =>
48 leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij)
49 continuous_map := by
50 intro i j hij
51 exact continuous_leftQuotientProjection
52 (K := (L j : Subgroup G)) (H := (L i : Subgroup G)) (hL hij)
53 map_id := by
54 intro i
55 exact leftQuotientProjection_id (K := (L i : Subgroup G))
56 map_comp := by
57 intro i j k hij hjk
58 exact
59 leftQuotientProjection_comp
60 (K := (L k : Subgroup G)) (H := (L j : Subgroup G)) (L := (L i : Subgroup G))
61 (hL hjk) (hL hij)
63omit [T2Space G] [TotallyDisconnectedSpace G] in
64/--
65A compatible family of maps into a decreasing family of left quotient spaces lifts uniquely to
66the quotient by the infimum subgroup.
67-/
68theorem exists_continuous_leftQuotient_lift_of_directed
69 (L : I → ClosedSubgroup G)
70 (hL : ∀ {i j}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G))
71 (hdir : Directed (· ≤ ·) (id : I → I))
72 {Y : Type v} [TopologicalSpace Y]
73 (η : ∀ i, Y → G ⧸ (L i : Subgroup G))
74 (hηcont : ∀ i, Continuous (η i))
75 (hηcompat : ∀ {i j} (hij : i ≤ j),
76 leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j = η i)
77 (y0 : Y)
78 (hηone : ∀ i, η i y0 = QuotientGroup.mk (s := (L i : Subgroup G)) (1 : G)) :
79 ∃ ηinf : Y → G ⧸ ((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G),
80 Continuous ηinf ∧
81 (∀ i,
82 leftQuotientProjection
83 (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))
84 (L i : Subgroup G)
85 (closedSubgroup_sInf_le (L := L) i) ∘ ηinf = η i) ∧
86 ηinf y0 =
87 QuotientGroup.mk (s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)))
88 (1 : G) := by
89 classical
90 let Linf : ClosedSubgroup G := closedSubgroup_sInf L
91 let S : InverseSystems.InverseSystem (I := I) := descendingClosedSubgroupSystem L hL
92 letI : IsClosed (((Linf : ClosedSubgroup G) : Subgroup G) : Set G) := Linf.isClosed'
93 letI : ∀ i, IsClosed (((L i : ClosedSubgroup G) : Subgroup G) : Set G) := fun i => (L i).isClosed'
94 letI : ∀ i, T2Space (S.X i) := fun i => by
95 change T2Space (G ⧸ (L i : Subgroup G))
96 infer_instance
97 let ψ : ∀ i, G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) → S.X i := fun i =>
98 leftQuotientProjection
99 (((Linf : ClosedSubgroup G) : Subgroup G))
100 (L i : Subgroup G)
101 (closedSubgroup_sInf_le (L := L) i)
102 have hψcont : ∀ i, Continuous (ψ i) := by
103 intro i
104 exact continuous_leftQuotientProjection
105 (K := (((Linf : ClosedSubgroup G) : Subgroup G)))
106 (H := (L i : Subgroup G))
107 (closedSubgroup_sInf_le (L := L) i)
108 have hψcompat : S.CompatibleMaps ψ := by
109 intro i j hij
110 funext x
111 change
112 leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij)
113 (leftQuotientProjection
114 ((Linf : ClosedSubgroup G) : Subgroup G) (L j : Subgroup G)
115 (closedSubgroup_sInf_le (L := L) j) x) =
116 leftQuotientProjection
117 ((Linf : ClosedSubgroup G) : Subgroup G) (L i : Subgroup G)
118 (closedSubgroup_sInf_le (L := L) i) x
119 exact leftQuotientProjection_comp_apply
120 ((Linf : ClosedSubgroup G) : Subgroup G)
121 (L j : Subgroup G) (L i : Subgroup G)
122 (closedSubgroup_sInf_le (L := L) j) (hL hij) x
123 let φ : G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) → S.inverseLimit :=
124 S.inverseLimitLift ψ hψcompat
125 have hφcont : Continuous φ := S.continuous_inverseLimitLift ψ hψcont hψcompat
126 have hψsurj : ∀ i, Function.Surjective (ψ i) := by
127 intro i
128 exact surjective_leftQuotientProjection
129 (K := (((Linf : ClosedSubgroup G) : Subgroup G)))
130 (H := (L i : Subgroup G))
131 (closedSubgroup_sInf_le (L := L) i)
132 have hφsurj : Function.Surjective φ :=
133 S.surjective_inverseLimitLift ψ hψcont hψcompat hψsurj hdir
134 have hφinj : Function.Injective φ := by
135 intro x y hxy
136 rcases Quotient.exists_rep x with ⟨gx, rfl⟩
137 rcases Quotient.exists_rep y with ⟨gy, rfl⟩
138 apply QuotientGroup.eq.2
139 have hcoord :
140 ∀ i, gx⁻¹ * gy ∈ (L i : Subgroup G) := by
141 intro i
142 have hi : ψ i (QuotientGroup.mk (s := (((Linf : ClosedSubgroup G) : Subgroup G))) gx) =
143 ψ i (QuotientGroup.mk (s := (((Linf : ClosedSubgroup G) : Subgroup G))) gy) := by
144 exact congrArg (fun z : S.inverseLimit => S.projection i z) hxy
145 exact QuotientGroup.eq.1 hi
146 change gx⁻¹ * gy ∈ iInf fun i => (L i : Subgroup G)
147 rw [Subgroup.mem_iInf]
148 exact hcoord
149 let eTop : G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) ≃ₜ S.inverseLimit :=
150 Continuous.homeoOfEquivCompactToT2
151 (f := Equiv.ofBijective φ ⟨hφinj, hφsurj⟩) hφcont
152 let ηinf : Y → G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) :=
153 eTop.symm ∘ S.inverseLimitLift η (by
154 intro i j hij
155 simpa only [S, descendingClosedSubgroupSystem, Function.comp] using hηcompat hij)
156 have hηinf_continuous : Continuous ηinf := by
157 exact eTop.continuous_invFun.comp <| S.continuous_inverseLimitLift η hηcont <| by
158 intro i j hij
159 simpa only [S, descendingClosedSubgroupSystem, Function.comp] using hηcompat hij
160 have hηinf_fac :
161 ∀ i,
162 leftQuotientProjection
163 (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))
164 (L i : Subgroup G)
165 (closedSubgroup_sInf_le (L := L) i) ∘ ηinf = η i := by
166 intro i
167 funext y
168 have hfac :=
169 congrFun (S.projection_comp_inverseLimitLift η
170 (by
171 intro i j hij
172 simpa only [S, descendingClosedSubgroupSystem, Function.comp] using hηcompat hij) i) y
173 have hcoord :
174 S.projection i (eTop (ηinf y)) = η i y := by
175 simpa [ηinf, Function.comp] using hfac
176 exact hcoord
177 have hηinf_one :
178 ηinf y0 =
179 QuotientGroup.mk (s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)))
180 (1 : G) := by
181 apply eTop.injective
182 apply S.ext
183 intro i
184 have hy0 := congrFun (hηinf_fac i) y0
185 change leftQuotientProjection
186 (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))
187 (L i : Subgroup G)
188 (closedSubgroup_sInf_le (L := L) i) (ηinf y0) =
189 leftQuotientProjection
190 (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))
191 (L i : Subgroup G)
192 (closedSubgroup_sInf_le (L := L) i)
193 (QuotientGroup.mk
194 (s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))) (1 : G))
195 simpa [hηone i]
196 using hy0
197 exact ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩
199end ProCGroups.ProC