ReidemeisterSchreier.FreeGroup.Automorphisms
This module develops Reidemeister--Schreier rewriting, Schreier generators, finite quotient transversals, and presentation transformations.
import
- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
noncomputable def FreeGroup.generatorInversionEquiv (X : Type u) : FreeGroup X ≃* FreeGroup X where
toFun := FreeGroup.lift fun x => (FreeGroup.of x)⁻¹
invFun := FreeGroup.lift fun x => (FreeGroup.of x)⁻¹
left_inv := by
intro g
have h :
(FreeGroup.lift fun x => (FreeGroup.of x)⁻¹).comp
(FreeGroup.lift fun x => (FreeGroup.of x)⁻¹) =
MonoidHom.id (FreeGroup X) := by
apply FreeGroup.ext_hom
intro x
simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroup.lift_apply_of, map_inv, inv_inv,
MonoidHom.id_apply]
exact congrArg (fun f : FreeGroup X →* FreeGroup X => f g) h
right_inv := by
intro g
have h :
(FreeGroup.lift fun x => (FreeGroup.of x)⁻¹).comp
(FreeGroup.lift fun x => (FreeGroup.of x)⁻¹) =
MonoidHom.id (FreeGroup X) := by
apply FreeGroup.ext_hom
intro x
simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroup.lift_apply_of, map_inv, inv_inv,
MonoidHom.id_apply]
exact congrArg (fun f : FreeGroup X →* FreeGroup X => f g) h
map_mul' := by
intro g h
simp only [map_mul]The free-group automorphism sending every generator to its inverse. It packages mutually inverse maps as an algebraic or topological equivalence.
@[simp] theorem FreeGroup.generatorInversionEquiv_apply_of (X : Type u) (x : X) :
FreeGroup.generatorInversionEquiv X (FreeGroup.of x) = (FreeGroup.of x)⁻¹The generator-inversion map defines an equivalence, with inverse given by the same inversion construction.
Show proof
by
simp only [generatorInversionEquiv, MulEquiv.coe_mk, Equiv.coe_fn_mk, FreeGroup.lift_apply_of]Proof. Use the universal property of the free group. The proposed map is determined by its values on generators, and the inverse map sends each generator back by the opposite generator formula. Checking the two composites on generators proves that the maps are inverse homomorphisms, so the packaged automorphism and its pointwise formulas follow.
□@[simp] theorem FreeGroup.generatorInversionEquiv_symm (X : Type u) :
(FreeGroup.generatorInversionEquiv X).symm = FreeGroup.generatorInversionEquiv XThe generator-inversion map defines an equivalence, with inverse given by the same inversion construction.
Show proof
by
ext x
rflProof. Use the universal property of the free group. The proposed map is determined by its values on generators, and the inverse map sends each generator back by the opposite generator formula. Checking the two composites on generators proves that the maps are inverse homomorphisms, so the packaged automorphism and its pointwise formulas follow.
□noncomputable def FreeGroupBasis.generatorInversionAut {ι G : Type u} [Group G]
(b : FreeGroupBasis ι G) : G ≃* G where
toFun := b.lift fun i => (b i)⁻¹
invFun := b.lift fun i => (b i)⁻¹
left_inv := by
intro g
have h :
(b.lift fun i => (b i)⁻¹).comp (b.lift fun i => (b i)⁻¹) = MonoidHom.id G := by
apply b.ext_hom
intro i
simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroupBasis.lift_apply_apply,
FreeGroupBasis.repr_apply_coe, FreeGroup.lift_apply_of, map_inv, inv_inv, MonoidHom.id_apply]
exact congrArg (fun f : G →* G => f g) h
right_inv := by
intro g
have h :
(b.lift fun i => (b i)⁻¹).comp (b.lift fun i => (b i)⁻¹) = MonoidHom.id G := by
apply b.ext_hom
intro i
simp only [MonoidHom.coe_comp, Function.comp_apply, FreeGroupBasis.lift_apply_apply,
FreeGroupBasis.repr_apply_coe, FreeGroup.lift_apply_of, map_inv, inv_inv, MonoidHom.id_apply]
exact congrArg (fun f : G →* G => f g) h
map_mul' := by
intro g h
simp only [FreeGroupBasis.lift_apply_apply, map_mul]The automorphism of a free group sending every basis element to its inverse.
@[simp] theorem FreeGroupBasis.generatorInversionAut_apply {ι G : Type u} [Group G]
(b : FreeGroupBasis ι G) (i : ι) :
FreeGroupBasis.generatorInversionAut b (b i) = (b i)⁻¹Show proof
by
simp only [generatorInversionAut, MulEquiv.coe_mk, Equiv.coe_fn_mk, FreeGroupBasis.lift_apply_apply,
FreeGroupBasis.repr_apply_coe, FreeGroup.lift_apply_of]Proof. Use the universal property of the free group. The proposed map is determined by its values on generators, and the inverse map sends each generator back by the opposite generator formula. Checking the two composites on generators proves that the maps are inverse homomorphisms, so the packaged automorphism and its pointwise formulas follow.
□theorem FreeGroupBasis.generatorInversionAut_involutive {ι G : Type u} [Group G]
(b : FreeGroupBasis ι G) :
Function.Involutive (FreeGroupBasis.generatorInversionAut b)The generator-inversion automorphism is involutive.
Show proof
(FreeGroupBasis.generatorInversionAut b).left_invProof. Use the universal property of the free group. The proposed map is determined by its values on generators, and the inverse map sends each generator back by the opposite generator formula. Checking the two composites on generators proves that the maps are inverse homomorphisms, so the packaged automorphism and its pointwise formulas follow.
□noncomputable def FreeGroup.inverseBasis (X : Type u) : FreeGroupBasis X (FreeGroup X) :=
(FreeGroupBasis.ofFreeGroup X).map (FreeGroup.generatorInversionEquiv X)The basis of a free group obtained by inverting the standard generators.
@[simp] theorem FreeGroup.inverseBasis_apply {X : Type u} (x : X) :
FreeGroup.inverseBasis X x = (FreeGroup.of x)⁻¹The inverse-basis map sends each generator to its specified inverse-basis value.
Show proof
by
change (FreeGroup.generatorInversionEquiv X) (FreeGroup.of x) = (FreeGroup.of x)⁻¹
change FreeGroup.lift (fun y : X => (FreeGroup.of y)⁻¹) (FreeGroup.of x) = (FreeGroup.of x)⁻¹
simp only [FreeGroup.lift_apply_of]Proof. Use the universal property of the free group. The proposed map is determined by its values on generators, and the inverse map sends each generator back by the opposite generator formula. Checking the two composites on generators proves that the maps are inverse homomorphisms, so the packaged automorphism and its pointwise formulas follow.
□