Source: ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.ClassicalGeneratorBasis
1import ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis
3/-!
4# Reidemeister Schreier / Discrete / Open Subgroups / Classical Generator Basis
6This module identifies the classical Schreier generators with the free basis
7obtained from complement edges, including the inverse-basis convention needed
8for the standard generator formula.
9-/
11namespace ReidemeisterSchreier.Discrete.OpenSubgroups
13section ClassicalGeneratorBasis
15namespace Internal
17/--
18There is an inverse-valued Schreier-basis equivalence sending the standard free generator
19represented by \(z\) to \(z^{-1}\) in the subgroup; the positive-valued compatibility theorem is
20exposed separately.
21-/
22private theorem IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv
23 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
24 (hT : IsRightSchreierTransversal (X := X) L T) :
25 ∃ e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L,
26 ∀ z : ↥(schreierGeneratorSet (X := X) hT),
27 e (FreeGroup.of z) = (z : L)⁻¹ := by
28 classical
29 letI := schreierTransversalRightCosetAction (X := X) hT
30 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
31 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
32 let C :
33 Set (Quiver.Total
34 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))) :=
35 ((Quiver.wideSubquiverEquivSetTotal <|
36 Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT))ᶜ : Set _)
37 let b : FreeGroupBasis ↑C L :=
38 (ReidemeisterSchreier.Groupoid.endBasis (schreierPrefixTree (X := X) hT)).map
39 (schreierRootEndMulEquiv (X := X) hT)
40 let toSch : ↑C → ↥(schreierGeneratorSet (X := X) hT) := fun i =>
41 ⟨schreierGenerator (X := X) hT (((i.1.left.back : T) : FreeGroup X)) i.1.hom.1,
42 by
43 refine ⟨
44 ((i.1.left.back : T) : FreeGroup X), (i.1.left.back : T).property,
45 i.1.hom.1, rfl, ?_⟩
46 intro hgen
47 exact i.2 (show i.1 ∈ Quiver.wideSubquiverEquivSetTotal
48 (Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)) from
49 schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT i.1.hom hgen)⟩
50 have hval : ∀ i : ↑C, (b i : L) =
51 (((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := by
52 intro i
53 rw [FreeGroupBasis.map_apply, ReidemeisterSchreier.Groupoid.endBasis_apply]
54 have htree : ∀ {a b : IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)}
55 (e : a ⟶ b),
56 e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b →
57 (schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) = (1 : L) := by
58 intro a b e he
59 exact schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
60 have hloop := ReidemeisterSchreier.Groupoid.map_loopOfHom_eq_map
61 (T := schreierPrefixTree (X := X) hT)
62 (F := schreierLabelFunctor (X := X) hT)
63 (hTree := by
64 intro a b e he
65 exact htree e he)
66 (q := IsFreeGroupoid.of i.1.hom)
67 let loop := ReidemeisterSchreier.Groupoid.rootLoopOfHom (schreierPrefixTree (X := X) hT)
68 (IsFreeGroupoid.of i.1.hom)
69 have hrootEq : (schreierRootEndMulEquiv (X := X) hT loop : L) =
70 (schreierLabelFunctor (X := X) hT).map loop := by
71 apply Subtype.ext
72 change loop.1 = (1 : FreeGroup X) * loop.1 * (1 : FreeGroup X)⁻¹
73 simp only [one_mul, inv_one, mul_one]
74 exact hrootEq.trans <| hloop.trans <| schreierLabelFunctor_map_of (X := X) hT i.1.hom
75 have hto_inj : Function.Injective toSch := by
76 intro i j hij
77 apply b.injective
78 have hz : ((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L) =
79 ((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L) := congrArg Subtype.val hij
80 have hz_inv : (((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) =
81 (((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := congrArg Inv.inv hz
82 exact (hval i).trans (hz_inv.trans (hval j).symm)
83 have hto_surj : Function.Surjective toSch := by
84 intro z
85 rcases z.2 with ⟨t, ht, x, hz, hne⟩
86 let a : CategoryTheory.ActionCategory (FreeGroup X) T :=
87 ((⟨t, ht⟩ : T) : CategoryTheory.ActionCategory (FreeGroup X) T)
88 let b0 : CategoryTheory.ActionCategory (FreeGroup X) T :=
89 (schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T)
90 let e :
91 (show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from
92 a) ⟶ b0 :=
93 ⟨x, by
94 rw [FreeGroup.inverseBasis_apply]
95 change (FreeGroup.of x)⁻¹ • (show T from CategoryTheory.ActionCategory.back a) =
96 (show T from CategoryTheory.ActionCategory.back b0)
97 simpa [a, b0] using
98 (schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ (⟨t, ht⟩ : T))⟩
99 have he_not : ⟨a, b0, e⟩ ∈ C := by
100 change ¬ e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b0
101 intro he
102 have hgen1_inv :
103 (schreierGenerator (X := X) hT
104 ((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1)⁻¹ = 1 := by
105 have htreeLabel :=
106 schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
107 rw [schreierLabelFunctor_map_of (X := X) hT e] at htreeLabel
108 exact htreeLabel
109 have hgen1 :
110 schreierGenerator (X := X) hT
111 ((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1 = 1 :=
112 inv_eq_one.mp hgen1_inv
113 exact hne (by simpa [a, e, hz] using hgen1)
114 refine ⟨⟨⟨a, b0, e⟩, he_not⟩, ?_⟩
115 apply Subtype.ext
116 simpa [toSch, a, e] using hz.symm
117 let eC : ↑C ≃ ↥(schreierGeneratorSet (X := X) hT) := Equiv.ofBijective toSch ⟨hto_inj, hto_surj⟩
118 refine ⟨(b.reindex eC).repr.symm, ?_⟩
119 intro z
120 have hbasis :
121 (b.reindex eC).repr.symm (FreeGroup.of z) = (b.reindex eC) z := by
122 apply (b.reindex eC).repr.injective
123 calc
124 (b.reindex eC).repr ((b.reindex eC).repr.symm (FreeGroup.of z))
125 = FreeGroup.of z := by simp only [MulEquiv.apply_symm_apply]
126 _ = (b.reindex eC).repr ((b.reindex eC) z) :=
127 (FreeGroupBasis.repr_apply_coe (b.reindex eC) z).symm
128 calc
129 (b.reindex eC).repr.symm (FreeGroup.of z)
130 = (b.reindex eC) z := hbasis
131 _ = b (eC.symm z) := by
132 rw [FreeGroupBasis.reindex_apply]
133 _ = (((toSch (eC.symm z) : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) :=
134 hval (eC.symm z)
135 _ = (z : L)⁻¹ := by
136 exact congrArg (fun w : ↥(schreierGeneratorSet (X := X) hT) => ((w : L)⁻¹))
137 (eC.apply_symm_apply z)
139end Internal
141/--
142Positive-valued Schreier-basis existence statement on the classical Schreier generator set. It
143is equivalent to the nontrivial Schreier-pair basis equivalence used in the main formulation.
144-/
145theorem IsRightSchreierTransversal.exists_schreierBasisEquiv
146 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
147 (hT : IsRightSchreierTransversal (X := X) L T) :
148 ∃ e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L,
149 ∀ z : ↥(schreierGeneratorSet (X := X) hT),
150 e (FreeGroup.of z) = (z : L) := by
151 classical
152 rcases Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT with
153 ⟨eInverse, hInverse⟩
154 let e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L :=
155 (FreeGroup.generatorInversionEquiv ↥(schreierGeneratorSet (X := X) hT)).trans eInverse
156 refine ⟨e, ?_⟩
157 intro z
158 dsimp [e]
159 calc
160 eInverse ((FreeGroup.of z)⁻¹) = (eInverse (FreeGroup.of z))⁻¹ := by simp only [map_inv]
161 _ = ((z : L)⁻¹)⁻¹ := by rw [hInverse z]
162 _ = (z : L) := inv_inv _
164/--
165The inverse-valued free-group equivalence on the classical Schreier generator value set is
166equivalent to the nontrivial Schreier-pair basis equivalence used in the main formulation.
167-/
168noncomputable def schreierGeneratorInverseBasisEquiv
169 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
170 (hT : IsRightSchreierTransversal (X := X) L T) :
171 FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L :=
172 Classical.choose (Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT)
174/--
175The inverse-valued classical generator-set equivalence sends a free generator to the inverse of
176the represented Schreier generator.
177-/
178theorem schreierGeneratorInverseBasisEquiv_of
179 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
180 (hT : IsRightSchreierTransversal (X := X) L T)
181 (z : ↥(schreierGeneratorSet (X := X) hT)) :
182 schreierGeneratorInverseBasisEquiv (X := X) hT (FreeGroup.of z) = (z : L)⁻¹ :=
183 Classical.choose_spec (Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT) z
185end ClassicalGeneratorBasis
187end ReidemeisterSchreier.Discrete.OpenSubgroups