ReidemeisterSchreier/Discrete/Presentations/Tietze/RelatorQuotientMutualMapData.lean
1import ReidemeisterSchreier.Discrete.Presentations.Relators
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Tietze/RelatorQuotientMutualMapData.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Tietze transformations
14Presentation-level Tietze moves for adding and deleting generators, replacing relators, comparing quotient presentations, and recording executable Tietze scripts.
15-/
17universe u v w
19/-!
20# Elementary Tietze infrastructure
22This file packages the "mutual maps modulo relators" pattern as reusable
23discrete Tietze infrastructure. It intentionally stays at the normal-closure
24level; downstream-specific simplification sequences live downstream.
25-/
27namespace ReidemeisterSchreier.Discrete.Presentations
29variable {G H K : Type*} [Group G] [Group H] [Group K]
31noncomputable def quotientEquivOfRelatorsByMutualMaps
32 (R : Set G) (S : Set H)
33 (f : G →* H) (g : H →* G)
34 (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
35 (hS : ∀ s ∈ S, g s ∈ Subgroup.normalClosure R)
36 (hgf : ∀ x : G, g (f x) * x⁻¹ ∈ Subgroup.normalClosure R)
37 (hfg : ∀ y : H, f (g y) * y⁻¹ ∈ Subgroup.normalClosure S) :
38 G ⧸ Subgroup.normalClosure R ≃* H ⧸ Subgroup.normalClosure S := by
39 let NR : Subgroup G := Subgroup.normalClosure R
40 let NS : Subgroup H := Subgroup.normalClosure S
41 have hfNR : NR ≤ Subgroup.comap f NS := by
42 exact Subgroup.normalClosure_le_normal hR
43 have hgNS : NS ≤ Subgroup.comap g NR := by
44 exact Subgroup.normalClosure_le_normal hS
45 let F : G ⧸ NR →* H ⧸ NS :=
46 QuotientGroup.lift NR ((QuotientGroup.mk' NS).comp f) (by
47 intro x hx
48 rw [MonoidHom.mem_ker]
49 exact (QuotientGroup.eq_one_iff (N := NS) (f x)).2 (hfNR hx))
50 let K : H ⧸ NS →* G ⧸ NR :=
51 QuotientGroup.lift NS ((QuotientGroup.mk' NR).comp g) (by
52 intro y hy
53 rw [MonoidHom.mem_ker]
54 exact (QuotientGroup.eq_one_iff (N := NR) (g y)).2 (hgNS hy))
55 refine
56 { toFun := F
57 invFun := K
58 left_inv := ?_
59 right_inv := ?_
60 map_mul' := fun a b => F.map_mul a b }
61 · intro x
62 rcases QuotientGroup.mk'_surjective NR x with ⟨x, rfl⟩
63 change K (F (QuotientGroup.mk' NR x)) = QuotientGroup.mk' NR x
64 simp only [QuotientGroup.mk'_apply]
65 exact (QuotientGroup.eq_iff_div_mem (N := NR) (x := g (f x)) (y := x)).2
66 (by simpa [NR, div_eq_mul_inv] using hgf x)
67 · intro y
68 rcases QuotientGroup.mk'_surjective NS y with ⟨y, rfl⟩
69 change F (K (QuotientGroup.mk' NS y)) = QuotientGroup.mk' NS y
70 simp only [QuotientGroup.mk'_apply]
71 exact (QuotientGroup.eq_iff_div_mem (N := NS) (x := f (g y)) (y := y)).2
72 (by simpa [NS, div_eq_mul_inv] using hfg y)
74structure RelatorQuotientMutualMapData
75 (R : Set G) (S : Set H) where
76 toHom : G →* H
77 invHom : H →* G
78 mapsRelators : ∀ r ∈ R, toHom r ∈ Subgroup.normalClosure S
79 mapsTargetRelators : ∀ s ∈ S, invHom s ∈ Subgroup.normalClosure R
80 inv_toHom : ∀ x : G, invHom (toHom x) * x⁻¹ ∈ Subgroup.normalClosure R
81 to_invHom : ∀ y : H, toHom (invHom y) * y⁻¹ ∈ Subgroup.normalClosure S
83namespace RelatorQuotientMutualMapData
85variable {R : Set G} {S : Set H} {T : Set K}
87def refl (R : Set G) :
88 RelatorQuotientMutualMapData R R where
89 toHom := MonoidHom.id G
90 invHom := MonoidHom.id G
91 mapsRelators := by
92 intro r hr
93 exact Subgroup.subset_normalClosure hr
94 mapsTargetRelators := by
95 intro r hr
96 exact Subgroup.subset_normalClosure hr
97 inv_toHom := by
98 intro x
99 simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
100 to_invHom := by
101 intro x
102 simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
104def symm
105 (D : RelatorQuotientMutualMapData R S) :
106 RelatorQuotientMutualMapData S R where
107 toHom := D.invHom
108 invHom := D.toHom
109 mapsRelators := D.mapsTargetRelators
110 mapsTargetRelators := D.mapsRelators
111 inv_toHom := D.to_invHom
112 to_invHom := D.inv_toHom
114def trans
115 (D₁ : RelatorQuotientMutualMapData R S)
116 (D₂ : RelatorQuotientMutualMapData S T) :
117 RelatorQuotientMutualMapData R T where
118 toHom := D₂.toHom.comp D₁.toHom
119 invHom := D₁.invHom.comp D₂.invHom
120 mapsRelators := by
121 intro r hr
122 exact map_mem_normalClosure_of_relators D₂.toHom D₂.mapsRelators
123 (D₁.mapsRelators r hr)
124 mapsTargetRelators := by
125 intro t ht
126 exact map_mem_normalClosure_of_relators D₁.invHom D₁.mapsTargetRelators
127 (D₂.mapsTargetRelators t ht)
128 inv_toHom := by
129 intro x
130 let y : H := D₁.toHom x
131 have h₂ :
132 D₂.invHom (D₂.toHom y) * y⁻¹ ∈ Subgroup.normalClosure S :=
133 D₂.inv_toHom y
134 have h₂map :
135 D₁.invHom (D₂.invHom (D₂.toHom y) * y⁻¹) ∈
136 Subgroup.normalClosure R :=
137 map_mem_normalClosure_of_relators D₁.invHom D₁.mapsTargetRelators h₂
138 have h₂map' :
139 D₁.invHom (D₂.invHom (D₂.toHom y)) *
140 (D₁.invHom y)⁻¹ ∈
141 Subgroup.normalClosure R := by
142 simpa using h₂map
143 have h₁ :
144 D₁.invHom y * x⁻¹ ∈ Subgroup.normalClosure R :=
145 D₁.inv_toHom x
146 have hprod := Subgroup.mul_mem (Subgroup.normalClosure R) h₂map' h₁
147 have hmul :
148 (D₁.invHom (D₂.invHom (D₂.toHom y)) *
149 (D₁.invHom y)⁻¹) *
150 (D₁.invHom y * x⁻¹) =
151 D₁.invHom (D₂.invHom (D₂.toHom y)) * x⁻¹ := by
152 group
153 simpa [MonoidHom.comp_apply, y, hmul] using hprod
154 to_invHom := by
155 intro z
156 let y : H := D₂.invHom z
157 have h₁ :
158 D₁.toHom (D₁.invHom y) * y⁻¹ ∈ Subgroup.normalClosure S :=
159 D₁.to_invHom y
160 have h₁map :
161 D₂.toHom (D₁.toHom (D₁.invHom y) * y⁻¹) ∈
162 Subgroup.normalClosure T :=
163 map_mem_normalClosure_of_relators D₂.toHom D₂.mapsRelators h₁
164 have h₁map' :
165 D₂.toHom (D₁.toHom (D₁.invHom y)) *
166 (D₂.toHom y)⁻¹ ∈
167 Subgroup.normalClosure T := by
168 simpa using h₁map
169 have h₂ :
170 D₂.toHom y * z⁻¹ ∈ Subgroup.normalClosure T :=
171 D₂.to_invHom z
172 have hprod := Subgroup.mul_mem (Subgroup.normalClosure T) h₁map' h₂
173 have hmul :
174 (D₂.toHom (D₁.toHom (D₁.invHom y)) *
175 (D₂.toHom y)⁻¹) *
176 (D₂.toHom y * z⁻¹) =
177 D₂.toHom (D₁.toHom (D₁.invHom y)) * z⁻¹ := by
178 group
179 simpa [MonoidHom.comp_apply, y, hmul] using hprod
183structure RelatorQuotientForwardMapData
184 (R : Set G) (S : Set H) (invHom : H →* G) where
185 toHom : G →* H
186 mapsRelators : ∀ r ∈ R, toHom r ∈ Subgroup.normalClosure S
187 inv_toHom : ∀ x : G, invHom (toHom x) * x⁻¹ ∈ Subgroup.normalClosure R
188 to_invHom : ∀ y : H, toHom (invHom y) * y⁻¹ ∈ Subgroup.normalClosure S
191 {R : Set G} {S : Set H} {invHom : H →* G}
192 (hTarget : ∀ s ∈ S, invHom s ∈ Subgroup.normalClosure R)
193 (D : RelatorQuotientForwardMapData R S invHom) :
194 RelatorQuotientMutualMapData R S where
195 toHom := D.toHom
196 invHom := invHom
197 mapsRelators := D.mapsRelators
198 mapsTargetRelators := hTarget
199 inv_toHom := D.inv_toHom
200 to_invHom := D.to_invHom
203 {R S : Set G}
204 (h : Subgroup.normalClosure R = Subgroup.normalClosure S) :
205 RelatorQuotientMutualMapData R S where
206 toHom := MonoidHom.id G
207 invHom := MonoidHom.id G
208 mapsRelators := by
209 intro r hr
210 rw [← h]
211 exact Subgroup.subset_normalClosure hr
212 mapsTargetRelators := by
213 intro s hs
214 rw [h]
215 exact Subgroup.subset_normalClosure hs
216 inv_toHom := by
217 intro x
218 simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
219 to_invHom := by
220 intro x
221 simp only [MonoidHom.id_apply, mul_inv_cancel, one_mem]
224 {R S : Set G}
225 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
226 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
227 RelatorQuotientMutualMapData R S :=
229 (normalClosure_eq_of_relatorEquivalent hR_to_S hS_to_R)
232 (R : Set G) (S : Set H) (e : G ≃* H)
233 (hmap :
234 Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) =
235 Subgroup.normalClosure S) :
236 RelatorQuotientMutualMapData R S where
237 toHom := e.toMonoidHom
238 invHom := e.symm.toMonoidHom
239 mapsRelators := by
240 intro r hr
241 have hrmap : e r ∈ Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) :=
242 ⟨r, Subgroup.subset_normalClosure hr, rfl⟩
243 rw [← hmap]
244 exact hrmap
245 mapsTargetRelators := by
246 intro s hs
247 have hsmap : s ∈ Subgroup.map e.toMonoidHom (Subgroup.normalClosure R) := by
248 rw [hmap]
249 exact Subgroup.subset_normalClosure hs
250 rcases hsmap with ⟨r, hr, hrs⟩
251 simpa [← hrs] using hr
252 inv_toHom := by
253 intro x
254 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulEquiv.symm_apply_apply, mul_inv_cancel, one_mem]
255 to_invHom := by
256 intro y
257 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulEquiv.apply_symm_apply, mul_inv_cancel, one_mem]
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, MulEquiv.apply_symm_apply]⟩
275 rwa [Subgroup.map_normalClosure _ e.toMonoidHom e.surjective] at hsmap
278end ReidemeisterSchreier.Discrete.Presentations