ProCGroups/ProC/Quotients/OpenSubgroupSections.lean

1import Mathlib.Topology.Algebra.ProperAction.Basic

2import ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/ProCGroups/ProC/Quotients/OpenSubgroupSections.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

11-/

12/-!

13# Pro-C groups and open normal quotients

15Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.

16-/

18open Set

19open scoped Topology Pointwise

21namespace ProCGroups.ProC

23universe u v

25open InverseSystems

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

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

30is discrete, this section is automatically continuous. -/

31noncomputable def quotientOpenSubgroupSection (U : Subgroup G) :

32 (G ⧸ U) → G := by

33 classical

34 intro q

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

36 else Classical.choose (Quotient.exists_rep q)

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

39@[simp] theorem quotientOpenSubgroupSection_one

40 (U : Subgroup G) :

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

42 classical

43 simp only [quotientOpenSubgroupSection, ↓reduceDIte]

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

46theorem quotientOpenSubgroupSection_rightInverse

47 (U : Subgroup G) :

48 Function.RightInverse (quotientOpenSubgroupSection U)

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

50 classical

51 intro q

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

53 · subst hq

54 simp only [quotientOpenSubgroupSection, ↓reduceDIte]

55 · simpa [quotientOpenSubgroupSection, hq] using

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

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

59theorem continuous_quotientOpenSubgroupSection

60 [TopologicalSpace G]

61 [IsTopologicalGroup G]

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

63 Continuous (quotientOpenSubgroupSection U) := by

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

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

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

67 simpa using

68 (continuous_of_discreteTopology :

69 Continuous (quotientOpenSubgroupSection U))

71/-- Helper for the finite/open case : the canonical

72quotient map by an open normal subgroup of a profinite group admits a continuous section

73normalized by `σ(1) = 1`. The actual section data is provided by

74`quotientOpenSubgroupSection`. -/

75theorem quotient_openNormalSubgroup_hasContinuousSection

76 [TopologicalSpace G]

77 [IsTopologicalGroup G]

78 (U : OpenNormalSubgroup G) :

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

80 Continuous σ ∧

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

82 σ 1 = 1 := by

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

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

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

86 · simpa [QuotientGroup.mk'] using

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

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

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

91theorem leftQuotientProjection_hasContinuousSection_of_openSubgroup

92 [TopologicalSpace G]

93 [IsTopologicalGroup G]

94 (hG : IsProfiniteGroup G) (K H : ClosedSubgroup G)

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

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

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

98 Continuous σ ∧

99 Function.RightInverse σ

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

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

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

103 classical

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

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

106 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

107 letI : T2Space G := IsProfiniteGroup.t2Space hG

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

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

110 let UH : OpenSubgroup H :=

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

112 obtain ⟨V, hVHK⟩ :=

113 exists_openNormalSubgroup_inter_closedSubgroup_le (G := G) hG H UH

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

115 intro x hx

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

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

118 by simpa using hx.1

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

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

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

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

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

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

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

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

127 quotientOpenSubgroupSection_rightInverse J

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

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

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

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

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

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

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

135 openNormalSubgroup_isClosed (G := G) V

136 have hWKcompact : IsCompact WK := by

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

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

139 have hBHcompact : IsCompact BH := by

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

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

142 have hBHclosed : IsClosed BH := by

143 exact hBHcompact.isClosed

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

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

146 rcases x with ⟨x, hx⟩

147 rcases hx with ⟨g, hg, rfl⟩

148 exact ⟨g, hg, rfl⟩⟩

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

150 exact Continuous.subtype_mk

151 ((continuous_leftQuotientProjection

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

153 (by

154 rintro ⟨x, hx⟩

155 rcases hx with ⟨g, hg, rfl⟩

156 exact ⟨g, hg, rfl⟩)

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

158 constructor

159 · intro x y hxy

160 rcases x with ⟨x, hx⟩

161 rcases y with ⟨y, hy⟩

162 rcases hx with ⟨gx, hgx, rfl⟩

163 rcases hy with ⟨gy, hgy, rfl⟩

164 apply Subtype.ext

165 apply QuotientGroup.eq.2

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

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

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

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

170 exact hVcapHK ⟨hVmem, hHmem⟩

171 · intro y

172 rcases y with ⟨y, hy⟩

173 rcases hy with ⟨g, hg, rfl⟩

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

175 apply Subtype.ext

176 rfl

177 letI : CompactSpace WK := isCompact_iff_compactSpace.mp hWKcompact

178 let eTop : WK ≃ₜ BH := hπloc_continuous.homeoOfBijectiveCompactToT2 hπloc_bij

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