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

Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.SchreierTransversals

1import ProCGroups.FreeProC.Basic
2import ProCGroups.WreathProducts
3import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.RightQuotient
5/-!
6# Schreier sections and oriented cocycles
8The source of truth is `SchreierCocycleData`: it stores a left/right
9orientation, a section map, the next-coset operation, and the proof that the
10resulting cocycle lands in the open subgroup. `ActualSchreierSection` and
11`ActualRightSchreierSection` add equivalences with the genuine quotient and the
12projection/next-coset coherence laws. `FiniteSchreierCocycleData` carries the
13finiteness evidence used by `Nat.card`.
15The concrete left- and right-coset constructions below feed this common API.
16Continuity, closure, generation, and cardinality are proved once for the
17oriented data rather than repeated as chosen-left/chosen-right wrapper
18families.
19-/
21open Set
22open scoped Topology Pointwise
24namespace ReidemeisterSchreier
25namespace Profinite
27open ProCGroups
28open ProCGroups.ProC
29open ProCGroups.FreeProC
30open ProCGroups.WreathProducts
32universe u v
34section LeftQuotientSections
36variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
38/-- The normalized continuous section of the left quotient by an open subgroup. -/
39noncomputable abbrev openSubgroupLeftSchreierSection (H : OpenSubgroup F) :
40 F ⧸ (H : Subgroup F) → F :=
43omit [IsTopologicalGroup F] in
44/--
45The normalized section of the left quotient is a right inverse to the quotient projection.
46-/
47theorem openSubgroupLeftSchreierSection_rightInverse (H : OpenSubgroup F) :
48 Function.RightInverse (openSubgroupLeftSchreierSection (F := F) H)
49 (QuotientGroup.mk (s := (H : Subgroup F))) := by
50 simpa [openSubgroupLeftSchreierSection] using
52 (G := F) (U := (H : Subgroup F)))
54/-- The corresponding Schreier section is continuous. -/
55theorem continuous_openSubgroupLeftSchreierSection (H : OpenSubgroup F) :
56 Continuous (openSubgroupLeftSchreierSection (F := F) H) := by
57 simpa [openSubgroupLeftSchreierSection] using
59 (G := F) (U := (H : Subgroup F)) H.isOpen')
61omit [IsTopologicalGroup F] in
62/-- The Schreier generator component of the corresponding rewriting map. -/
63@[simp] theorem openSubgroupLeftSchreierSection_mk
64 (H : OpenSubgroup F) (q : F ⧸ (H : Subgroup F)) :
65 QuotientGroup.mk (s := (H : Subgroup F))
66 (openSubgroupLeftSchreierSection (F := F) H q) = q :=
67 openSubgroupLeftSchreierSection_rightInverse (F := F) H q
69omit [IsTopologicalGroup F] in
70/-- The normalized left-quotient section sends the identity coset to the identity. -/
71@[simp] theorem openSubgroupLeftSchreierSection_one
72 (H : OpenSubgroup F) :
73 openSubgroupLeftSchreierSection (F := F) H
74 (QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)) = 1 := by
75 simp only [openSubgroupLeftSchreierSection, quotientOpenSubgroupSection_one]
77end LeftQuotientSections
79section AbstractSchreierSections
81variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
82variable {X : Type v}
83variable (H : OpenSubgroup F)
85/-- The two cocycle orientations used by left- and right-coset Schreier generators. -/
86inductive SchreierOrientation where
87 /-- The left-oriented cocycle places the inverse of the next representative first. -/
88 | left
89 /-- The right-oriented cocycle places the inverse of the next representative last. -/
90 | right
91deriving DecidableEq
93namespace SchreierOrientation
95/-- The oriented Schreier cocycle associated to a section and a next-coset operation. -/
96def cocycle {Q : Type u} (o : SchreierOrientation)
97 (sec : Q → F) (next : Q → X → Q) (ι : X → F) (q : Q) (x : X) : F :=
98 match o with
99 | left => (sec (next q x))⁻¹ * sec q * ι x
100 | right => sec q * ι x * (sec (next q x))⁻¹
102end SchreierOrientation
104/--
105A section-level Schreier generator package. It abstracts over the quotient type, the left/right
106cocycle orientation, and the next-coset operation, so the common generator-set, continuity,
107closure, and cardinality formulation can be formulated once.
108-/
109structure SchreierCocycleData where
110 /-- The abstract type indexing the chosen coset representatives. -/
111 Q : Type u
112 /-- Whether the associated Schreier cocycle uses the left- or right-coset formula. -/
113 orientation : SchreierOrientation
114 /-- The representative in \(F\) assigned to each abstract quotient index. -/
115 sectionMap : Q → F
116 /-- The quotient index reached after multiplying a representative by a chosen generator. -/
117 next : (X → F) → Q → X → Q
118 /-- Every oriented cocycle value belongs to the open subgroup \(H\). -/
119 cocycle_mem :
120 ∀ (ι : X → F) (q : Q) (x : X),
121 orientation.cocycle sectionMap (next ι) ι q x ∈ (H : Subgroup F)
123/-- Genuine left-quotient Schreier section data.
125The equivalence identifies the abstract cocycle index with the actual quotient
126`F ⧸ H`; the remaining fields state that both the representative and the
127next-coset operation project to that quotient. Thus no arbitrary raw map can
128masquerade as a quotient projection. -/
129structure ActualSchreierSection where
130 /-- The abstract cocycle and section data. -/
131 cocycleData : SchreierCocycleData (F := F) (X := X) H
132 /-- Identification of the abstract index type with the left quotient \(F/H\). -/
133 quotientEquiv : cocycleData.Q ≃ F ⧸ (H : Subgroup F)
134 /-- Each chosen representative projects to its corresponding quotient index. -/
135 section_projects :
136 ∀ q : cocycleData.Q,
137 QuotientGroup.mk (s := (H : Subgroup F)) (cocycleData.sectionMap q) =
138 quotientEquiv q
139 /-- The next-index operation projects the representative multiplied by the chosen generator. -/
140 next_projects :
141 ∀ (ι : X → F) (q : cocycleData.Q) (x : X),
142 quotientEquiv (cocycleData.next ι q x) =
143 QuotientGroup.mk (s := (H : Subgroup F))
144 (cocycleData.sectionMap q * ι x)
146/-- Genuine right-quotient Schreier section data.
148This is the right-coset counterpart of `ActualSchreierSection`; its index type
149is explicitly identified with `OpenSubgroupRightQuotient H`. -/
150structure ActualRightSchreierSection where
151 /-- The abstract cocycle and section data. -/
152 cocycleData : SchreierCocycleData (F := F) (X := X) H
153 /-- Identification of the abstract index type with the right quotient by \(H\). -/
154 quotientEquiv : cocycleData.Q ≃ OpenSubgroupRightQuotient H
155 /-- Each chosen representative maps to its corresponding right-quotient index. -/
156 section_projects :
157 ∀ q : cocycleData.Q,
158 (Quotient.mk'' (cocycleData.sectionMap q) :
159 OpenSubgroupRightQuotient H) = quotientEquiv q
160 /-- The next-index operation maps the representative multiplied by the chosen generator. -/
161 next_projects :
162 ∀ (ι : X → F) (q : cocycleData.Q) (x : X),
163 quotientEquiv (cocycleData.next ι q x) =
164 (Quotient.mk'' (cocycleData.sectionMap q * ι x) :
165 OpenSubgroupRightQuotient H)
167/-- A cocycle package together with the finiteness data required by its
168`Nat.card` estimates. This prevents a finite-index formula from silently
169using `Nat.card = 0` on an infinite quotient. -/
170structure FiniteSchreierCocycleData where
171 /-- The underlying abstract Schreier cocycle package. -/
172 cocycleData : SchreierCocycleData (F := F) (X := X) H
173 /-- Finiteness of the generator-index type. -/
174 finiteGeneratorIndex : Finite X
175 /-- Finiteness of the abstract quotient-index type. -/
176 finiteQuotient : Finite cocycleData.Q
178namespace SchreierCocycleData
180variable {H}
182/-- The subgroup-valued generator attached to an abstract Schreier section. -/
183noncomputable def generator (S : SchreierCocycleData (F := F) (X := X) H)
184 (ι : X → F) (q : S.Q) (x : X) : ↥(H : Subgroup F) :=
185 ⟨S.orientation.cocycle S.sectionMap (S.next ι) ι q x, S.cocycle_mem ι q x⟩
187omit [IsTopologicalGroup F] in
188/-- Forgetting the subgroup proof from a Schreier generator yields its defining cocycle
189value. -/
190@[simp] theorem generator_coe (S : SchreierCocycleData (F := F) (X := X) H)
191 (ι : X → F) (q : S.Q) (x : X) :
192 ((S.generator ι q x : ↥(H : Subgroup F)) : F) =
193 S.orientation.cocycle S.sectionMap (S.next ι) ι q x :=
194 rfl
196/-- Nontrivial generator values of an abstract Schreier section. -/
197def generatorSet (S : SchreierCocycleData (F := F) (X := X) H)
198 (ι : X → F) : Set ↥(H : Subgroup F) :=
199 {z | ∃ q : S.Q, ∃ x : X, z = S.generator ι q x ∧ z ≠ 1}
201/--
202This type records the nontrivial Schreier pairs whose cocycle values form the abstract Schreier
203generator set.
204-/
205def NontrivialPairs (S : SchreierCocycleData (F := F) (X := X) H)
206 (ι : X → F) : Type (max u v) :=
207 {p : S.Q × X // S.generator ι p.1 p.2 ≠ 1}
209omit [IsTopologicalGroup F] in
210/--
211The abstract Schreier generator or next-coset formula is obtained by evaluating the chosen
212section cocycle.
213-/
214instance finite_nontrivialPairs
215 (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F)
216 [Finite X] [Finite S.Q] :
217 Finite (S.NontrivialPairs ι) :=
218 Finite.of_injective (fun p : S.NontrivialPairs ι => p.1) (by
219 intro a b h
220 exact Subtype.ext h)
222omit [IsTopologicalGroup F] in
223/-- The tautological map from nontrivial abstract Schreier pairs to the generator value set. -/
224noncomputable def nontrivialPairsToGeneratorSet
225 (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F) :
226 S.NontrivialPairs ι → ↥(S.generatorSet ι) := fun p =>
227 ⟨S.generator ι p.1.1 p.1.2, ⟨p.1.1, p.1.2, rfl, p.2⟩⟩
229omit [IsTopologicalGroup F] in
230/--
231The map from nontrivial abstract Schreier pairs onto the abstract Schreier generator set is
232surjective.
233-/
234theorem surjective_nontrivialPairsToGeneratorSet
235 (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F) :
236 Function.Surjective (S.nontrivialPairsToGeneratorSet ι) := by
237 intro z
238 rcases z.2 with ⟨q, x, hz, hz_ne⟩
239 refine ⟨⟨(q, x), ?_⟩, ?_⟩
240 · simpa [hz] using hz_ne
241 · apply Subtype.ext
242 exact hz.symm
244omit [IsTopologicalGroup F] in
245/--
246Surjectivity of the map from nontrivial Schreier pairs bounds the cardinality of the abstract
247Schreier generator set by the number of nontrivial pairs.
248-/
249theorem natCard_generatorSet_le_nontrivialPairs
250 (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F)
251 [Finite X] [Finite S.Q] :
252 Nat.card (S.generatorSet ι) ≤ Nat.card (S.NontrivialPairs ι) :=
253 Nat.card_le_card_of_surjective (S.nontrivialPairsToGeneratorSet ι)
254 (S.surjective_nontrivialPairsToGeneratorSet ι)
256omit [IsTopologicalGroup F] in
257/--
258The number of nontrivial abstract Schreier pairs is bounded by the corresponding finite
259coset-generator product.
260-/
261theorem natCard_nontrivialPairs_le
262 (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F)
263 [Finite X] [Finite S.Q] :
264 Nat.card (S.NontrivialPairs ι) ≤ Nat.card S.Q * Nat.card X := by
265 have hle : Nat.card (S.NontrivialPairs ι) ≤ Nat.card (S.Q × X) :=
266 Nat.card_le_card_of_injective (fun p : S.NontrivialPairs ι => p.1) (by
267 intro a b h
268 exact Subtype.ext h)
269 simpa [Nat.card_prod] using hle
271omit [IsTopologicalGroup F] in
272/-- The Schreier generator set has cardinality at most the number of quotient cosets times the
273number of original generators. -/
274theorem natCard_generatorSet_le
275 (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F)
276 [Finite X] [Finite S.Q] :
277 Nat.card (S.generatorSet ι) ≤ Nat.card S.Q * Nat.card X :=
278 (S.natCard_generatorSet_le_nontrivialPairs ι).trans (S.natCard_nontrivialPairs_le ι)
280omit [IsTopologicalGroup F] in
281/--
282The subgroup closure of the abstract Schreier generator set is the closure of the corresponding
283generator-map range.
284-/
285theorem subgroupClosure_generatorSet_eq_closure_range
286 (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F) :
287 Subgroup.closure (S.generatorSet ι) =
288 Subgroup.closure (Set.range fun p : S.Q × X => S.generator ι p.1 p.2) := by
289 simpa [generatorSet] using
291 (G := ↥(H : Subgroup F))
292 (fun p : S.Q × X => S.generator ι p.1 p.2))
294/--
295The Schreier generator family topologically generates precisely when the corresponding
296subgroup-generation condition holds.
297-/
298theorem topologicallyGenerates_generatorSet_iff
299 {S : SchreierCocycleData (F := F) (X := X) H} {ι : X → F} :
301 (S.generatorSet ι) ↔
303 (Set.range fun p : S.Q × X => S.generator ι p.1 p.2) := by
306 S.subgroupClosure_generatorSet_eq_closure_range ι]
308omit [IsTopologicalGroup F] in
309/--
310It characterizes exactly when generator identity with the unit equivalence left is equal to the
311unit for the chosen Schreier transversal and induced coset representatives.
312-/
313theorem generator_eq_one_iff_left
314 {S : SchreierCocycleData (F := F) (X := X) H}
315 (hleft : S.orientation = SchreierOrientation.left)
316 {ι : X → F} {q : S.Q} {x : X} :
317 S.generator ι q x = 1 ↔ S.sectionMap (S.next ι q x) = S.sectionMap q * ι x := by
318 constructor
319 · intro h
320 have hval := congrArg Subtype.val h
321 change S.orientation.cocycle S.sectionMap (S.next ι) ι q x = 1 at hval
322 exact inv_mul_eq_one.mp (by
323 simpa [SchreierOrientation.cocycle, hleft, mul_assoc] using hval)
324 · intro hrep
325 apply Subtype.ext
326 simp only [generator, SchreierOrientation.cocycle, hleft, hrep, mul_inv_rev, mul_assoc,
327 inv_mul_cancel,
328 mul_one, OneMemClass.coe_one]
330omit [IsTopologicalGroup F] in
331/--
332The right Schreier generator is trivial exactly in the corresponding unit-representative case.
333-/
334theorem generator_eq_one_iff_right
335 {S : SchreierCocycleData (F := F) (X := X) H}
336 (hright : S.orientation = SchreierOrientation.right)
337 {ι : X → F} {q : S.Q} {x : X} :
338 S.generator ι q x = 1 ↔ S.sectionMap (S.next ι q x) = S.sectionMap q * ι x := by
339 constructor
340 · intro h
341 have hval := congrArg Subtype.val h
342 change S.orientation.cocycle S.sectionMap (S.next ι) ι q x = 1 at hval
343 exact (mul_inv_eq_one.mp
344 (by simpa [SchreierOrientation.cocycle, hright, mul_assoc] using hval)).symm
345 · intro hrep
346 apply Subtype.ext
347 simp only [generator, SchreierOrientation.cocycle, hright, hrep, mul_inv_rev, mul_assoc,
348 mul_inv_cancel_left,
349 mul_inv_cancel, OneMemClass.coe_one]
351omit [IsTopologicalGroup F] in
352/--
353The rewritten Reidemeister--Schreier generator evaluates to the identity when the next section
354value is the basepoint.
355-/
356theorem generator_eq_of_section_next_eq_one
357 (S : SchreierCocycleData (F := F) (X := X) H)
358 (ι : X → F) (q : S.Q) (x : X)
359 (hnext : S.sectionMap (S.next ι q x) = 1)
360 (hmem : S.sectionMap q * ι x ∈ (H : Subgroup F)) :
361 S.generator ι q x = ⟨S.sectionMap q * ι x, hmem⟩ := by
362 apply Subtype.ext
363 cases hside : S.orientation with
364 | left =>
365 simp only [generator, SchreierOrientation.cocycle, hside, hnext, inv_one, one_mul]
366 | right =>
367 simp only [generator, SchreierOrientation.cocycle, hside, hnext, inv_one, mul_one]
369/--
370The abstract Schreier section generator is the cocycle value determined by the chosen section
371and next coset.
372-/
373theorem continuous_generator
374 (S : SchreierCocycleData (F := F) (X := X) H)
375 [TopologicalSpace S.Q] [TopologicalSpace X]
376 (ι : X → F)
377 (hsection : Continuous S.sectionMap)
378 (hnext : Continuous (fun p : S.Q × X => S.next ι p.1 p.2))
379 (hι : Continuous ι) :
380 Continuous (fun p : S.Q × X => S.generator ι p.1 p.2) := by
381 refine Continuous.subtype_mk ?_ ?_
382 cases hside : S.orientation with
383 | left =>
384 have hcont :
385 Continuous (fun p : S.Q × X =>
386 (S.sectionMap (S.next ι p.1 p.2))⁻¹ * (S.sectionMap p.1 * ι p.2)) :=
387 ((hsection.comp hnext).inv).mul
388 ((hsection.comp continuous_fst).mul (hι.comp continuous_snd))
389 simpa [generator, SchreierOrientation.cocycle, hside, mul_assoc] using hcont
390 | right =>
391 have hcont :
392 Continuous (fun p : S.Q × X =>
393 (S.sectionMap p.1 * ι p.2) * (S.sectionMap (S.next ι p.1 p.2))⁻¹) :=
394 ((hsection.comp continuous_fst).mul (hι.comp continuous_snd)).mul
395 ((hsection.comp hnext).inv)
396 simpa [generator, SchreierOrientation.cocycle, hside, mul_assoc] using hcont
398end SchreierCocycleData
400namespace FiniteSchreierCocycleData
402omit [IsTopologicalGroup F] in
403/-- The generator-cardinality bound with all finiteness evidence carried by the
404data object rather than repeated as ambient typeclass assumptions. -/
405theorem natCard_generatorSet_le
406 (S : FiniteSchreierCocycleData (F := F) (X := X) H) (ι : X → F) :
407 Nat.card (S.cocycleData.generatorSet ι) ≤
408 Nat.card S.cocycleData.Q * Nat.card X := by
409 letI : Finite X := S.finiteGeneratorIndex
410 letI : Finite S.cocycleData.Q := S.finiteQuotient
411 exact S.cocycleData.natCard_generatorSet_le ι
413end FiniteSchreierCocycleData
415end AbstractSchreierSections
417section LeftSchreierGenerators
419variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
420variable (H : OpenSubgroup F)
421variable {X : Type v}
422variable (σ : F ⧸ (H : Subgroup F) → F)
423variable (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
424variable (ι : X → F)
426/-- The next left coset obtained from a chosen representative and a generator. -/
427def leftSchreierNextCoset (q : F ⧸ (H : Subgroup F)) (x : X) : F ⧸ (H : Subgroup F) :=
428 QuotientGroup.mk (s := (H : Subgroup F)) (σ q * ι x)
430/-- Left-coset Schreier generator attached to a section of the quotient by an open subgroup. -/
431noncomputable def leftSchreierGenerator
432 (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
433 (q : F ⧸ (H : Subgroup F)) (x : X) :
434 ↥(H : Subgroup F) := by
435 let qx := leftSchreierNextCoset (F := F) H σ ι q x
436 refine ⟨SchreierOrientation.left.cocycle σ
437 (leftSchreierNextCoset (F := F) H σ ι) ι q x, ?_⟩
438 have hqx :
439 QuotientGroup.mk (s := (H : Subgroup F)) (σ qx) =
440 QuotientGroup.mk (s := (H : Subgroup F)) (σ q * ι x) := by
441 simpa [qx, leftSchreierNextCoset] using hσ qx
442 simpa [SchreierOrientation.cocycle, mul_assoc] using (QuotientGroup.eq.1 hqx)
444/-- The left-coset Schreier data as an instance of the abstract section formulation. -/
445noncomputable def leftSchreierSection :
446 SchreierCocycleData (F := F) (X := X) H where
447 Q := F ⧸ (H : Subgroup F)
448 orientation := SchreierOrientation.left
449 sectionMap := σ
450 next := fun ι q x => leftSchreierNextCoset (F := F) H σ ι q x
451 cocycle_mem := by
452 intro ι q x
453 exact (leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x).property
455/-- The left quotient construction with its projection, section law, and
456next-coset coherence retained in the type. -/
457noncomputable def actualLeftSchreierSection :
458 ActualSchreierSection (F := F) (X := X) H where
459 cocycleData := leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ)
460 quotientEquiv := Equiv.refl _
461 section_projects := hσ
462 next_projects := by
463 intro ι q x
464 rfl
466omit [IsTopologicalGroup F] in
467/--
468The left Schreier section generator is the cocycle value determined by the chosen section and
469next coset.
470-/
471@[simp] theorem leftSchreierSection_generator
472 (q : F ⧸ (H : Subgroup F)) (x : X) :
473 (leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
474 SchreierCocycleData (F := F) (X := X) H).generator ι q x =
475 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x := by
476 apply Subtype.ext
477 rfl
479end LeftSchreierGenerators
481section RightSchreierGenerators
483variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
484variable (H : OpenSubgroup F)
485variable {X : Type v}
486variable (τ : OpenSubgroupRightQuotient H → F)
487variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
488variable (ι : X → F)
490/-- The right quotient by an open subgroup carries the natural multiplication action. -/
491instance instMulActionOpenSubgroupRightQuotient :
492 MulAction F (OpenSubgroupRightQuotient H) :=
493 rightCosetMulAction (H : Subgroup F)
495/--
496The next right Schreier coset is obtained by acting on the current right coset by the inverse of
497the chosen generator image.
498-/
499def rightSchreierNextCoset (q : OpenSubgroupRightQuotient H) (x : X) :
500 OpenSubgroupRightQuotient H :=
501 (ι x)⁻¹ • q
503/--
504The Schreier generator formula records the element determined by the chosen representative
505associated to the chosen transversal and letter.
506-/
507noncomputable def rightSchreierGenerator (q : OpenSubgroupRightQuotient H) (x : X) :
508 ↥(H : Subgroup F) :=
509 rightQuotientSectionCocycle (H := (H : Subgroup F)) τ hτ (ι x) q
511/-- The right-coset Schreier data as an instance of the abstract section formulation. -/
512@[reducible] noncomputable def rightSchreierSection :
513 SchreierCocycleData (F := F) (X := X) H where
514 Q := OpenSubgroupRightQuotient H
515 orientation := SchreierOrientation.right
516 sectionMap := τ
517 next := fun ι q x => rightSchreierNextCoset (F := F) H ι q x
518 cocycle_mem := by
519 intro ι q x
520 exact (rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x).property
522/-- The right quotient construction with its projection, section law, and
523next-coset coherence retained in the type. -/
524noncomputable def actualRightSchreierSection :
525 ActualRightSchreierSection (F := F) (X := X) H where
526 cocycleData := rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ)
527 quotientEquiv := Equiv.refl _
528 section_projects := hτ
529 next_projects := by
530 change ∀ (ι : X → F) (q : OpenSubgroupRightQuotient H) (x : X),
531 rightSchreierNextCoset (F := F) H ι q x = Quotient.mk'' (τ q * ι x)
532 intro ι q x
533 calc
534 (ι x)⁻¹ • q =
535 (ι x)⁻¹ • (Quotient.mk'' (τ q) : OpenSubgroupRightQuotient H) := by
536 rw [hτ q]
537 _ = Quotient.mk'' (τ q * ι x) := by
538 rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F))]
540omit [IsTopologicalGroup F] in
541/--
542The right Schreier section generator is the cocycle value determined by the chosen section and
543next coset.
544-/
545@[simp] theorem rightSchreierSection_generator
546 (q : OpenSubgroupRightQuotient H) (x : X) :
547 (rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
548 SchreierCocycleData (F := F) (X := X) H).generator ι q x =
549 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x := by
550 apply Subtype.ext
551 rfl
553omit [IsTopologicalGroup F] in
554/-- The right Schreier generator evaluates to the identity in the target subgroup presentation. -/
555theorem rightSchreierGenerator_eq_one
556 {q : OpenSubgroupRightQuotient H} {x : X}
557 (hx : ι x = 1) :
558 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x = 1 := by
559 apply Subtype.ext
560 simp only [rightSchreierGenerator, rightQuotientSectionCocycle, hx, mul_one, inv_one, one_smul,
561 mul_inv_cancel, OneMemClass.coe_one]
563section Topological
565variable [TopologicalSpace X]
566variable [TopologicalSpace (OpenSubgroupRightQuotient H)]
567variable [DiscreteTopology (OpenSubgroupRightQuotient H)]
569/-- The corresponding Schreier next-coset map is continuous. -/
570theorem continuous_rightSchreierNextCoset
571 (hιcont : Continuous ι) :
572 Continuous (fun p : OpenSubgroupRightQuotient H × X =>
573 rightSchreierNextCoset (F := F) H ι p.1 p.2) := by
574 letI : MulAction F (OpenSubgroupRightQuotient H) :=
575 rightCosetMulAction (H : Subgroup F)
576 refine (continuous_prod_of_discrete_left).2 ?_
577 intro q
578 have hqcont :
579 Continuous fun x : X => ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H) := by
580 rw [continuous_discrete_rng]
581 intro q'
582 classical
583 let a : F := q.out
584 let b : F := q'.out
585 have hpre :
586 (fun x : X => ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H)) ⁻¹' ({q'} :
587 Set (OpenSubgroupRightQuotient H)) =
588 (fun x : X => b * (ι x)⁻¹ * a⁻¹) ⁻¹' ((H : Subgroup F) : Set F) := by
589 ext x
590 constructor
591 · intro hx
592 have hEq :
593 (Quotient.mk'' (a * ι x) : OpenSubgroupRightQuotient H) = Quotient.mk'' b := by
594 calc
595 (Quotient.mk'' (a * ι x) : OpenSubgroupRightQuotient H)
596 = (ι x)⁻¹ • (Quotient.mk'' a : OpenSubgroupRightQuotient H) := by
597 rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) (ι x) a]
598 _ = (ι x)⁻¹ • q := by rw [Quotient.out_eq' q]
599 _ = q' := hx
600 _ = Quotient.mk'' b := (Quotient.out_eq' q').symm
601 have hrel :
602 QuotientGroup.rightRel (H : Subgroup F) (a * ι x) b := Quotient.eq''.mp hEq
603 simpa [a, b, mul_inv_rev, mul_assoc] using (QuotientGroup.rightRel_apply.mp hrel)
604 · intro hx
605 change b * (ι x)⁻¹ * a⁻¹ ∈ (H : Subgroup F) at hx
606 have hrel :
607 QuotientGroup.rightRel (H : Subgroup F) (a * ι x) b := by
608 rw [QuotientGroup.rightRel_apply]
609 simpa only [a, b, mul_inv_rev, mul_assoc] using hx
610 calc
611 ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H)
612 = (ι x)⁻¹ • (Quotient.mk'' a : OpenSubgroupRightQuotient H) := by
613 rw [Quotient.out_eq' q]
614 _ = Quotient.mk'' (a * ι x) := by
615 rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) (ι x) a]
616 _ = Quotient.mk'' b := Quotient.eq''.mpr hrel
617 _ = q' := Quotient.out_eq' q'
618 rw [show
619 (fun x : X => ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H)) ⁻¹' ({q'} :
620 Set (OpenSubgroupRightQuotient H)) =
621 (fun x : X => b * (ι x)⁻¹ * a⁻¹) ⁻¹' ((H : Subgroup F) : Set F) by
622 simpa using hpre]
623 exact H.isOpen'.preimage ((continuous_const.mul (hιcont.inv)).mul continuous_const)
624 simpa [rightSchreierNextCoset] using hqcont
626/-- The corresponding Schreier generator map is continuous. -/
627theorem continuous_rightSchreierGenerator
628 (hτcont : Continuous τ) (hιcont : Continuous ι) :
629 Continuous (fun p : OpenSubgroupRightQuotient H × X =>
630 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2) := by
631 letI : TopologicalSpace
632 (rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
633 SchreierCocycleData (F := F) (X := X) H).Q :=
634 inferInstanceAs (TopologicalSpace (OpenSubgroupRightQuotient H))
635 simpa using
636 ((rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
637 SchreierCocycleData (F := F) (X := X) H).continuous_generator
638 ι hτcont
639 (continuous_rightSchreierNextCoset (F := F) (H := H) (ι := ι) hιcont)
640 hιcont)
642end Topological
645omit [IsTopologicalGroup F] in
646/--
647The basepoint projection induced by a wreath-product homomorphism evaluates a right Schreier
648generator by the corresponding left coordinate.
649-/
650theorem rightQuotientBasepointProjectionHom_rightSchreierGenerator
651 {A : Type*} [Group A]
652 (ψ : F →* PermutationalWreathProduct A (OpenSubgroupRightQuotient H) F)
653 (hψ :
654 (SemidirectProduct.rightHom :
655 PermutationalWreathProduct A (OpenSubgroupRightQuotient H) F →* F).comp ψ =
656 MonoidHom.id F)
657 (hτpure :
658 ∀ q : OpenSubgroupRightQuotient H,
659 wreathLeftCoordinate ψ
660 (openSubgroupRightCoset H (1 : F)) (τ q) = 1)
661 (q : OpenSubgroupRightQuotient H) (x : X) :
662 rightQuotientBasepointProjectionHom (H : Subgroup F) ψ hψ
663 (rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x) =
664 wreathLeftCoordinate ψ q (ι x) := by
665 exact rightQuotientBasepointProjectionHom_apply_cocycle
666 (H : Subgroup F) τ hτ ψ hψ hτpure (ι x) q
668end RightSchreierGenerators
670end Profinite
671end ReidemeisterSchreier