Documentation

TauCeti.GroupTheory.FreeGroup.Primitive

Primitive elements of free groups #

An element is primitive if it occurs in a free basis. The definition applies to any group, and the basis witness ensures that the group is free. Primitive elements cannot be proper powers or lie in the commutator subgroup: a basis coordinate maps them to the generator of the infinite cyclic group. Primitivity is preserved by group isomorphisms.

The Nielsen move replacing one free generator a by a b ^ n for a distinct generator b and any n : ℤ shows that a b ^ n, in particular a b, is primitive.

source
def Group.IsPrimitive {G : Type u} [Group G] (x : G) :
Prop

An element of a group is primitive when it belongs to some free basis of the group.

Instances For
    source
    theorem Group.isPrimitive_iff {G : Type u} [Group G] {x : G} :
    IsPrimitive x ↔ ∃ (ι : Type u) (b : FreeGroupBasis ι G) (i : ι), b i = x
    source
    @[simp]
    theorem FreeGroupBasis.isPrimitive {G : Type u} [Group G] {ι : Type v} (b : FreeGroupBasis ι G) (i : ι) :
    Group.IsPrimitive (b i)

    Every element of a free basis is primitive.

    source
    @[simp]
    theorem FreeGroupBasis.repr_symm_apply_of {G : Type u} [Group G] {ι : Type v} (b : FreeGroupBasis ι G) (i : ι) :
    b.repr.symm (FreeGroup.of i) = b i

    The inverse basis representation sends a free generator to its basis element.

    source
    theorem Group.IsPrimitive.map_mulEquiv {G : Type u} {H : Type v} [Group G] [Group H] {x : G} (hx : IsPrimitive x) (e : G ≃* H) :
    IsPrimitive (e x)

    A primitive element is preserved by a group isomorphism.

    source
    theorem Group.IsPrimitive.inv {G : Type u} [Group G] {x : G} (hx : IsPrimitive x) :
    IsPrimitive x⁻¹

    The inverse of a primitive element is primitive.

    source
    theorem Group.IsPrimitive.not_isProperPower {G : Type u} [Group G] {x : G} (hx : IsPrimitive x) :
    ¬IsProperPower x

    A primitive element is not a proper power.

    source
    theorem Group.IsPrimitive.ne_one {G : Type u} [Group G] {x : G} (hx : IsPrimitive x) :
    x ≠ 1

    A primitive element is nontrivial.

    source
    theorem Group.IsPrimitive.exists_monoidHom_apply_eq_ofAdd_one {G : Type u} [Group G] {x : G} (hx : IsPrimitive x) :
    ∃ (f : G →* Multiplicative ℤ), f x = Multiplicative.ofAdd 1

    Some homomorphism sends a primitive element to the generator Multiplicative.ofAdd 1 of the infinite cyclic group.

    source
    @[simp]
    theorem Group.isPrimitive_inv {G : Type u} [Group G] {x : G} :
    IsPrimitive x⁻¹ ↔ IsPrimitive x

    An element is primitive exactly when its inverse is primitive.

    source
    @[simp]
    theorem MulEquiv.isPrimitive_map_iff {G : Type u} {H : Type v} [Group G] [Group H] (e : G ≃* H) {x : G} :
    Group.IsPrimitive (e x) ↔ Group.IsPrimitive x

    Primitivity is preserved and reflected by a group isomorphism.

    source
    @[simp]
    theorem Group.isPrimitive_conj_iff {G : Type u} [Group G] (g x : G) :
    IsPrimitive (g * x * g⁻¹) ↔ IsPrimitive x

    Conjugation preserves and reflects primitivity.

    source
    @[simp]
    theorem Group.not_isPrimitive_one {G : Type u} [Group G] :
    ¬IsPrimitive 1

    The identity is not a primitive element.

    source
    theorem Group.not_isPrimitive_pow {G : Type u} [Group G] (x : G) {n : ℕ} (hn : 2 ≤ n) :
    ¬IsPrimitive (x ^ n)

    A proper natural power cannot be a primitive element.

    source
    theorem Group.not_isPrimitive_zpow {G : Type u} [Group G] (x : G) {n : ℤ} (hn : 2 ≤ n.natAbs) :
    ¬IsPrimitive (x ^ n)

    A proper integer power cannot be a primitive element.

    source
    @[simp]
    theorem Group.not_isPrimitive_sq {G : Type u} [Group G] (x : G) :
    ¬IsPrimitive (x ^ 2)

    A square cannot be a primitive element.

    source
    theorem Group.not_isPrimitive_of_mem_commutator {G : Type u} [Group G] {x : G} (hx : x ∈ commutator G) :
    ¬IsPrimitive x

    An element of the commutator subgroup cannot belong to a free basis.

    source
    @[simp]
    theorem Group.not_isPrimitive_commutator {G : Type u} [Group G] (x y : G) :
    ¬IsPrimitive ⁅x, y⁆

    A commutator cannot belong to a free basis.

    source
    @[simp]
    theorem FreeGroup.isPrimitive_of {α : Type u} (a : α) :
    Group.IsPrimitive (of a)

    Every free generator is primitive.

    source
    theorem FreeGroupBasis.isPrimitive_mul_zpow {G : Type u} [Group G] {ι : Type v} (b : FreeGroupBasis ι G) {i j : ι} (hij : i ≠ j) (n : ℤ) :
    Group.IsPrimitive (b i * b j ^ n)

    Multiplying a basis element by an integral power of another gives a primitive element.

    source
    theorem FreeGroupBasis.isPrimitive_mul {G : Type u} [Group G] {ι : Type v} (b : FreeGroupBasis ι G) {i j : ι} (hij : i ≠ j) :
    Group.IsPrimitive (b i * b j)

    The product of two distinct basis elements is primitive.

    source
    theorem FreeGroup.isPrimitive_of_mul_of_zpow {α : Type u} (a b : α) (hab : a ≠ b) (n : ℤ) :
    Group.IsPrimitive (of a * of b ^ n)

    Multiplying a free generator by an integral power of another gives a primitive element.

    source
    theorem FreeGroup.isPrimitive_of_mul_of {α : Type u} (a b : α) (hab : a ≠ b) :
    Group.IsPrimitive (of a * of b)

    The product of two distinct free generators is primitive.

    source
    theorem FreeGroup.isPrimitive_iff_exists_mulEquiv_of {α : Type u} {x : FreeGroup α} :
    Group.IsPrimitive x ↔ ∃ (e : FreeGroup α ≃* FreeGroup α) (a : α), e (of a) = x

    An element of a free group is primitive exactly when it is the image of a canonical generator under an automorphism.