Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Presentation
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Operations
3/-!
4# Conjugated products and presentation endomorphisms
6This module expands conjugated list products and promotes generatorwise
7normal-closure relations to all words under a free-group endomorphism.
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/-- Conjugating a list product is the product of the conjugated entries. -/
19theorem conjugate_list_prod {G : Type*} [Group G] (x : G) :
20 ∀ l : List G, x * l.prod * x⁻¹ = (l.map fun t => x * t * x⁻¹).prod
21 | [] => by
22 simp only [List.prod_nil, mul_one, mul_inv_cancel, List.map_nil]
23 | t :: ts => by
24 rw [List.prod_cons, List.map_cons, List.prod_cons]
25 calc
26 x * (t * ts.prod) * x⁻¹ = (x * t * x⁻¹) * (x * ts.prod * x⁻¹) := by
27 group
28 _ = x * t * x⁻¹ * (List.map (fun t => x * t * x⁻¹) ts).prod := by
29 rw [conjugate_list_prod x ts]
31/-- A rectangular product of conjugated entries is the conjugate of the corresponding rectangular product. -/
32theorem nested_conjugate_list_prod {G : Type*} [Group G]
33 (x : G) {p n : ℕ} (f : Fin p → Fin n → G) :
34 (List.ofFn (fun b : Fin p =>
35 (List.ofFn (fun j : Fin n => x * f b j * x⁻¹)).prod)).prod =
36 x * (List.ofFn (fun b : Fin p =>
37 (List.ofFn (fun j : Fin n => f b j)).prod)).prod * x⁻¹ := by
38 have hinner :
39 (List.ofFn (fun b : Fin p =>
40 (List.ofFn (fun j : Fin n => x * f b j * x⁻¹)).prod)) =
41 List.ofFn (fun b : Fin p =>
42 x * (List.ofFn (fun j : Fin n => f b j)).prod * x⁻¹) := by
43 apply List.ofFn_inj.2
44 funext b
45 simpa only [List.map_ofFn, Function.comp_def] using
46 (conjugate_list_prod x (List.ofFn (fun j : Fin n => f b j))).symm
47 rw [hinner]
48 simpa only [List.map_ofFn, Function.comp_def] using
49 (conjugate_list_prod x
50 (List.ofFn (fun b : Fin p =>
51 (List.ofFn (fun j : Fin n => f b j)).prod))).symm
53/-- The value of a subgroup list product is the product of the underlying subgroup elements. -/
54theorem subgroup_list_prod_val {G : Type*} [Group G]
55 {H : Subgroup G} {n : ℕ} (f : Fin n → H) :
56 (((List.ofFn f).prod : H) : G) =
57 (List.ofFn (fun i : Fin n => ((f i : H) : G))).prod := by
58 change H.subtype ((List.ofFn f).prod) =
59 (List.ofFn (fun i : Fin n => ((f i : H) : G))).prod
60 rw [map_list_prod, List.map_ofFn]
61 apply congrArg List.prod
62 apply List.ofFn_inj.2
63 funext i
64 rfl
66/--
67The subgroup nested list product underlying value is evaluated by the displayed coordinate or
68generator-level formula in the Reidemeister--Schreier rewriting system.
69-/
70theorem subgroup_nested_list_prod_val {G : Type*} [Group G]
71 {H : Subgroup G} {p n : ℕ} (f : Fin p → Fin n → H) :
72 (((List.ofFn (fun b : Fin p =>
73 (List.ofFn (fun j : Fin n => f b j)).prod)).prod : H) : G) =
74 (List.ofFn (fun b : Fin p =>
75 (List.ofFn (fun j : Fin n => ((f b j : H) : G))).prod)).prod := by
76 change H.subtype
77 ((List.ofFn (fun b : Fin p =>
78 (List.ofFn (fun j : Fin n => f b j)).prod)).prod) =
79 (List.ofFn (fun b : Fin p =>
80 (List.ofFn (fun j : Fin n => ((f b j : H) : G))).prod)).prod
81 rw [map_list_prod, List.map_ofFn]
82 apply congrArg List.prod
83 apply List.ofFn_inj.2
84 funext b
85 exact subgroup_list_prod_val (fun j : Fin n => f b j)
89/--
90If an endomorphism is congruent to the identity on generators modulo a normal closure, then it
91is congruent to the identity on every free-group word.
92-/
93theorem freeGroup_endomorph_mul_inv_mem_normalClosure_of_generator_mul_inv
94 {Y : Type*} (R : Set (FreeGroup Y)) (F : FreeGroup Y →* FreeGroup Y)
95 (hgen :
96 ∀ y : Y,
97 F (FreeGroup.of y) * (FreeGroup.of y)⁻¹ ∈ Subgroup.normalClosure R) :
98 ∀ w : FreeGroup Y, F w * w⁻¹ ∈ Subgroup.normalClosure R := by
99 classical
100 let N : Subgroup (FreeGroup Y) := Subgroup.normalClosure R
101 let q : FreeGroup Y →* FreeGroup Y ⧸ N := QuotientGroup.mk' N
102 have hq : q.comp F = q := by
103 apply FreeGroup.ext_hom
104 intro y
105 change q (F (FreeGroup.of y)) = q (FreeGroup.of y)
106 exact
107 (QuotientGroup.eq_iff_div_mem
108 (N := N) (x := F (FreeGroup.of y)) (y := FreeGroup.of y)).2
109 (by simpa [N, div_eq_mul_inv] using hgen y)
110 intro w
111 have hw :
112 q (F w) = q w := by
113 simpa using congrArg (fun ψ : FreeGroup Y →* FreeGroup Y ⧸ N => ψ w) hq
114 exact
115 (QuotientGroup.eq_iff_div_mem (N := N) (x := F w) (y := w)).1
116 (by
117 change q (F w) = q w
118 exact hw)
121end NormalClosure
123end ReidemeisterSchreier.Discrete.Presentations