Yamaguchi Lean 4 Library
Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets
ProCGroups/ReidemeisterSchreier/Profinite/OpenSubgroups/FinitePermutationTargets/Source

Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets

1import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
3/-!
4# Reidemeister Schreier / Profinite / Open Subgroups / Finite Permutation Targets
6This module packages the finite permutation image of the coset action of an
7open subgroup, proves continuity of the action homomorphism, and transfers
8finite-group-class membership to the image.
9-/
11open Set
12open scoped Topology
14namespace ReidemeisterSchreier
15namespace Profinite
17universe u v
19section FinitePermutationTargets
21open ProCGroups.ProC
23/-- The actual permutation image of the finite coset action, before any universe lift. -/
24abbrev openSubgroupIndexActionImage
25 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
26 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) : Type :=
28 (G := G) (H : Subgroup G) H.isOpen'
29 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn).range
31/-- The actual finite permutation image belongs to the class across universes. -/
32theorem openSubgroupIndexContinuousHom_range_mem_class
33 {C : ProCGroups.FiniteGroupClass.{u}}
36 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
38 (H : OpenSubgroup G) {n : ℕ}
39 (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
40 C.MemAcrossUniverses (openSubgroupIndexActionImage (G := G) H hn) := by
41 let φ : G →ₜ* Equiv.Perm (Fin n) :=
43 H.isOpen' (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
44 let U : OpenNormalSubgroup G :=
45 { toOpenSubgroup :=
46 { toSubgroup := φ.toMonoidHom.ker
47 isOpen' := by
48 have h1open :
49 IsOpen ({1} : Set (Equiv.Perm (Fin n))) := isOpen_discrete _
50 change IsOpen (φ ⁻¹' ({1} : Set (Equiv.Perm (Fin n))))
51 exact h1open.preimage φ.continuous_toFun }
52 isNormal' := inferInstance }
53 have hQuotU : C (G ⧸ (U : Subgroup G)) :=
54 HasOpenNormalBasisInClass.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
55 hIso hQuot hG U
56 exact
57 (C.memAcrossUniverses_iff_of_mulEquiv
58 (QuotientGroup.quotientKerEquivRange φ.toMonoidHom)).1
59 (C.memAcrossUniverses_of_mem hQuotU)
61/-- Universe-lifted permutation image of the finite coset action attached to an open subgroup. -/
62abbrev openSubgroupIndexActionRange
63 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
64 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) : Type u :=
65 ULift.{u} (openSubgroupIndexActionImage (G := G) H hn)
67/--
68The finite permutation image is equipped with the discrete topology inherited from the finite
69permutation target.
70-/
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
77/-- The finite permutation image carries the discrete topology. -/
78instance openSubgroupIndexActionRange_discreteTopology
79 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
80 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
81 DiscreteTopology (openSubgroupIndexActionRange (G := G) H hn) :=
82 inferInstance
84/-- The finite permutation image is a topological group with its discrete topology. -/
85instance openSubgroupIndexActionRange_isTopologicalGroup
86 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
87 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
88 IsTopologicalGroup (openSubgroupIndexActionRange (G := G) H hn) :=
89 inferInstance
91/-- The permutation image of the open-subgroup coset action is finite. -/
92instance openSubgroupIndexActionRange_finite
93 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
94 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
95 Finite (openSubgroupIndexActionRange (G := G) H hn) :=
96 inferInstance
98/-- The finite coset-action homomorphism lifted to its universe-lifted permutation image. -/
99noncomputable def openSubgroupIndexActionRangeContinuousHom
100 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
101 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
102 G →ₜ* openSubgroupIndexActionRange (G := G) H hn := by
103 let φ : G →ₜ* Equiv.Perm (Fin n) :=
105 H.isOpen' (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
106 refine
107 { toMonoidHom :=
108 { toFun := fun g => ⟨⟨φ g, ⟨g, rfl⟩⟩⟩
109 map_one' := by
110 apply ULift.ext
111 apply Subtype.ext
112 simp only [map_one, ContinuousMonoidHom.coe_toMonoidHom, ULift.one_down,
113 OneMemClass.coe_one, φ]
114 map_mul' := by
115 intro g h
116 apply ULift.ext
117 apply Subtype.ext
118 change φ (g * h) = φ g * φ h
119 exact map_mul φ g h }
120 continuous_toFun := ?_ }
121 exact continuous_uliftUp.comp <|
122 Continuous.subtype_mk φ.continuous_toFun _
124/--
125The lifted permutation image acts on the finite coset index set through its underlying
126permutation.
127-/
128instance openSubgroupIndexActionRange_mulAction
129 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
130 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
131 MulAction (openSubgroupIndexActionRange (G := G) H hn) (Fin n) where
132 smul g i := g.down.1 i
133 one_smul i := by
134 rfl
135 mul_smul g h i := by
136 rfl
138/-- The lifted permutation image acts on a finite coset by applying the represented permutation. -/
139@[simp] theorem openSubgroupIndexActionRange_smul_apply
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 (g : openSubgroupIndexActionRange (G := G) H hn) (i : Fin n) :
143 g • i = g.down.1 i :=
144 rfl
146/-- The inverse transported permutation action of the coset-permutation image on the quotient. -/
147noncomputable def openSubgroupIndexActionRange_leftQuotient_smul
148 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
149 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
150 openSubgroupIndexActionRange (G := G) H hn →
151 (G ⧸ (H : Subgroup G)) → (G ⧸ (H : Subgroup G)) :=
152 fun g q =>
154 (G := G) (H : Subgroup G)
155 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
156 e.symm (g.down.1 (e q))
158/-- The finite permutation action evaluates on a coset by applying the represented group element. -/
159@[simp 900] theorem openSubgroupIndexActionRange_leftQuotientMulAction_apply
160 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
161 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n)
162 (g : openSubgroupIndexActionRange (G := G) H hn) (q : G ⧸ (H : Subgroup G)) :
164 (G := G) (H : Subgroup G)
165 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
166 e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn g q) = g.down.1 (e q) := by
167 simp only [openSubgroupIndexActionRange_leftQuotient_smul, ContinuousMonoidHom.coe_toMonoidHom,
168 Equiv.apply_symm_apply]
170/--
171The permutation image acts on the quotient by the inverse transported permutation, so that
172\(\rho(g)\) sends the basepoint coset to the coset of \(g\).
173-/
174noncomputable instance openSubgroupIndexActionRange_leftQuotientMulAction
175 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
176 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
177 MulAction (openSubgroupIndexActionRange (G := G) H hn) (G ⧸ (H : Subgroup G)) where
178 smul := openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn
179 one_smul q := by
181 (G := G) (H : Subgroup G)
182 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
183 apply e.injective
184 change e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn 1 q) = e q
185 simp only [openSubgroupIndexActionRange_leftQuotient_smul, ContinuousMonoidHom.coe_toMonoidHom,
186 ULift.one_down, OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq, Equiv.symm_apply_apply]
187 mul_smul g h q := by
189 (G := G) (H : Subgroup G)
190 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
191 apply e.injective
192 change
193 e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn (g * h) q) =
194 e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn g
195 (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn h q))
196 rw [openSubgroupIndexActionRange_leftQuotientMulAction_apply (G := G) H hn (g * h) q]
197 rw [openSubgroupIndexActionRange_leftQuotientMulAction_apply (G := G) H hn g]
198 rw [openSubgroupIndexActionRange_leftQuotientMulAction_apply (G := G) H hn h q]
199 rfl
201/--
202The induced action of the finite permutation image on the quotient by the open subgroup is
203continuous.
204-/
205instance openSubgroupIndexActionRange_leftQuotientContinuousSMul
206 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
207 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
208 ContinuousSMul (openSubgroupIndexActionRange (G := G) H hn) (G ⧸ (H : Subgroup G)) := by
209 letI : DiscreteTopology (G ⧸ (H : Subgroup G)) := inferInstance
210 exact ⟨continuous_of_discreteTopology⟩
212/-- The lifted finite permutation action sends the basepoint coset to the expected coset. -/
213@[simp 900] theorem openSubgroupIndexActionRangeContinuousHom_smul_basepoint
214 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
215 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) (g : G) :
216 openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •
217 (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
218 QuotientGroup.mk (s := (H : Subgroup G)) g := by
219 classical
221 (G := G) (H : Subgroup G)
222 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
223 let φ : G →* Equiv.Perm (Fin n) :=
225 (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
226 have hbase :
227 g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
228 QuotientGroup.mk (s := (H : Subgroup G)) g := by
229 change QuotientGroup.mk (s := (H : Subgroup G)) (g * 1) =
230 QuotientGroup.mk (s := (H : Subgroup G)) g
231 simp only [mul_one]
232 have haction :
233 openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •
234 (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
235 g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) := by
236 have himage :
237 e (openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •
238 (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) =
239 e (g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) := by
240 change
241 e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn
242 (openSubgroupIndexActionRangeContinuousHom (G := G) H hn g)
243 (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) =
244 e (g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)))
245 rw [openSubgroupIndexActionRange_leftQuotientMulAction_apply]
246 change φ g (e (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) =
247 e (g • (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)))
248 rw [show φ g = e.permCongr (MulAction.toPerm g) by
249 rfl]
250 rw [Equiv.permCongr_apply, e.symm_apply_apply]
251 rfl
252 exact e.injective himage
253 exact haction.trans hbase
255/--
256Under the subgroup-membership condition, the lifted finite permutation action fixes the
257basepoint coset as prescribed.
258-/
259@[simp] theorem openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem
260 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
261 (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n)
262 {g : G} (hg : g ∈ (H : Subgroup G)) :
263 openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •
264 (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
265 QuotientGroup.mk (s := (H : Subgroup G)) (1 : G) := by
266 rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint (G := G) H hn g]
267 simpa [QuotientGroup.eq] using hg
269/--
270The universe-lifted finite permutation image of an open-subgroup action belongs to the ambient
271finite-group class.
272-/
273theorem openSubgroupIndexActionRange_mem_class
274 {C : ProCGroups.FiniteGroupClass.{u}}
277 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
279 (H : OpenSubgroup G) {n : ℕ}
280 (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
281 C (openSubgroupIndexActionRange (G := G) H hn) := by
282 apply C.mem_of_memAcrossUniverses
283 exact
284 (C.memAcrossUniverses_ulift_iff
285 (openSubgroupIndexActionImage (G := G) H hn)).2
286 (openSubgroupIndexContinuousHom_range_mem_class
287 (C := C) hIso hQuot hG H hn)
289end FinitePermutationTargets
292end Profinite
293end ReidemeisterSchreier