ReidemeisterSchreier/Profinite/OpenSubgroups/FinitePermutationTargets.lean

1import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/FinitePermutationTargets.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Profinite open-subgroup Schreier theory

14Profinite open subgroup quotients, finite permutation targets, dense free models, exact right Schreier generation, and topological rank bounds.

15-/

17open Set

18open scoped Topology

20namespace ReidemeisterSchreier

21namespace Profinite

23universe u v

25section FinitePermutationTargets

27open ProCGroups.ProC

29/-- The finite permutation representation attached to an open subgroup of a concrete pro-`C`

30group has image in `C`. We package the image using `ULift` so it can live in the same universe as

31the ambient finite-group class. -/

32theorem openSubgroupIndexContinuousHom_range_mem_class

33 {C : ProCGroups.FiniteGroupClass.{u}}

34 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)

35 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)

36 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

37 (hG : ProCGroups.ProC.IsProCGroup C G)

38 (H : OpenSubgroup G) {n : ℕ}

39 (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

40 C

41 (ULift

42 ((ProCGroups.FiniteGeneration.openSubgroupIndexContinuousHom

43 (G := G) (H : Subgroup G) H.isOpen'

44 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn).range)) := by

45 let φ : G →ₜ* Equiv.Perm (Fin n) :=

46 ProCGroups.FiniteGeneration.openSubgroupIndexContinuousHom (G := G) (H : Subgroup G)

47 H.isOpen' (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn

48 let U : OpenNormalSubgroup G :=

49 { toOpenSubgroup :=

50 { toSubgroup := φ.toMonoidHom.ker

51 isOpen' := by

52 have h1open :

53 IsOpen ({1} : Set (Equiv.Perm (Fin n))) := isOpen_discrete _

54 simpa [Set.preimage, MonoidHom.mem_ker] using h1open.preimage φ.continuous_toFun }

55 isNormal' := inferInstance }

56 have hQuotU : C (G ⧸ (U : Subgroup G)) :=

57 ProCGroups.ProC.IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed

58 hIso hQuot hG U

59 exact hIso

60 ⟨(QuotientGroup.quotientKerEquivRange φ.toMonoidHom).trans MulEquiv.ulift.symm⟩

61 hQuotU

63/-- Universe-lifted permutation image of the finite coset action attached to an open subgroup. -/

64abbrev openSubgroupIndexActionRange

65 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

66 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) : Type u :=

67 ULift

68 ((ProCGroups.FiniteGeneration.openSubgroupIndexContinuousHom (G := G) (H : Subgroup G)

69 H.isOpen' (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn).range)

71instance openSubgroupIndexActionRange_topologicalSpace

72 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

73 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

74 TopologicalSpace (openSubgroupIndexActionRange (G := G) H hn) :=

75 inferInstance

77instance openSubgroupIndexActionRange_discreteTopology

78 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

79 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

80 DiscreteTopology (openSubgroupIndexActionRange (G := G) H hn) :=

81 inferInstance

83instance openSubgroupIndexActionRange_isTopologicalGroup

84 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

85 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

86 IsTopologicalGroup (openSubgroupIndexActionRange (G := G) H hn) :=

87 inferInstance

89instance openSubgroupIndexActionRange_finite

90 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

91 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

92 Finite (openSubgroupIndexActionRange (G := G) H hn) :=

93 inferInstance

95/-- The finite coset-action homomorphism lifted to its image. -/

96noncomputable def openSubgroupIndexActionRangeContinuousHom

97 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

98 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

99 G →ₜ* openSubgroupIndexActionRange (G := G) H hn := by

100 let φ : G →ₜ* Equiv.Perm (Fin n) :=

101 ProCGroups.FiniteGeneration.openSubgroupIndexContinuousHom (G := G) (H : Subgroup G)

102 H.isOpen' (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn

103 refine

104 { toMonoidHom :=

105 { toFun := fun g => ⟨⟨φ g, ⟨g, rfl⟩⟩⟩

106 map_one' := by

107 apply ULift.ext

108 apply Subtype.ext

109 simp only [map_one, ContinuousMonoidHom.coe_toMonoidHom, ULift.one_down, OneMemClass.coe_one, φ]

110 map_mul' := by

111 intro g h

112 apply ULift.ext

113 apply Subtype.ext

114 simp only [map_mul, ContinuousMonoidHom.coe_toMonoidHom, ULift.mul_down, Subgroup.coe_mul]}

115 continuous_toFun := ?_ }

116 exact continuous_uliftUp.comp <|

117 Continuous.subtype_mk φ.continuous_toFun _

118

119/-- The lifted permutation image acts on the chosen finite coset index set through the underlying

120permutation. -/

121instance openSubgroupIndexActionRange_mulAction

122 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

123 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

124 MulAction (openSubgroupIndexActionRange (G := G) H hn) (Fin n) where

125 smul g i := g.down.1 i

126 one_smul i := by

127 rfl

128 mul_smul g h i := by

129 rfl

130

131@[simp] theorem openSubgroupIndexActionRange_smul_apply

132 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

133 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n)

134 (g : openSubgroupIndexActionRange (G := G) H hn) (i : Fin n) :

135 g • i = g.down.1 i :=

136 rfl

137

138/-- The inverse transported permutation action of the coset-permutation image on the quotient. -/

139noncomputable def openSubgroupIndexActionRange_leftQuotient_smul

140 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

141 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

142 openSubgroupIndexActionRange (G := G) H hn →

143 (G ⧸ (H : Subgroup G)) → (G ⧸ (H : Subgroup G)) :=

144 fun g q =>

145 let e := ProCGroups.FiniteGeneration.openSubgroupIndexEquiv

146 (G := G) (H : Subgroup G)

147 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn

148 e.symm (g.down.1 (e q))

149

150@[simp 900] theorem openSubgroupIndexActionRange_leftQuotientMulAction_apply

151 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

152 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n)

153 (g : openSubgroupIndexActionRange (G := G) H hn) (q : G ⧸ (H : Subgroup G)) :

154 let e := ProCGroups.FiniteGeneration.openSubgroupIndexEquiv

155 (G := G) (H : Subgroup G)

156 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn

157 e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn g q) = g.down.1 (e q) := by

