Documentation

TauCeti.GroupTheory.PresentedGroup

Words and changes of relators in presented groups #

A signed word is a list of pairs (x, b), with true denoting a generator and false its inverse. This file gives the product formula for the image of such a word under the quotient map to a presented group. The corresponding formulas for free groups are in TauCeti.GroupTheory.FreeGroup.Basic.

Equality of the normal closures of two relator sets gives a canonical isomorphism of the presented groups, preserving the image of every word.

Main results #

source
@[simp]
theorem PresentedGroup.lift_of_eq_mk {α : Type u_1} {rels : Set (FreeGroup α)} (x : FreeGroup α) :
(FreeGroup.lift of) x = (mk rels) x

Lifting the canonical generators is the quotient map on every free-group element.

source
@[simp]
theorem PresentedGroup.toGroup_mk {α : Type u_1} {G : Type u_2} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1) (x : FreeGroup α) :
(toGroup h) ((mk rels) x) = (FreeGroup.lift f) x

The induced homomorphism evaluates a presented word by the free-group lift.

source
def PresentedGroup.equivOfNormalClosureEq {α : Type u_1} {S T : Set (FreeGroup α)} (h : Subgroup.normalClosure S = Subgroup.normalClosure T) :
PresentedGroup S ≃* PresentedGroup T

Relator sets with the same normal closure present canonically isomorphic groups.

Instances For
    source
    @[simp]
    theorem PresentedGroup.equivOfNormalClosureEq_mk {α : Type u_1} {S T : Set (FreeGroup α)} (h : Subgroup.normalClosure S = Subgroup.normalClosure T) (w : FreeGroup α) :
    (equivOfNormalClosureEq h) ((mk S) w) = (mk T) w

    The canonical change of relators preserves every word.

    source
    @[simp]
    theorem PresentedGroup.equivOfNormalClosureEq_symm_mk {α : Type u_1} {S T : Set (FreeGroup α)} (h : Subgroup.normalClosure S = Subgroup.normalClosure T) (w : FreeGroup α) :
    (equivOfNormalClosureEq h).symm ((mk T) w) = (mk S) w

    The inverse change of relators also preserves every word.

    source
    @[simp]
    theorem PresentedGroup.equivPresentedGroup_mk {α : Type u_1} {β : Type u_2} (S : Set (FreeGroup α)) (e : α ≃ β) (w : FreeGroup α) :
    (equivPresentedGroup S e) ((mk S) w) = (mk (⇑(FreeGroup.freeGroupCongr e) '' S)) ((FreeGroup.freeGroupCongr e) w)

    Relabeling generators relabels every word by the induced free-group isomorphism.

    source
    theorem PresentedGroup.mk_mk {α : Type u_1} (S : Set (FreeGroup α)) (L : List (α × Bool)) :
    (mk S) (FreeGroup.mk L) = (List.map (fun (p : α × Bool) => bif p.2 then of p.1 else (of p.1)⁻¹) L).prod

    The image of a word in a presented group is the product of the images of its signed letters.