Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Congruence
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic
3/-!
4# Relator maps and normal-closure congruence
6This module transports normal-closure membership and relator equivalence
7through inclusions, homomorphisms, and indexed unions of relator families.
8-/
10namespace ReidemeisterSchreier.Discrete.Presentations
12variable {G H : Type*} [Group G] [Group H]
14section NormalClosure
16variable {R S : Set G} {r a b : G}
18/-- Membership in a normal closure is preserved when the relator set is enlarged. -/
19theorem mem_normalClosure_of_subset
20 (hR_to_S : R ⊆ S) {x : G}
21 (hx : x ∈ Subgroup.normalClosure R) :
22 x ∈ Subgroup.normalClosure S :=
23 Subgroup.normalClosure_mono hR_to_S hx
25/-- Membership in the left normal closure implies membership in the normal closure of the union. -/
26theorem mem_normalClosure_union_left
27 {x : G} (hx : x ∈ Subgroup.normalClosure R) :
28 x ∈ Subgroup.normalClosure (R ∪ S) :=
29 mem_normalClosure_of_subset (R := R) (S := R ∪ S)
30 (Set.subset_union_left) hx
32/-- Membership in the right normal closure implies membership in the normal closure of the union. -/
33theorem mem_normalClosure_union_right
34 {x : G} (hx : x ∈ Subgroup.normalClosure S) :
35 x ∈ Subgroup.normalClosure (R ∪ S) :=
36 mem_normalClosure_of_subset (R := S) (S := R ∪ S)
37 (Set.subset_union_right) hx
39/--
40Membership in one indexed normal closure implies membership in the normal closure of the indexed
41union.
42-/
43theorem mem_normalClosure_iUnion
44 {ι : Sort*} (R : ι → Set G) (i : ι)
45 {x : G} (hx : x ∈ Subgroup.normalClosure (R i)) :
46 x ∈ Subgroup.normalClosure (Set.iUnion R) :=
47 mem_normalClosure_of_subset (R := R i) (S := Set.iUnion R)
48 (fun _ hy => Set.mem_iUnion.2 ⟨i, hy⟩) hx
50/--
51Membership in one doubly indexed normal closure implies membership in the normal closure of the
52doubly indexed union.
53-/
54theorem mem_normalClosure_iUnion₂
55 {ι : Sort*} {κ : ι → Sort*}
56 (R : ∀ i : ι, κ i → Set G) (i : ι) (j : κ i)
57 {x : G} (hx : x ∈ Subgroup.normalClosure (R i j)) :
58 x ∈ Subgroup.normalClosure
59 (Set.iUnion fun i : ι => Set.iUnion (R i)) :=
60 mem_normalClosure_of_subset
61 (R := R i j)
62 (S := Set.iUnion fun i : ι => Set.iUnion (R i))
63 (fun _ hy => Set.mem_iUnion.2 ⟨i, Set.mem_iUnion.2 ⟨j, hy⟩⟩) hx
65/--
66An explicit pair of indices gives membership in the normal closure of the doubly indexed union.
67-/
68theorem mem_normalClosure_iUnion₂_of_exists
69 {ι : Sort*} {κ : ι → Sort*}
70 (R : ∀ i : ι, κ i → Set G)
71 {x : G} (hx : ∃ i : ι, ∃ j : κ i,
72 x ∈ Subgroup.normalClosure (R i j)) :
73 x ∈ Subgroup.normalClosure
74 (Set.iUnion fun i : ι => Set.iUnion (R i)) := by
75 rcases hx with ⟨i, j, hij⟩
76 exact mem_normalClosure_iUnion₂ (R := R) i j hij
78/--
79Maps that preserve each indexed relator family send the union of the source relators into the
80target normal closure.
81-/
82theorem maps_iUnion_relators_mem_normalClosure
83 {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
84 (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S) :
85 ∀ r ∈ Set.iUnion R, f r ∈ Subgroup.normalClosure S := by
86 intro r hr
87 rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
88 exact hR i r hi
90/--
91Maps that preserve each doubly indexed relator family send the union of the source relators into
92the target normal closure.
93-/
94theorem maps_iUnion₂_relators_mem_normalClosure
95 {ι : Sort*} {κ : ι → Sort*}
96 (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
97 (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
98 f r ∈ Subgroup.normalClosure S) :
99 ∀ r ∈ Set.iUnion (fun i : ι => Set.iUnion (R i)),
100 f r ∈ Subgroup.normalClosure S := by
101 intro r hr
102 rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
103 rcases Set.mem_iUnion.1 hi with ⟨j, hj⟩
104 exact hR i j r hj
106/-- A relator-preserving map sends relators into the normal closure of the target relator set. -/
107theorem map_mem_normalClosure_of_relators
108 (f : G →* H) {R : Set G} {S : Set H}
109 (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
110 {x : G} (hx : x ∈ Subgroup.normalClosure R) :
111 f x ∈ Subgroup.normalClosure S := by
112 let N : Subgroup G := Subgroup.comap f (Subgroup.normalClosure S)
113 have hle : Subgroup.normalClosure R ≤ N := by
114 refine Subgroup.normalClosure_le_normal ?_
115 intro r hr
116 exact hR r hr
117 exact hle hx
119/--
120A homomorphism preserves relator equivalence when each source relator maps into the target
121normal closure.
122-/
123theorem hom_relatorEquivalent_of_maps_relators
124 (f : G →* H) {R : Set G} {S : Set H}
125 (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
126 {u v : G} (h : RelatorEquivalent R u v) :
127 RelatorEquivalent S (f u) (f v) := by
128 have hx :
129 f (u * v⁻¹) ∈ Subgroup.normalClosure S :=
130 map_mem_normalClosure_of_relators f hR (by simpa [RelatorEquivalent] using h)
131 simpa [RelatorEquivalent, map_mul] using hx
133/--
134A homomorphism preserves relator equivalence when each source relator maps to a
135target-relator-equivalent trivial word.
136-/
137theorem hom_relatorEquivalent_of_maps_relators_relatorEquivalent
138 (f : G →* H) {R : Set G} {S : Set H}
139 (hR : ∀ r ∈ R, RelatorEquivalent S (f r) 1)
140 {u v : G} (h : RelatorEquivalent R u v) :
141 RelatorEquivalent S (f u) (f v) :=
142 hom_relatorEquivalent_of_maps_relators f
143 (fun r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR r hr)) h
145/--
146A mapped relator from an indexed family lies in the normal closure of the union of the mapped
147relator families.
148-/
149theorem map_mem_normalClosure_iUnion_of_relators
150 {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
151 (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
152 {x : G} (hx : x ∈ Subgroup.normalClosure (Set.iUnion R)) :
153 f x ∈ Subgroup.normalClosure S :=
154 map_mem_normalClosure_of_relators f
155 (maps_iUnion_relators_mem_normalClosure f hR) hx
157/--
158A mapped relator from a doubly indexed family lies in the normal closure of the union of the
159mapped relator families.
160-/
161theorem map_mem_normalClosure_iUnion₂_of_relators
162 {ι : Sort*} {κ : ι → Sort*}
163 (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
164 (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
165 f r ∈ Subgroup.normalClosure S)
166 {x : G}
167 (hx : x ∈ Subgroup.normalClosure
168 (Set.iUnion fun i : ι => Set.iUnion (R i))) :
169 f x ∈ Subgroup.normalClosure S :=
170 map_mem_normalClosure_of_relators f
171 (maps_iUnion₂_relators_mem_normalClosure f hR) hx
173/--
174A homomorphism preserves relator equivalence for an indexed union of relators when every source
175relator maps into the target normal closure.
176-/
177theorem hom_relatorEquivalent_of_maps_iUnion_relators
178 {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
179 (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
180 {u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
181 RelatorEquivalent S (f u) (f v) :=
182 hom_relatorEquivalent_of_maps_relators f
183 (maps_iUnion_relators_mem_normalClosure f hR) h
185/--
186A homomorphism preserves relator equivalence for an indexed union of relators when every source
187relator maps to a target-relator-equivalent trivial word.
188-/
189theorem hom_relatorEquivalent_of_maps_iUnion_relators_relatorEquivalent
190 {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
191 (hR : ∀ i : ι, ∀ r ∈ R i, RelatorEquivalent S (f r) 1)
192 {u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
193 RelatorEquivalent S (f u) (f v) :=
194 hom_relatorEquivalent_of_maps_iUnion_relators f
195 (fun i r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR i r hr)) h
197/--
198A homomorphism preserves relator equivalence for a doubly indexed union of relators when every
199source relator maps into the target normal closure.
200-/
201theorem hom_relatorEquivalent_of_maps_iUnion₂_relators
202 {ι : Sort*} {κ : ι → Sort*}
203 (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
204 (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
205 f r ∈ Subgroup.normalClosure S)
206 {u v : G}
207 (h : RelatorEquivalent
208 (Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
209 RelatorEquivalent S (f u) (f v) :=
210 hom_relatorEquivalent_of_maps_relators f
211 (maps_iUnion₂_relators_mem_normalClosure f hR) h
213/--
214A homomorphism preserves relator equivalence for a doubly indexed union of relators when every
215source relator maps to a target-relator-equivalent trivial word.
216-/
217theorem hom_relatorEquivalent_of_maps_iUnion₂_relators_relatorEquivalent
218 {ι : Sort*} {κ : ι → Sort*}
219 (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
220 (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
221 RelatorEquivalent S (f r) 1)
222 {u v : G}
223 (h : RelatorEquivalent
224 (Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
225 RelatorEquivalent S (f u) (f v) :=
226 hom_relatorEquivalent_of_maps_iUnion₂_relators f
227 (fun i j r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR i j r hr)) h
229end NormalClosure
231end ReidemeisterSchreier.Discrete.Presentations