Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData
3/-!
4# Reidemeister Schreier / Discrete / Presentations / Tietze / Generator Map
6This module builds relator-quotient equivalences from maps on generators,
7including indexed relator families, and proves the normal-closure properties
8of the associated free-group pullback relators.
9-/
11universe u v w
13namespace ReidemeisterSchreier.Discrete.Presentations
15variable {G H K : Type*} [Group G] [Group H] [Group K]
17/--
18A group equivalence whose forward and inverse maps send relators into the opposite normal
19closures supplies mutual map data for the two relator quotients.
20-/
21def relatorQuotientMutualMapDataOfRelatorImagesMemNormalClosure
22 (e : G ≃* H) (R : Set G) (S : Set H)
23 (hR_to_S : ∀ r ∈ R, e r ∈ Subgroup.normalClosure S)
24 (hS_to_R : ∀ s ∈ S, e.symm s ∈ Subgroup.normalClosure R) :
25 RelatorQuotientMutualMapData R S :=
26 relatorQuotientMutualMapDataOfNormalClosureMapEq R S e
27 (map_normalClosure_eq_of_mulEquiv_relator_images_mem_normalClosure e R S hR_to_S hS_to_R)
29/--
30Compatible generator maps in both directions define mutual map data on the corresponding relator
31quotients.
32-/
33def relatorQuotientMutualMapDataOfGeneratorMaps
34 {X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
35 (toGenerator : X → FreeGroup Y)
36 (invGenerator : Y → FreeGroup X)
37 (hR :
38 ∀ r ∈ R,
39 FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)
40 (hS :
41 ∀ s ∈ S,
42 FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)
43 (hinv_to :
44 ∀ x : X,
45 RelatorEquivalent R
46 (FreeGroup.lift invGenerator (toGenerator x))
47 (FreeGroup.of x))
48 (hto_inv :
49 ∀ y : Y,
50 RelatorEquivalent S
51 (FreeGroup.lift toGenerator (invGenerator y))
52 (FreeGroup.of y)) :
53 RelatorQuotientMutualMapData R S where
54 toHom := FreeGroup.lift toGenerator
55 invHom := FreeGroup.lift invGenerator
56 mapsRelators := hR
57 mapsTargetRelators := hS
58 inv_toHom := by
59 intro w
60 let N : Subgroup (FreeGroup X) := Subgroup.normalClosure R
61 let F : FreeGroup X →* FreeGroup X ⧸ N :=
62 (QuotientGroup.mk' N).comp
63 ((FreeGroup.lift invGenerator).comp (FreeGroup.lift toGenerator))
64 have hhom : F = QuotientGroup.mk' N := by
65 ext x
66 dsimp [F]
67 simp only [FreeGroup.lift_apply_of]
68 rw [← relatorEquivalent_iff_eq_in_presentedQuotient]
69 exact hinv_to x
70 have hw := congrArg (fun f : FreeGroup X →* FreeGroup X ⧸ N => f w) hhom
71 change
72 ((FreeGroup.lift invGenerator
73 (FreeGroup.lift toGenerator w) : FreeGroup X) :
74 FreeGroup X ⧸ N) =
75 ((w : FreeGroup X) : FreeGroup X ⧸ N) at hw
76 exact (by
77 simpa [N, RelatorEquivalent] using
78 (relatorEquivalent_iff_eq_in_presentedQuotient.2 hw :
79 RelatorEquivalent R
80 (FreeGroup.lift invGenerator (FreeGroup.lift toGenerator w)) w))
81 to_invHom := by
82 intro w
83 let N : Subgroup (FreeGroup Y) := Subgroup.normalClosure S
84 let F : FreeGroup Y →* FreeGroup Y ⧸ N :=
85 (QuotientGroup.mk' N).comp
86 ((FreeGroup.lift toGenerator).comp (FreeGroup.lift invGenerator))
87 have hhom : F = QuotientGroup.mk' N := by
88 ext y
89 dsimp [F]
90 simp only [FreeGroup.lift_apply_of]
91 rw [← relatorEquivalent_iff_eq_in_presentedQuotient]
92 exact hto_inv y
93 have hw := congrArg (fun f : FreeGroup Y →* FreeGroup Y ⧸ N => f w) hhom
94 change
95 ((FreeGroup.lift toGenerator
96 (FreeGroup.lift invGenerator w) : FreeGroup Y) :
97 FreeGroup Y ⧸ N) =
98 ((w : FreeGroup Y) : FreeGroup Y ⧸ N) at hw
99 exact (by
100 simpa [N, RelatorEquivalent] using
101 (relatorEquivalent_iff_eq_in_presentedQuotient.2 hw :
102 RelatorEquivalent S
103 (FreeGroup.lift toGenerator (FreeGroup.lift invGenerator w)) w))
105/--
106Generator maps that preserve relators up to relator equivalence give mutual map data between
107relator quotients.
108-/
109def relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent
110 {X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
111 (toGenerator : X → FreeGroup Y)
112 (invGenerator : Y → FreeGroup X)
113 (hR :
114 ∀ r ∈ R,
115 RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)
116 (hS :
117 ∀ s ∈ S,
118 RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)
119 (hinv_to :
120 ∀ x : X,
121 RelatorEquivalent R
122 (FreeGroup.lift invGenerator (toGenerator x))
123 (FreeGroup.of x))
124 (hto_inv :
125 ∀ y : Y,
126 RelatorEquivalent S
127 (FreeGroup.lift toGenerator (invGenerator y))
128 (FreeGroup.of y)) :
129 RelatorQuotientMutualMapData R S :=
130 relatorQuotientMutualMapDataOfGeneratorMaps
131 toGenerator invGenerator
132 (fun r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR r hr))
133 (fun s hs => RelatorEquivalent.mem_normalClosure_of_eq_one (hS s hs))
134 hinv_to hto_inv
136/--
137Generator-map certificate for presentations whose relators are indexed families, with source and
138target relators checked one family at a time.
139-/
140def relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion
141 {X Y : Type*} {ι κ : Sort*}
142 {R : ι → Set (FreeGroup X)} {S : κ → Set (FreeGroup Y)}
143 (toGenerator : X → FreeGroup Y)
144 (invGenerator : Y → FreeGroup X)
145 (hR :
146 ∀ i : ι, ∀ r ∈ R i,
147 RelatorEquivalent (Set.iUnion S) (FreeGroup.lift toGenerator r) 1)
148 (hS :
149 ∀ k : κ, ∀ s ∈ S k,
150 RelatorEquivalent (Set.iUnion R) (FreeGroup.lift invGenerator s) 1)
151 (hinv_to :
152 ∀ x : X,
153 RelatorEquivalent (Set.iUnion R)
154 (FreeGroup.lift invGenerator (toGenerator x))
155 (FreeGroup.of x))
156 (hto_inv :
157 ∀ y : Y,
158 RelatorEquivalent (Set.iUnion S)
159 (FreeGroup.lift toGenerator (invGenerator y))
160 (FreeGroup.of y)) :
161 RelatorQuotientMutualMapData (Set.iUnion R) (Set.iUnion S) :=
162 relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent
163 toGenerator invGenerator
164 (by
165 intro r hr
166 rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
167 exact hR i r hi)
168 (by
169 intro s hs
170 rcases Set.mem_iUnion.1 hs with ⟨k, hk⟩
171 exact hS k s hk)
172 hinv_to hto_inv
174/--
175Generator maps that preserve doubly indexed relator families give mutual map data between the
176relator quotients.
177-/
178def relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent_iUnion₂
179 {X Y : Type*} {ι κ : Sort*} {α : ι → Sort*} {β : κ → Sort*}
180 {R : ∀ i : ι, α i → Set (FreeGroup X)}
181 {S : ∀ k : κ, β k → Set (FreeGroup Y)}
182 (toGenerator : X → FreeGroup Y)
183 (invGenerator : Y → FreeGroup X)
184 (hR :
185 ∀ i : ι, ∀ a : α i, ∀ r ∈ R i a,
186 RelatorEquivalent
187 (Set.iUnion fun k : κ => Set.iUnion (S k))
188 (FreeGroup.lift toGenerator r) 1)
189 (hS :
190 ∀ k : κ, ∀ b : β k, ∀ s ∈ S k b,
191 RelatorEquivalent
192 (Set.iUnion fun i : ι => Set.iUnion (R i))
193 (FreeGroup.lift invGenerator s) 1)
194 (hinv_to :
195 ∀ x : X,
196 RelatorEquivalent
197 (Set.iUnion fun i : ι => Set.iUnion (R i))
198 (FreeGroup.lift invGenerator (toGenerator x))
199 (FreeGroup.of x))
200 (hto_inv :
201 ∀ y : Y,
202 RelatorEquivalent
203 (Set.iUnion fun k : κ => Set.iUnion (S k))
204 (FreeGroup.lift toGenerator (invGenerator y))
205 (FreeGroup.of y)) :
206 RelatorQuotientMutualMapData
207 (Set.iUnion fun i : ι => Set.iUnion (R i))
208 (Set.iUnion fun k : κ => Set.iUnion (S k)) :=
209 relatorQuotientMutualMapDataOfGeneratorMapsRelatorEquivalent
210 toGenerator invGenerator
211 (by
212 intro r hr
213 rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
214 rcases Set.mem_iUnion.1 hi with ⟨a, ha⟩
215 exact hR i a r ha)
216 (by
217 intro s hs
218 rcases Set.mem_iUnion.1 hs with ⟨k, hk⟩
219 rcases Set.mem_iUnion.1 hk with ⟨b, hb⟩
220 exact hS k b s hb)
221 hinv_to hto_inv
223/-- Pull a relator set back along a free-group equivalence. -/
224def freeGroupPullbackRelatorSet
225 {Y : Type*} (e : FreeGroup Y ≃* G) (S : Set G) :
226 Set (FreeGroup Y) :=
227 e.symm '' S
229/-- Mapping the normal closure of the pulled-back relators recovers the original normal closure. -/
230theorem map_normalClosure_freeGroupPullbackRelatorSet
231 {Y : Type*} (e : FreeGroup Y ≃* G) (S : Set G) :
232 Subgroup.map e.toMonoidHom
233 (Subgroup.normalClosure (freeGroupPullbackRelatorSet e S)) =
234 Subgroup.normalClosure S := by
235 rw [Subgroup.map_normalClosure _ e.toMonoidHom e.surjective]
236 congr
237 ext z
238 constructor
239 · rintro ⟨y, ⟨s, hs, hy⟩, rfl⟩
240 simpa [← hy] using hs
241 · intro hz
242 exact ⟨e.symm z, ⟨z, hz, rfl⟩, by simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe,
243 MulEquiv.apply_symm_apply]⟩
245/--
246A free-group equivalence identifies the quotient by a relator set with the quotient by its
247pullback relator set.
248-/
249noncomputable def freeGroupPullbackRelatorQuotientEquiv
250 {Y : Type*} (e : FreeGroup Y ≃* G) (S : Set G) :
251 FreeGroup Y ⧸
252 Subgroup.normalClosure (freeGroupPullbackRelatorSet e S) ≃*
253 G ⧸ Subgroup.normalClosure S :=
254 QuotientGroup.congr
255 (Subgroup.normalClosure (freeGroupPullbackRelatorSet e S))
256 (Subgroup.normalClosure S)
257 e
258 (map_normalClosure_freeGroupPullbackRelatorSet e S)
260/-- Mutual relator-quotient map data induce an isomorphism of the corresponding quotients. -/
261noncomputable def quotientEquivOfRelatorQuotientMutualMapData
262 (R : Set G) (S : Set H)
263 (hData : RelatorQuotientMutualMapData R S) :
264 G ⧸ Subgroup.normalClosure R ≃* H ⧸ Subgroup.normalClosure S :=
265 quotientEquivOfRelatorsByMutualMaps R S
266 hData.toHom hData.invHom hData.mapsRelators hData.mapsTargetRelators
267 hData.inv_toHom hData.to_invHom
270end ReidemeisterSchreier.Discrete.Presentations