Yamaguchi Lean 4 Library
ReidemeisterSchreier/Discrete/Presentations/Tietze/GeneratorMap.lean
ReidemeisterSchreier/Discrete/Presentations/Tietze/GeneratorMap/Source

ReidemeisterSchreier/Discrete/Presentations/Tietze/GeneratorMap.lean

1import ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Tietze/GeneratorMap.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
19namespace ReidemeisterSchreier.Discrete.Presentations
21variable {G H K : Type*} [Group G] [Group H] [Group K]
24 (e : G ≃* H) (R : Set G) (S : Set H)
25 (hR_to_S : ∀ r ∈ R, e r ∈ Subgroup.normalClosure S)
26 (hS_to_R : ∀ s ∈ S, e.symm s ∈ Subgroup.normalClosure R) :
32 {X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
33 (toGenerator : X → FreeGroup Y)
34 (invGenerator : Y → FreeGroup X)
35 (hR :
36 ∀ r ∈ R,
37 FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)
38 (hS :
39 ∀ s ∈ S,
40 FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)
41 (hinv_to :
42 ∀ x : X,
44 (FreeGroup.lift invGenerator (toGenerator x))
45 (FreeGroup.of x))
46 (hto_inv :
47 ∀ y : Y,
49 (FreeGroup.lift toGenerator (invGenerator y))
50 (FreeGroup.of y)) :
52 toHom := FreeGroup.lift toGenerator
53 invHom := FreeGroup.lift invGenerator
54 mapsRelators := hR
55 mapsTargetRelators := hS
56 inv_toHom := by
57 intro w
58 let N : Subgroup (FreeGroup X) := Subgroup.normalClosure R
59 let F : FreeGroup X →* FreeGroup X ⧸ N :=
60 (QuotientGroup.mk' N).comp
61 ((FreeGroup.lift invGenerator).comp (FreeGroup.lift toGenerator))
62 have hhom : F = QuotientGroup.mk' N := by
63 ext x
64 dsimp [F]
65 simp only [FreeGroup.lift_apply_of]
67 exact hinv_to x
68 have hw := congrArg (fun f : FreeGroup X →* FreeGroup X ⧸ N => f w) hhom
69 change
70 ((FreeGroup.lift invGenerator
71 (FreeGroup.lift toGenerator w) : FreeGroup X) :
72 FreeGroup X ⧸ N) =
73 ((w : FreeGroup X) : FreeGroup X ⧸ N) at hw
74 exact (by
75 simpa [N, RelatorEquivalent] using
76 (relatorEquivalent_iff_eq_in_presentedQuotient.2 hw :
78 (FreeGroup.lift invGenerator (FreeGroup.lift toGenerator w)) w))
79 to_invHom := by
80 intro w
81 let N : Subgroup (FreeGroup Y) := Subgroup.normalClosure S
82 let F : FreeGroup Y →* FreeGroup Y ⧸ N :=
83 (QuotientGroup.mk' N).comp
84 ((FreeGroup.lift toGenerator).comp (FreeGroup.lift invGenerator))
85 have hhom : F = QuotientGroup.mk' N := by
86 ext y
87 dsimp [F]
88 simp only [FreeGroup.lift_apply_of]
90 exact hto_inv y
91 have hw := congrArg (fun f : FreeGroup Y →* FreeGroup Y ⧸ N => f w) hhom
92 change
93 ((FreeGroup.lift toGenerator
94 (FreeGroup.lift invGenerator w) : FreeGroup Y) :
95 FreeGroup Y ⧸ N) =
96 ((w : FreeGroup Y) : FreeGroup Y ⧸ N) at hw
97 exact (by
98 simpa [N, RelatorEquivalent] using
99 (relatorEquivalent_iff_eq_in_presentedQuotient.2 hw :
101 (FreeGroup.lift toGenerator (FreeGroup.lift invGenerator w)) w))
104 {X Y : Type*} {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
105 (toGenerator : X → FreeGroup Y)
106 (invGenerator : Y → FreeGroup X)
107 (hR :
108 ∀ r ∈ R,
109 RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)
110 (hS :
111 ∀ s ∈ S,
112 RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)
113 (hinv_to :
114 ∀ x : X,
116 (FreeGroup.lift invGenerator (toGenerator x))
117 (FreeGroup.of x))
118 (hto_inv :
119 ∀ y : Y,
121 (FreeGroup.lift toGenerator (invGenerator y))
122 (FreeGroup.of y)) :
125 toGenerator invGenerator
126 (fun r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR r hr))
127 (fun s hs => RelatorEquivalent.mem_normalClosure_of_eq_one (hS s hs))
128 hinv_to hto_inv
130/-- Generator-map certificate for presentations whose relators are indexed
131families. This is an application-facing dispatcher: a downstream proof can check
132source and target relators one family at a time. -/
134 {X Y : Type*} {ι κ : Sort*}
135 {R : ι → Set (FreeGroup X)} {S : κ → Set (FreeGroup Y)}
136 (toGenerator : X → FreeGroup Y)
137 (invGenerator : Y → FreeGroup X)
138 (hR :
139 ∀ i : ι, ∀ r ∈ R i,
140 RelatorEquivalent (Set.iUnion S) (FreeGroup.lift toGenerator r) 1)
141 (hS :
142 ∀ k : κ, ∀ s ∈ S k,
143 RelatorEquivalent (Set.iUnion R) (FreeGroup.lift invGenerator s) 1)
144 (hinv_to :
145 ∀ x : X,
146 RelatorEquivalent (Set.iUnion R)
147 (FreeGroup.lift invGenerator (toGenerator x))
148 (FreeGroup.of x))
149 (hto_inv :
150 ∀ y : Y,
151 RelatorEquivalent (Set.iUnion S)
152 (FreeGroup.lift toGenerator (invGenerator y))
153 (FreeGroup.of y)) :
154 RelatorQuotientMutualMapData (Set.iUnion R) (Set.iUnion S) :=
156 toGenerator invGenerator
157 (by
158 intro r hr
159 rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
160 exact hR i r hi)
161 (by
162 intro s hs
163 rcases Set.mem_iUnion.1 hs with ⟨k, hk⟩
164 exact hS k s hk)
165 hinv_to hto_inv
167/-- Two-level family variant of
170 {X Y : Type*} {ι κ : Sort*} {α : ι → Sort*} {β : κ → Sort*}
171 {R : ∀ i : ι, α i → Set (FreeGroup X)}
172 {S : ∀ k : κ, β k → Set (FreeGroup Y)}
173 (toGenerator : X → FreeGroup Y)
174 (invGenerator : Y → FreeGroup X)
175 (hR :
176 ∀ i : ι, ∀ a : α i, ∀ r ∈ R i a,
178 (Set.iUnion fun k : κ => Set.iUnion (S k))
179 (FreeGroup.lift toGenerator r) 1)
180 (hS :
181 ∀ k : κ, ∀ b : β k, ∀ s ∈ S k b,
183 (Set.iUnion fun i : ι => Set.iUnion (R i))
184 (FreeGroup.lift invGenerator s) 1)
185 (hinv_to :
186 ∀ x : X,
188 (Set.iUnion fun i : ι => Set.iUnion (R i))
189 (FreeGroup.lift invGenerator (toGenerator x))
190 (FreeGroup.of x))
191 (hto_inv :
192 ∀ y : Y,
194 (Set.iUnion fun k : κ => Set.iUnion (S k))
195 (FreeGroup.lift toGenerator (invGenerator y))
196 (FreeGroup.of y)) :
198 (Set.iUnion fun i : ι => Set.iUnion (R i))
199 (Set.iUnion fun k : κ => Set.iUnion (S k)) :=
201 toGenerator invGenerator
202 (by
203 intro r hr
204 rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
205 rcases Set.mem_iUnion.1 hi with ⟨a, ha⟩
206 exact hR i a r ha)
207 (by
208 intro s hs
209 rcases Set.mem_iUnion.1 hs with ⟨k, hk⟩
210 rcases Set.mem_iUnion.1 hk with ⟨b, hb⟩
211 exact hS k b s hb)
212 hinv_to hto_inv
215 {Y : Type*} (e : FreeGroup Y ≃* G) (S : Set G) :
216 Set (FreeGroup Y) :=
217 e.symm '' S
220 {Y : Type*} (e : FreeGroup Y ≃* G) (S : Set G) :
221 Subgroup.map e.toMonoidHom
222 (Subgroup.normalClosure (freeGroupPullbackRelatorSet e S)) =
223 Subgroup.normalClosure S := by
224 rw [Subgroup.map_normalClosure _ e.toMonoidHom e.surjective]
225 congr
226 ext z
227 constructor
228 · rintro ⟨y, ⟨s, hs, hy⟩, rfl⟩
229 simpa [← hy] using hs
230 · intro hz
231 exact ⟨e.symm z, ⟨z, hz, rfl⟩, by simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulEquiv.apply_symm_apply]⟩
234 {Y : Type*} (e : FreeGroup Y ≃* G) (S : Set G) :
235 FreeGroup Y ⧸
236 Subgroup.normalClosure (freeGroupPullbackRelatorSet e S) ≃*
237 G ⧸ Subgroup.normalClosure S :=
238 QuotientGroup.congr
239 (Subgroup.normalClosure (freeGroupPullbackRelatorSet e S))
240 (Subgroup.normalClosure S)
241 e
245 (R : Set G) (S : Set H)
247 G ⧸ Subgroup.normalClosure R ≃* H ⧸ Subgroup.normalClosure S :=
249 hData.toHom hData.invHom hData.mapsRelators hData.mapsTargetRelators
250 hData.inv_toHom hData.to_invHom
253end ReidemeisterSchreier.Discrete.Presentations