158 simp only [openSubgroupIndexActionRange_leftQuotient_smul, ContinuousMonoidHom.coe_toMonoidHom,

159 Equiv.apply_symm_apply]

160

161/-- The permutation image acts on the quotient by the inverse transported permutation, so that

162`ρ(g)` sends the basepoint coset to the coset of `g`. -/

163noncomputable instance openSubgroupIndexActionRange_leftQuotientMulAction

164 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

165 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

166 MulAction (openSubgroupIndexActionRange (G := G) H hn) (G ⧸ (H : Subgroup G)) where

167 smul := openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn

168 one_smul q := by

169 let e := ProCGroups.FiniteGeneration.openSubgroupIndexEquiv

170 (G := G) (H : Subgroup G)

171 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn

172 apply e.injective

173 change e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn 1 q) = e q

174 simp only [openSubgroupIndexActionRange_leftQuotient_smul, ContinuousMonoidHom.coe_toMonoidHom,

175 ULift.one_down, OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq, Equiv.symm_apply_apply]

176 mul_smul g h q := by

177 let e := ProCGroups.FiniteGeneration.openSubgroupIndexEquiv

178 (G := G) (H : Subgroup G)

179 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn

180 apply e.injective

181 change

182 e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn (g * h) q) =

183 e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn g

184 (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn h q))

185 simp only [openSubgroupIndexActionRange_leftQuotient_smul, ContinuousMonoidHom.coe_toMonoidHom,

186 ULift.mul_down, Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply, Equiv.apply_symm_apply]

187

188instance openSubgroupIndexActionRange_leftQuotientContinuousSMul

189 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

190 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

191 ContinuousSMul (openSubgroupIndexActionRange (G := G) H hn) (G ⧸ (H : Subgroup G)) := by

192 letI : DiscreteTopology (G ⧸ (H : Subgroup G)) := inferInstance

193 exact ⟨continuous_of_discreteTopology⟩

194

195@[simp 900] theorem openSubgroupIndexActionRangeContinuousHom_smul_basepoint

196 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

197 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) (g : G) :

198 openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •

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

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

201 classical

202 let e := ProCGroups.FiniteGeneration.openSubgroupIndexEquiv

203 (G := G) (H : Subgroup G)

204 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn

205 let φ : G →* Equiv.Perm (Fin n) :=

206 ProCGroups.FiniteGeneration.openSubgroupIndexAction (G := G) (H : Subgroup G)

207 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn

208 have hbase :

209 g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =

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

211 change QuotientGroup.mk (s := (H : Subgroup G)) (g * 1) =

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

213 simp only [mul_one]

214 have haction :

215 openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •

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

217 g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) := by

218 have himage :

219 e (openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •

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

221 e (g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) := by

222 change

223 e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn

224 (openSubgroupIndexActionRangeContinuousHom (G := G) H hn g)

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

226 e (g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)))

227 rw [openSubgroupIndexActionRange_leftQuotientMulAction_apply]

228 change φ g (e (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) =

229 e (g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)))

230 rw [show φ g = e.permCongr (MulAction.toPerm g) by

231 rfl]

232 rw [Equiv.permCongr_apply, e.symm_apply_apply]

233 rfl

234 exact e.injective himage

235 exact haction.trans hbase

236

237@[simp] theorem openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem

238 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

239 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n)

240 {g : G} (hg : g ∈ (H : Subgroup G)) :

241 openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •

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

243 QuotientGroup.mk (s := (H : Subgroup G)) (1 : G) := by

244 rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint (G := G) H hn g]

245 simpa [QuotientGroup.eq] using hg

246

247/-- The universe-lifted finite permutation image of an open subgroup action still belongs to the

248ambient finite-group class. -/

249theorem openSubgroupIndexActionRange_mem_class

250 {C : ProCGroups.FiniteGroupClass.{u}}

251 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)

252 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)

253 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

254 (hG : ProCGroups.ProC.IsProCGroup C G)

255 (H : OpenSubgroup G) {n : ℕ}

256 (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :

257 C (openSubgroupIndexActionRange (G := G) H hn) :=

258 openSubgroupIndexContinuousHom_range_mem_class

259 (C := C) hIso hQuot hG H hn

260

261end FinitePermutationTargets

262

263

264end Profinite

265end ReidemeisterSchreier