Source: ProCGroups.ProC.Quotients.OpenSubgroupSections

1import Mathlib.Topology.Algebra.ProperAction.Basic

2import ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods

4/-!

5# Sections for quotients by open subgroups

7Finite quotients by open subgroups admit normalized choice sections, which are continuous because

8the quotient is discrete. This file records their right-inverse property and derives sections of

9left-quotient projections with an open lower subgroup.

10-/

12open Set

13open scoped Topology Pointwise

15namespace ProCGroups.ProC

17universe u v

19open InverseSystems

21variable {G : Type u} [Group G]

23/--

24A normalized set-theoretic section of the quotient map by an open subgroup. Since the quotient

25is discrete, this section is automatically continuous.

26-/

27noncomputable def quotientOpenSubgroupSection (U : Subgroup G) :

28 (G ⧸ U) → G := by

29 classical

30 intro q

31 exact if hq : q = QuotientGroup.mk (s := U) (1 : G) then 1

32 else Classical.choose (Quotient.exists_rep q)

34/-- The normalized set-theoretic section sends the identity coset to the identity. -/

35@[simp] theorem quotientOpenSubgroupSection_one

36 (U : Subgroup G) :

37 quotientOpenSubgroupSection U (QuotientGroup.mk (s := U) (1 : G)) = 1 := by

38 classical

39 simp only [quotientOpenSubgroupSection, ↓reduceDIte]

41/-- The normalized section is a genuine right inverse to the quotient map. -/

42theorem quotientOpenSubgroupSection_rightInverse

43 (U : Subgroup G) :

44 Function.RightInverse (quotientOpenSubgroupSection U)

45 (QuotientGroup.mk (s := U)) := by

46 classical

47 intro q

48 by_cases hq : q = QuotientGroup.mk (s := U) (1 : G)

49 · subst hq

50 simp only [quotientOpenSubgroupSection, ↓reduceDIte]

51 · simpa [quotientOpenSubgroupSection, hq] using

52 (Classical.choose_spec (Quotient.exists_rep q))

54/-- The normalized section by an open subgroup is continuous because the quotient is discrete. -/

55theorem continuous_quotientOpenSubgroupSection

56 [TopologicalSpace G]

57 [IsTopologicalGroup G]

58 (U : Subgroup G) (hU : IsOpen (U : Set G)) :

59 Continuous (quotientOpenSubgroupSection U) := by

60 letI : ContinuousMul G := (‹IsTopologicalGroup G›).toContinuousMul

61 letI : ContinuousInv G := (‹IsTopologicalGroup G›).toContinuousInv

62 letI : DiscreteTopology (G ⧸ U) := QuotientGroup.discreteTopology hU

63 simpa using

64 (continuous_of_discreteTopology :

65 Continuous (quotientOpenSubgroupSection U))

67/--

68Helper for the finite/open case: the canonical quotient map by an open normal subgroup of a

69profinite group admits a continuous section normalized by \(s(1)=1\). The actual section data is

70provided by quotientOpenSubgroupSection.

71-/

72theorem quotient_openNormalSubgroup_hasContinuousSection

73 [TopologicalSpace G]

74 [IsTopologicalGroup G]

75 (U : OpenNormalSubgroup G) :

76 ∃ σ : (G ⧸ (U : Subgroup G)) → G,

77 Continuous σ ∧

78 Function.RightInverse σ (QuotientGroup.mk' (U : Subgroup G)) ∧

79 σ 1 = 1 := by

80 let hU : IsOpen ((U : Subgroup G) : Set G) := openNormalSubgroup_isOpen (G := G) U

81 refine ⟨quotientOpenSubgroupSection (U : Subgroup G), ?_, ?_, ?_⟩

82 · simpa using continuous_quotientOpenSubgroupSection (G := G) (U : Subgroup G) hU

83 · simpa [QuotientGroup.mk'] using

84 quotientOpenSubgroupSection_rightInverse (G := G) (U : Subgroup G)

85 · simpa using quotientOpenSubgroupSection_one (G := G) (U : Subgroup G)

87/-- Finite-index case of the section theorem for left quotient projections. -/

88theorem leftQuotientProjection_hasContinuousSection_of_openSubgroup

89 [TopologicalSpace G]

90 [IsTopologicalGroup G]

91 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

92 (K H : ClosedSubgroup G)

93 (hKH : (K : Subgroup G) ≤ (H : Subgroup G))

94 (hKopen : IsOpen (((K : Subgroup G).subgroupOf (H : Subgroup G)) : Set H)) :

95 ∃ σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G),

96 Continuous σ ∧

97 Function.RightInverse σ

98 (leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH) ∧

99 σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =

100 QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) := by

101 classical

102 letI : ContinuousMul G := (‹IsTopologicalGroup G›).toContinuousMul

103 letI : ContinuousInv G := (‹IsTopologicalGroup G›).toContinuousInv

104 letI : IsClosed (((K : ClosedSubgroup G) : Subgroup G) : Set G) := K.isClosed'

