ReidemeisterSchreier/FreeGroup/Automorphisms.lean
1import Mathlib.GroupTheory.FreeGroup.NielsenSchreier
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/FreeGroup/Automorphisms.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free-group support
14Automorphisms, signed-letter words, prefix-parent operations, and generator equivalences for free groups.
15-/
17namespace ReidemeisterSchreier
19/-- The free-group automorphism sending every generator to its inverse. -/
20noncomputable def FreeGroup.generatorInversionEquiv (X : Type u) : FreeGroup X ≃* FreeGroup X where
21 toFun := FreeGroup.lift fun x => (FreeGroup.of x)⁻¹
22 invFun := FreeGroup.lift fun x => (FreeGroup.of x)⁻¹
23 left_inv := by
24 intro g
25 have h :
26 (FreeGroup.lift fun x => (FreeGroup.of x)⁻¹).comp
27 (FreeGroup.lift fun x => (FreeGroup.of x)⁻¹) =
28 MonoidHom.id (FreeGroup X) := by
29 apply FreeGroup.ext_hom
30 intro x
32 MonoidHom.id_apply]
33 exact congrArg (fun f : FreeGroup X →* FreeGroup X => f g) h
34 right_inv := by
35 intro g
36 have h :
37 (FreeGroup.lift fun x => (FreeGroup.of x)⁻¹).comp
38 (FreeGroup.lift fun x => (FreeGroup.of x)⁻¹) =
39 MonoidHom.id (FreeGroup X) := by
40 apply FreeGroup.ext_hom
41 intro x
43 MonoidHom.id_apply]
44 exact congrArg (fun f : FreeGroup X →* FreeGroup X => f g) h
45 map_mul' := by
46 intro g h
49@[simp] theorem FreeGroup.generatorInversionEquiv_apply_of (X : Type u) (x : X) :
50 FreeGroup.generatorInversionEquiv X (FreeGroup.of x) = (FreeGroup.of x)⁻¹ := by
51 simp only [generatorInversionEquiv, MulEquiv.coe_mk, Equiv.coe_fn_mk, FreeGroup.lift_apply_of]
53@[simp] theorem FreeGroup.generatorInversionEquiv_symm (X : Type u) :
54 (FreeGroup.generatorInversionEquiv X).symm = FreeGroup.generatorInversionEquiv X := by
55 ext x
56 rfl
58/-- The automorphism of a free group sending every basis element to its inverse. -/
59noncomputable def FreeGroupBasis.generatorInversionAut {ι G : Type u} [Group G]
60 (b : FreeGroupBasis ι G) : G ≃* G where
61 toFun := b.lift fun i => (b i)⁻¹
62 invFun := b.lift fun i => (b i)⁻¹
63 left_inv := by
64 intro g
65 have h :
66 (b.lift fun i => (b i)⁻¹).comp (b.lift fun i => (b i)⁻¹) = MonoidHom.id G := by
67 apply b.ext_hom
68 intro i
69 simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroupBasis.lift_apply_apply,
71 exact congrArg (fun f : G →* G => f g) h
72 right_inv := by
73 intro g
74 have h :
75 (b.lift fun i => (b i)⁻¹).comp (b.lift fun i => (b i)⁻¹) = MonoidHom.id G := by
76 apply b.ext_hom
77 intro i
78 simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroupBasis.lift_apply_apply,
80 exact congrArg (fun f : G →* G => f g) h
81 map_mul' := by
82 intro g h
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, FreeGroupBasis.lift_apply_apply,
89 FreeGroupBasis.repr_apply_coe, FreeGroup.lift_apply_of]
91theorem FreeGroupBasis.generatorInversionAut_involutive {ι G : Type u} [Group G]
92 (b : FreeGroupBasis ι G) :
93 Function.Involutive (FreeGroupBasis.generatorInversionAut b) :=
94 (FreeGroupBasis.generatorInversionAut b).left_inv
96/-- The basis of a free group obtained by inverting the standard generators. -/
97noncomputable def FreeGroup.inverseBasis (X : Type u) : FreeGroupBasis X (FreeGroup X) :=
98 (FreeGroupBasis.ofFreeGroup X).map (FreeGroup.generatorInversionEquiv X)
100@[simp] theorem FreeGroup.inverseBasis_apply {X : Type u} (x : X) :
101 FreeGroup.inverseBasis X x = (FreeGroup.of x)⁻¹ := by
102 change (FreeGroup.generatorInversionEquiv X) (FreeGroup.of x) = (FreeGroup.of x)⁻¹
103 change FreeGroup.lift (fun y : X => (FreeGroup.of y)⁻¹) (FreeGroup.of x) = (FreeGroup.of x)⁻¹
104 simp only [FreeGroup.lift_apply_of]
106end ReidemeisterSchreier