Documentation

TauCeti.GroupTheory.FreeGroup.Nielsen

Elementary automorphisms of free groups #

Inverting every generator and multiplying one generator by an integral power of another both give automorphisms of a free group. These transformations supply bases used to construct primitive elements.

source
noncomputable def TauCeti.FreeGroup.generatorInversion {α : Type u} :
FreeGroup α ≃* FreeGroup α

The automorphism that inverts every free generator.

Instances For
    source
    @[simp]
    theorem TauCeti.FreeGroup.generatorInversion_of {α : Type u} (a : α) :
    generatorInversion (FreeGroup.of a) = (FreeGroup.of a)⁻¹

    Generator inversion sends each generator to its inverse.

    source
    @[simp]
    theorem TauCeti.FreeGroup.generatorInversion_symm_of {α : Type u} (a : α) :
    generatorInversion.symm (FreeGroup.of a) = (FreeGroup.of a)⁻¹

    The inverse automorphism also inverts every generator.

    source
    noncomputable def TauCeti.FreeGroup.nielsenMul {α : Type u} (a b : α) (hab : a ≠ b) (n : ℤ) :
    FreeGroup α ≃* FreeGroup α

    The Nielsen automorphism sending a to a b ^ n and fixing the other free generators.

    Instances For
      source
      @[simp]
      theorem TauCeti.FreeGroup.nielsenMul_of_left {α : Type u} (a b : α) (hab : a ≠ b) (n : ℤ) :
      (nielsenMul a b hab n) (FreeGroup.of a) = FreeGroup.of a * FreeGroup.of b ^ n

      The Nielsen transformation multiplies the selected generator by a power of the other.

      source
      @[simp]
      theorem TauCeti.FreeGroup.nielsenMul_of_ne {α : Type u} (a b i : α) (hab : a ≠ b) (n : ℤ) (hi : i ≠ a) :
      (nielsenMul a b hab n) (FreeGroup.of i) = FreeGroup.of i

      The Nielsen transformation fixes every other generator.

      source
      theorem TauCeti.FreeGroup.nielsenMul_symm_of_left {α : Type u} (a b : α) (hab : a ≠ b) (n : ℤ) :
      (nielsenMul a b hab n).symm (FreeGroup.of a) = FreeGroup.of a * FreeGroup.of b ^ (-n)

      The inverse Nielsen transformation uses the opposite exponent.

      source
      theorem TauCeti.FreeGroup.nielsenMul_symm_of_ne {α : Type u} (a b i : α) (hab : a ≠ b) (n : ℤ) (hi : i ≠ a) :
      (nielsenMul a b hab n).symm (FreeGroup.of i) = FreeGroup.of i

      The inverse Nielsen transformation fixes every other generator.

      source
      @[simp]
      theorem TauCeti.FreeGroup.nielsenMul_symm {α : Type u} (a b : α) (hab : a ≠ b) (n : ℤ) :
      (nielsenMul a b hab n).symm = nielsenMul a b hab (-n)

      The inverse Nielsen transformation is the move with the opposite exponent.