105 letI : IsClosed (((H : ClosedSubgroup G) : Subgroup G) : Set G) := H.isClosed'

106 let UH : OpenSubgroup H :=

107 ⟨((K : Subgroup G).subgroupOf (H : Subgroup G)), hKopen⟩

108 obtain ⟨V, hVHK⟩ :=

109 exists_openNormalSubgroup_inter_closedSubgroup_le (G := G) H UH

110 have hVcapHK : ((V : Subgroup G) ⊓ (H : Subgroup G)) ≤ (K : Subgroup G) := by

111 intro x hx

112 exact hVHK <| show (⟨x, hx.2⟩ : H) ∈

113 (OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V : Subgroup H)

114 by

115 change x ∈ (V : Subgroup G)

116 exact hx.1

117 let J : Subgroup G := (H : Subgroup G) ⊔ (V : Subgroup G)

118 have hHJ : (H : Subgroup G) ≤ J := le_sup_left

119 have hKJ : (K : Subgroup G) ≤ J := hKH.trans hHJ

120 have hJopen : IsOpen (J : Set G) := by

121 exact Subgroup.isOpen_of_openSubgroup J (show (V : Subgroup G) ≤ J from le_sup_right)

122 let ρ : G ⧸ J → G := quotientOpenSubgroupSection J

123 have hρcont : Continuous ρ := continuous_quotientOpenSubgroupSection J hJopen

124 have hρright : Function.RightInverse ρ (QuotientGroup.mk (s := J)) :=

125 quotientOpenSubgroupSection_rightInverse J

126 let WK : Set (G ⧸ (K : Subgroup G)) :=

127 (QuotientGroup.mk (s := (K : Subgroup G))) ''

128 ((((V : OpenNormalSubgroup G) : Subgroup G) : Set G))

129 let BH : Set (G ⧸ (H : Subgroup G)) :=

130 (QuotientGroup.mk (s := (H : Subgroup G))) ''

131 ((((V : OpenNormalSubgroup G) : Subgroup G) : Set G))

132 have hVclosed : IsClosed ((((V : OpenNormalSubgroup G) : Subgroup G) : Set G)) :=

133 openNormalSubgroup_isClosed (G := G) V

134 have hWKcompact : IsCompact WK := by

135 exact hVclosed.isCompact.image (QuotientGroup.continuous_mk :

136 Continuous (QuotientGroup.mk (s := (K : Subgroup G)) : G → G ⧸ (K : Subgroup G)))

137 have hBHcompact : IsCompact BH := by

138 exact hVclosed.isCompact.image (QuotientGroup.continuous_mk :

139 Continuous (QuotientGroup.mk (s := (H : Subgroup G)) : G → G ⧸ (H : Subgroup G)))

140 have hBHclosed : IsClosed BH := by

141 exact hBHcompact.isClosed

142 let πloc : WK → BH := fun x =>

143 ⟨leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH x.1, by

144 rcases x with ⟨x, hx⟩

145 rcases hx with ⟨g, hg, rfl⟩

146 exact ⟨g, hg, rfl⟩⟩

147 have hπloc_continuous : Continuous πloc := by

148 exact Continuous.subtype_mk

149 ((continuous_leftQuotientProjection

150 (K : Subgroup G) (H : Subgroup G) hKH).comp continuous_subtype_val)

151 (by

152 rintro ⟨x, hx⟩

153 rcases hx with ⟨g, hg, rfl⟩

154 exact ⟨g, hg, rfl⟩)

155 have hπloc_bij : Function.Bijective πloc := by

156 constructor

157 · intro x y hxy

158 rcases x with ⟨x, hx⟩

159 rcases y with ⟨y, hy⟩

160 rcases hx with ⟨gx, hgx, rfl⟩

161 rcases hy with ⟨gy, hgy, rfl⟩

162 apply Subtype.ext

163 apply QuotientGroup.eq.2

164 have hHmem : gx⁻¹ * gy ∈ (H : Subgroup G) := by

165 exact QuotientGroup.eq.1 (congrArg Subtype.val hxy)

166 have hVmem : gx⁻¹ * gy ∈ (V : Subgroup G) := by

167 exact (V : Subgroup G).mul_mem ((V : Subgroup G).inv_mem hgx) hgy

168 exact hVcapHK ⟨hVmem, hHmem⟩

169 · intro y

170 rcases y with ⟨y, hy⟩

171 rcases hy with ⟨g, hg, rfl⟩

172 refine ⟨⟨QuotientGroup.mk (s := (K : Subgroup G)) g, ⟨g, hg, rfl⟩⟩, ?_⟩

173 apply Subtype.ext

174 rfl

175 letI : CompactSpace WK := isCompact_iff_compactSpace.mp hWKcompact

176 let eTop : WK ≃ₜ BH :=

177 Continuous.homeoOfEquivCompactToT2

178 (f := Equiv.ofBijective πloc hπloc_bij) hπloc_continuous

