Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Congruence
2import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Operations
4/-!
5# Reidemeister Schreier / Discrete / Presentations / Tietze / Relator Quotient Mutual Map Data
7This module packages mutually inverse maps between relator quotients. It
8provides reflexive, symmetric, and transitive composition together with a
9one-sided constructor when the inverse data can be derived.
10-/
12universe u v w
14namespace ReidemeisterSchreier.Discrete.Presentations
16variable {G H K : Type*} [Group G] [Group H] [Group K]
18/--
19Mutual homomorphisms respecting relators induce an isomorphism between the corresponding relator
20quotients.
21-/
22noncomputable def quotientEquivOfRelatorsByMutualMaps
23 (R : Set G) (S : Set H)
24 (f : G →* H) (g : H →* G)
25 (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
26 (hS : ∀ s ∈ S, g s ∈ Subgroup.normalClosure R)
27 (hgf : ∀ x : G, g (f x) * x⁻¹ ∈ Subgroup.normalClosure R)
28 (hfg : ∀ y : H, f (g y) * y⁻¹ ∈ Subgroup.normalClosure S) :
29 G ⧸ Subgroup.normalClosure R ≃* H ⧸ Subgroup.normalClosure S := by
30 let NR : Subgroup G := Subgroup.normalClosure R
31 let NS : Subgroup H := Subgroup.normalClosure S
32 have hfNR : NR ≤ Subgroup.comap f NS := by
33 exact Subgroup.normalClosure_le_normal hR
34 have hgNS : NS ≤ Subgroup.comap g NR := by
35 exact Subgroup.normalClosure_le_normal hS
36 let F : G ⧸ NR →* H ⧸ NS :=
37 QuotientGroup.lift NR ((QuotientGroup.mk' NS).comp f) (by
38 intro x hx
39 rw [MonoidHom.mem_ker]
40 exact (QuotientGroup.eq_one_iff (N := NS) (f x)).2 (hfNR hx))
41 let K : H ⧸ NS →* G ⧸ NR :=
42 QuotientGroup.lift NS ((QuotientGroup.mk' NR).comp g) (by
43 intro y hy
44 rw [MonoidHom.mem_ker]
45 exact (QuotientGroup.eq_one_iff (N := NR) (g y)).2 (hgNS hy))
46 refine
47 { toFun := F
48 invFun := K
49 left_inv := ?_
50 right_inv := ?_
51 map_mul' := fun a b => F.map_mul a b }
52 · intro x
53 rcases QuotientGroup.mk'_surjective NR x with ⟨x, rfl⟩
54 change K (F (QuotientGroup.mk' NR x)) = QuotientGroup.mk' NR x
55 simp only [QuotientGroup.mk'_apply]
56 exact (QuotientGroup.eq_iff_div_mem (N := NR) (x := g (f x)) (y := x)).2
57 (by simpa [NR, div_eq_mul_inv] using hgf x)
58 · intro y
59 rcases QuotientGroup.mk'_surjective NS y with ⟨y, rfl⟩
60 change F (K (QuotientGroup.mk' NS y)) = QuotientGroup.mk' NS y
61 simp only [QuotientGroup.mk'_apply]
62 exact (QuotientGroup.eq_iff_div_mem (N := NS) (x := f (g y)) (y := y)).2
63 (by simpa [NS, div_eq_mul_inv] using hfg y)
65/--
66Mutual relator-quotient map data records forward and inverse homomorphisms that are inverse
67modulo the two relator normal closures.
68-/
69structure RelatorQuotientMutualMapData
70 (R : Set G) (S : Set H) where
71 /-- The forward homomorphism from the source presentation group to the target one. -/
72 toHom : G →* H
73 /-- The homomorphism in the reverse direction. -/
74 invHom : H →* G
75 /-- The forward homomorphism sends each source relator into the target normal closure. -/
76 mapsRelators : ∀ r ∈ R, toHom r ∈ Subgroup.normalClosure S
77 /-- The reverse homomorphism sends each target relator into the source normal closure. -/
78 mapsTargetRelators : ∀ s ∈ S, invHom s ∈ Subgroup.normalClosure R
79 /-- The reverse-after-forward composite is the identity modulo the source relators. -/
80 inv_toHom : ∀ x : G, invHom (toHom x) * x⁻¹ ∈ Subgroup.normalClosure R
81 /-- The forward-after-reverse composite is the identity modulo the target relators. -/
82 to_invHom : ∀ y : H, toHom (invHom y) * y⁻¹ ∈ Subgroup.normalClosure S
84namespace RelatorQuotientMutualMapData
86variable {R : Set G} {S : Set H} {T : Set K}
88/-- The identity homomorphism gives reflexive mutual map data for a relator quotient. -/
89def refl (R : Set G) :
90 RelatorQuotientMutualMapData R R where
91 toHom := MonoidHom.id G
92 invHom := MonoidHom.id G
93 mapsRelators := by
94 intro r hr
95 exact Subgroup.subset_normalClosure hr
96 mapsTargetRelators := by
97 intro r hr
98 exact Subgroup.subset_normalClosure hr
99 inv_toHom := by
100 intro x
101 simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
102 to_invHom := by
103 intro x
104 simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
106/-- Swapping the forward and inverse homomorphisms gives the symmetric mutual map data. -/
107def symm
108 (D : RelatorQuotientMutualMapData R S) :
109 RelatorQuotientMutualMapData S R where
110 toHom := D.invHom
111 invHom := D.toHom
112 mapsRelators := D.mapsTargetRelators
113 mapsTargetRelators := D.mapsRelators
114 inv_toHom := D.to_invHom
115 to_invHom := D.inv_toHom
117/--
118Composing two pieces of mutual map data gives transitive mutual map data between relator
119quotients.
120-/
121def trans
122 (D₁ : RelatorQuotientMutualMapData R S)
123 (D₂ : RelatorQuotientMutualMapData S T) :
124 RelatorQuotientMutualMapData R T where
125 toHom := D₂.toHom.comp D₁.toHom
126 invHom := D₁.invHom.comp D₂.invHom
127 mapsRelators := by
128 intro r hr
129 exact map_mem_normalClosure_of_relators D₂.toHom D₂.mapsRelators
130 (D₁.mapsRelators r hr)
131 mapsTargetRelators := by
132 intro t ht
133 exact map_mem_normalClosure_of_relators D₁.invHom D₁.mapsTargetRelators
134 (D₂.mapsTargetRelators t ht)
135 inv_toHom := by
136 intro x
137 let y : H := D₁.toHom x
138 have h₂ :
139 D₂.invHom (D₂.toHom y) * y⁻¹ ∈ Subgroup.normalClosure S :=
140 D₂.inv_toHom y
141 have h₂map :
142 D₁.invHom (D₂.invHom (D₂.toHom y) * y⁻¹) ∈
143 Subgroup.normalClosure R :=
144 map_mem_normalClosure_of_relators D₁.invHom D₁.mapsTargetRelators h₂
145 have h₂map' :
146 D₁.invHom (D₂.invHom (D₂.toHom y)) *
147 (D₁.invHom y)⁻¹ ∈
148 Subgroup.normalClosure R := by
149 simpa using h₂map
150 have h₁ :
151 D₁.invHom y * x⁻¹ ∈ Subgroup.normalClosure R :=
152 D₁.inv_toHom x
153 have hprod := Subgroup.mul_mem (Subgroup.normalClosure R) h₂map' h₁
154 have hmul :
155 (D₁.invHom (D₂.invHom (D₂.toHom y)) *
156 (D₁.invHom y)⁻¹) *
157 (D₁.invHom y * x⁻¹) =
158 D₁.invHom (D₂.invHom (D₂.toHom y)) * x⁻¹ := by
159 group
160 simpa [MonoidHom.comp_apply, y, hmul] using hprod
161 to_invHom := by
162 intro z
163 let y : H := D₂.invHom z
164 have h₁ :
165 D₁.toHom (D₁.invHom y) * y⁻¹ ∈ Subgroup.normalClosure S :=
166 D₁.to_invHom y
167 have h₁map :
168 D₂.toHom (D₁.toHom (D₁.invHom y) * y⁻¹) ∈
169 Subgroup.normalClosure T :=
170 map_mem_normalClosure_of_relators D₂.toHom D₂.mapsRelators h₁
171 have h₁map' :
172 D₂.toHom (D₁.toHom (D₁.invHom y)) *
173 (D₂.toHom y)⁻¹ ∈
174 Subgroup.normalClosure T := by
175 simpa using h₁map
176 have h₂ :
177 D₂.toHom y * z⁻¹ ∈ Subgroup.normalClosure T :=
178 D₂.to_invHom z
179 have hprod := Subgroup.mul_mem (Subgroup.normalClosure T) h₁map' h₂
180 have hmul :
181 (D₂.toHom (D₁.toHom (D₁.invHom y)) *
182 (D₂.toHom y)⁻¹) *
183 (D₂.toHom y * z⁻¹) =
184 D₂.toHom (D₁.toHom (D₁.invHom y)) * z⁻¹ := by
185 group
186 simpa [MonoidHom.comp_apply, y, hmul] using hprod
188end RelatorQuotientMutualMapData
190/-- Equal normal closures provide mutual relator-quotient map data using the identity maps. -/
191def relatorQuotientMutualMapDataOfNormalClosureEq
192 {R S : Set G}
193 (h : Subgroup.normalClosure R = Subgroup.normalClosure S) :
194 RelatorQuotientMutualMapData R S where
195 toHom := MonoidHom.id G
196 invHom := MonoidHom.id G
197 mapsRelators := by
198 intro r hr
199 rw [← h]
200 exact Subgroup.subset_normalClosure hr
201 mapsTargetRelators := by
202 intro s hs
203 rw [h]
204 exact Subgroup.subset_normalClosure hs
205 inv_toHom := by
206 intro x
207 simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
208 to_invHom := by
209 intro x
210 simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
212/-- Relator-equivalent defining relators give mutual map data between the relator quotients. -/
213def relatorQuotientMutualMapDataOfRelatorEquivalent
214 {R S : Set G}
215 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
216 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
217 RelatorQuotientMutualMapData R S :=
218 relatorQuotientMutualMapDataOfNormalClosureEq
219 (normalClosure_eq_of_relatorEquivalent hR_to_S hS_to_R)
221/--
222A multiplicative equivalence carrying one normal closure to the other provides mutual
223relator-quotient map data.
224-/
225def relatorQuotientMutualMapDataOfNormalClosureMapEq
226 (R : Set G) (S : Set H) (e : G ≃* H)
227 (hmap :
228 Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) =
229 Subgroup.normalClosure S) :
230 RelatorQuotientMutualMapData R S where
231 toHom := e.toMonoidHom
232 invHom := e.symm.toMonoidHom
233 mapsRelators := by
234 intro r hr
235 have hrmap : e r ∈ Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) :=
236 ⟨r, Subgroup.subset_normalClosure hr, rfl⟩
237 rw [← hmap]
238 exact hrmap
239 mapsTargetRelators := by
240 intro s hs
241 have hsmap : s ∈ Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) := by
242 rw [hmap]
243 exact Subgroup.subset_normalClosure hs
244 rcases hsmap with ⟨r, hr, hrs⟩
245 simpa [← hrs] using hr
246 inv_toHom := by
247 intro x
248 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulEquiv.symm_apply_apply,
249 mul_inv_cancel, one_mem]
250 to_invHom := by
251 intro y
252 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulEquiv.apply_symm_apply,
253 mul_inv_cancel, one_mem]
255/--
256A multiplicative equivalence identifies normal closures when the images of relators in both
257directions lie in the corresponding normal closures.
258-/
259theorem map_normalClosure_eq_of_mulEquiv_relator_images_mem_normalClosure
260 (e : G ≃* H) (R : Set G) (S : Set H)
261 (hR_to_S : ∀ r ∈ R, e r ∈ Subgroup.normalClosure S)
262 (hS_to_R : ∀ s ∈ S, e.symm s ∈ Subgroup.normalClosure R) :
263 Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) =
264 Subgroup.normalClosure S := by
265 apply le_antisymm
266 · rw [Subgroup.map_normalClosure _ e.toMonoidHom e.surjective]
267 refine Subgroup.normalClosure_le_normal ?_
268 rintro z ⟨r, hr, rfl⟩
269 exact hR_to_S r hr
270 · rw [Subgroup.map_normalClosure _ e.toMonoidHom e.surjective]
271 refine Subgroup.normalClosure_le_normal ?_
272 intro s hs
273 have hsmap : s ∈ Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) :=
274 ⟨e.symm s, hS_to_R s hs, by simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe,
275 MulEquiv.apply_symm_apply]⟩
276 rwa [Subgroup.map_normalClosure _ e.toMonoidHom e.surjective] at hsmap
279end ReidemeisterSchreier.Discrete.Presentations