Source: ProCGroups.ReidemeisterSchreier.FreeGroup.Automorphisms
1import Mathlib.GroupTheory.FreeGroup.NielsenSchreier
3/-!
4# Reidemeister Schreier / Free Group / Automorphisms
6This module constructs the free-group automorphism that inverts every
7generator, transports free bases along it, and proves the resulting
8automorphism is involutive.
9-/
11namespace ReidemeisterSchreier
13/--
14The free-group automorphism sending every generator to its inverse. It packages mutually inverse
15maps as an algebraic or topological equivalence.
16-/
17noncomputable def FreeGroup.generatorInversionEquiv (X : Type u) : FreeGroup X ≃* FreeGroup X where
18 toFun := FreeGroup.lift fun x => (FreeGroup.of x)⁻¹
19 invFun := FreeGroup.lift fun x => (FreeGroup.of x)⁻¹
20 left_inv := by
21 intro g
22 have h :
23 (FreeGroup.lift fun x => (FreeGroup.of x)⁻¹).comp
24 (FreeGroup.lift fun x => (FreeGroup.of x)⁻¹) =
25 MonoidHom.id (FreeGroup X) := by
26 apply FreeGroup.ext_hom
27 intro x
28 simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroup.lift_apply_of, map_inv, inv_inv,
29 MonoidHom.id_apply]
30 exact congrArg (fun f : FreeGroup X →* FreeGroup X => f g) h
31 right_inv := by
32 intro g
33 have h :
34 (FreeGroup.lift fun x => (FreeGroup.of x)⁻¹).comp
35 (FreeGroup.lift fun x => (FreeGroup.of x)⁻¹) =
36 MonoidHom.id (FreeGroup X) := by
37 apply FreeGroup.ext_hom
38 intro x
39 simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroup.lift_apply_of, map_inv, inv_inv,
40 MonoidHom.id_apply]
41 exact congrArg (fun f : FreeGroup X →* FreeGroup X => f g) h
42 map_mul' := by
43 intro g h
44 simp only [map_mul]
46/-- The generator-inversion automorphism sends each free generator to its inverse. -/
47@[simp] theorem FreeGroup.generatorInversionEquiv_apply_of (X : Type u) (x : X) :
48 FreeGroup.generatorInversionEquiv X (FreeGroup.of x) = (FreeGroup.of x)⁻¹ := by
49 simp only [generatorInversionEquiv, MulEquiv.coe_mk, Equiv.coe_fn_mk, FreeGroup.lift_apply_of]
51/-- The generator-inversion automorphism is its own inverse. -/
52@[simp] theorem FreeGroup.generatorInversionEquiv_symm (X : Type u) :
53 (FreeGroup.generatorInversionEquiv X).symm = FreeGroup.generatorInversionEquiv X := by
54 ext x
55 rfl
57/-- The automorphism of a free group sending every basis element to its inverse. -/
58noncomputable def FreeGroupBasis.generatorInversionAut {ι G : Type u} [Group G]
59 (b : FreeGroupBasis ι G) : G ≃* G where
60 toFun := b.lift fun i => (b i)⁻¹
61 invFun := b.lift fun i => (b i)⁻¹
62 left_inv := by
63 intro g
64 have h :
65 (b.lift fun i => (b i)⁻¹).comp (b.lift fun i => (b i)⁻¹) = MonoidHom.id G := by
66 apply b.ext_hom
67 intro i
68 simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroupBasis.lift_apply_apply,
69 FreeGroupBasis.repr_apply_coe, FreeGroup.lift_apply_of, map_inv, inv_inv, MonoidHom.id_apply]
70 exact congrArg (fun f : G →* G => f g) h
71 right_inv := by
72 intro g
73 have h :
74 (b.lift fun i => (b i)⁻¹).comp (b.lift fun i => (b i)⁻¹) = MonoidHom.id G := by
75 apply b.ext_hom
76 intro i
77 simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroupBasis.lift_apply_apply,
78 FreeGroupBasis.repr_apply_coe, FreeGroup.lift_apply_of, map_inv, inv_inv, MonoidHom.id_apply]
79 exact congrArg (fun f : G →* G => f g) h
80 map_mul' := by
81 intro g h
82 simp only [FreeGroupBasis.lift_apply_apply, map_mul]
84/-- The generator-inversion automorphism sends a generator to its prescribed inverse. -/
85@[simp] theorem FreeGroupBasis.generatorInversionAut_apply {ι G : Type u} [Group G]
86 (b : FreeGroupBasis ι G) (i : ι) :
87 FreeGroupBasis.generatorInversionAut b (b i) = (b i)⁻¹ := by
88 simp only [generatorInversionAut, MulEquiv.coe_mk, Equiv.coe_fn_mk,
89 FreeGroupBasis.lift_apply_apply,
90 FreeGroupBasis.repr_apply_coe, FreeGroup.lift_apply_of]
92/-- The generator-inversion automorphism is involutive. -/
93theorem FreeGroupBasis.generatorInversionAut_involutive {ι G : Type u} [Group G]
94 (b : FreeGroupBasis ι G) :
95 Function.Involutive (FreeGroupBasis.generatorInversionAut b) :=
96 (FreeGroupBasis.generatorInversionAut b).left_inv
98/-- The basis of a free group obtained by inverting the standard generators. -/
99noncomputable def FreeGroup.inverseBasis (X : Type u) : FreeGroupBasis X (FreeGroup X) :=
100 (FreeGroupBasis.ofFreeGroup X).map (FreeGroup.generatorInversionEquiv X)
102/-- The inverse-basis map sends each generator to its specified inverse-basis value. -/
103@[simp] theorem FreeGroup.inverseBasis_apply {X : Type u} (x : X) :
104 FreeGroup.inverseBasis X x = (FreeGroup.of x)⁻¹ := by
105 change (FreeGroup.generatorInversionEquiv X) (FreeGroup.of x) = (FreeGroup.of x)⁻¹
106 change FreeGroup.lift (fun y : X => (FreeGroup.of y)⁻¹) (FreeGroup.of x) = (FreeGroup.of x)⁻¹
107 simp only [FreeGroup.lift_apply_of]
109end ReidemeisterSchreier