179 let σB : BH → G ⧸ (K : Subgroup G) := fun y => (eTop.symm y).1

180 have hσB_continuous : Continuous σB := continuous_subtype_val.comp eTop.continuous_invFun

181 have hσB_right : ∀ y : BH,

182 leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH (σB y) = y.1 := by

183 intro y

184 exact congrArg Subtype.val (eTop.right_inv y)

185 have hσB_one :

186 σB ⟨QuotientGroup.mk (s := (H : Subgroup G)) (1 : G), ⟨1, V.one_mem', rfl⟩⟩ =

187 QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) := by

188 let y0 : BH :=

189 ⟨QuotientGroup.mk (s := (H : Subgroup G)) (1 : G), ⟨1, V.one_mem', rfl⟩⟩

190 have hσB_mem : σB y0 ∈ WK := (eTop.symm y0).2

191 have h1_mem : QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) ∈ WK := ⟨1, V.one_mem', rfl⟩

192 have hs : (⟨σB y0, hσB_mem⟩ : WK) =

193 ⟨QuotientGroup.mk (s := (K : Subgroup G)) (1 : G), h1_mem⟩ := by

194 apply hπloc_bij.1

195 apply Subtype.ext

196 simpa [πloc, y0] using hσB_right y0

197 exact congrArg Subtype.val hs

198 let c : G ⧸ (H : Subgroup G) → G ⧸ J :=

199 leftQuotientProjection (H : Subgroup G) J hHJ

200 have hc_continuous : Continuous c :=

201 continuous_leftQuotientProjection (H : Subgroup G) J hHJ

202 let r : G ⧸ (H : Subgroup G) → G := ρ ∘ c

203 have hr_continuous : Continuous r := hρcont.comp hc_continuous

204 let z : G ⧸ (H : Subgroup G) → BH := fun y =>

205 ⟨(r y)⁻¹ • y, by

206 rcases Quotient.exists_rep y with ⟨g, rfl⟩

207 change

208 QuotientGroup.mk (s := (H : Subgroup G))

209 ((r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g) ∈

210 BH

211 have hsame :

212 QuotientGroup.mk (s := J) (r (QuotientGroup.mk (s := (H : Subgroup G)) g)) =

213 QuotientGroup.mk (s := J) g := by

214 simpa [r, c, Function.comp] using

215 hρright (leftQuotientProjection (H : Subgroup G) J hHJ

216 (QuotientGroup.mk (s := (H : Subgroup G)) g))

217 have hmemJ :

218 (r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈ J := by

219 exact QuotientGroup.eq.1 hsame

220 have hmemJ' :

221 (r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈

222 (H : Subgroup G) ⊔ (V : Subgroup G) := by

223 simpa [J] using hmemJ

224 have hmemJ'' :

225 (r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈

226 (V : Subgroup G) ⊔ (H : Subgroup G) := by

227 simpa [sup_comm] using hmemJ'

228 have hmemSet :

229 (r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈

230 ((V : Subgroup G) : Set G) * ((H : Subgroup G) : Set G) := by

231 change (r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈

232 (((V : Subgroup G) ⊔ (H : Subgroup G) : Subgroup G) : Set G) at hmemJ''

233 rwa [Subgroup.normal_mul (V : Subgroup G) (H : Subgroup G)] at hmemJ''

234 rcases hmemSet with ⟨v, hv, h, hh, hEq⟩

235 refine ⟨v, hv, ?_⟩

236 rw [← hEq]

237 exact (QuotientGroup.mk_mul_of_mem v hh).symm⟩

238 have hz_continuous : Continuous z := by

239 exact Continuous.subtype_mk ((continuous_inv.comp hr_continuous).smul continuous_id) (by

240 intro y

241 exact (z y).2)

242 let σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G) := fun y =>

243 r y • σB (z y)

244 have hσ_continuous : Continuous σ := by

245 exact hr_continuous.smul (hσB_continuous.comp hz_continuous)

246 refine ⟨σ, hσ_continuous, ?_, ?_⟩

247 · intro y

248 calc

249 leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH (σ y)

250 = r y • leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH (σB (z y)) := by

251 simp only [leftQuotientProjection_smul, σ]

252 _ = r y • (z y).1 := by rw [hσB_right]

253 _ = y := by

254 change r y • ((r y)⁻¹ • y) = y

255 simp only [smul_smul, mul_inv_cancel, one_smul]

256 · have hc_one :

257 c (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =

258 QuotientGroup.mk (s := J) (1 : G) := rfl

259 have hr_one : r (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) = 1 := by

260 exact quotientOpenSubgroupSection_one J

261 have hz_one :

262 z (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =

263 ⟨QuotientGroup.mk (s := (H : Subgroup G)) (1 : G), ⟨1, V.one_mem', rfl⟩⟩ := by

264 apply Subtype.ext

265 simp only [hr_one, inv_one, one_smul, z]

266 simp only [hr_one, hz_one, hσB_one, one_smul, σ]

267

268end ProCGroups.ProC