Index-two Reidemeister--Schreier rewriting for presentations by involutions

Let G = ⟨X | R⟩ be a group presented by involutions: every generator squares to the identity in G, and every relator of R other than those squares is a word of even length. Sending every generator to the nontrivial element of C₂ then defines the parity homomorphism G →* C₂, and its kernel is a subgroup of index at most two. The Reidemeister--Schreier method presents that kernel on the Schreier generators of the transversal {1, a} for a distinguished generator a: the generator attached to x ≠ a is a x, the one attached to a is trivial, and a source word x₁ x₂ x₃ ⋯ of even length rewrites as (a x₁)⁻¹ (a x₂) (a x₃)⁻¹ ⋯, the sign of each letter alternating with its position. The rewrite of a relator r and of its conjugate a r a together present the kernel.

This file proves that theorem for such presentations. TauCeti.schreierWord is the rewrite, TauCeti.schreierRelators is the rewritten relator set, TauCeti.IsSchreierIndexTwoSource records the hypotheses on the source presentation, and TauCeti.IsSchreierIndexTwoSource.mulEquivKerParityHom is the identification of the rewritten presented group with the kernel of the parity homomorphism. The kernel is the commutator subgroup as soon as all generators agree in the abelianization, TauCeti.IsSchreierIndexTwoSource.commutator_eq_ker_parityHom.

The generator index type of the rewritten presentation is left free, as an equivalence e between the source generators other than a and a type β, so that a transcription indexed by Fin n is a direct instance.

Main definitions

• TauCeti.lengthParity: the homomorphism from the free group to C₂ sending every generator to the nontrivial element.
• TauCeti.schreierWord and TauCeti.schreierRelators: the Reidemeister--Schreier rewrite of a word and of a set of words for the transversal {1, a}.
• TauCeti.IsSchreierIndexTwoSource: the hypotheses on a source presentation R and the set W of words to rewrite.
• TauCeti.IsSchreierIndexTwoSource.parityHom: the parity homomorphism of the source presented group.
• TauCeti.IsSchreierIndexTwoSource.toPresentedGroup: the homomorphism from the rewritten presented group to the source presented group, sending the Schreier generator of x to a x.
• TauCeti.IsSchreierIndexTwoSource.mulEquivKerParityHom and TauCeti.IsSchreierIndexTwoSource.mulEquivCommutator: the rewritten presented group is the kernel of the parity homomorphism, and the commutator subgroup when all generators agree in the abelianization.
• TauCeti.GroupPresentation.mulEquivCommutator: the same identification for a transcribed presentation row whose relations are the rewritten relators.

Main results

• TauCeti.IsSchreierIndexTwoSource.range_toPresentedGroup_eq_ker_parityHom: the rewritten presented group maps onto the kernel of the parity homomorphism.
• TauCeti.IsSchreierIndexTwoSource.toPresentedGroup_injective: that map is injective.
• TauCeti.IsSchreierIndexTwoSource.commutator_eq_ker_parityHom: the kernel of the parity homomorphism is the commutator subgroup when all generators agree in the abelianization.

References

• W. Magnus, A. Karrass and D. Solitar, Combinatorial Group Theory, §2.3, for the Reidemeister--Schreier method.
• D. L. Johnson, Presentations of Groups, 2nd ed., Chapter 9.

The length parity

def TauCeti.lengthParity (α : Type u_3) : FreeGroup α →* Multiplicative (ZMod 2)

The length parity of a word: the homomorphism from the free group on α to C₂ sending every generator to the nontrivial element. On the word L it is the parity of the length of L, TauCeti.lengthParity_mk.

@[simp]

theorem TauCeti.lengthParity_of {α : Type u_1} (x : α) : (lengthParity α) (FreeGroup.of x) = Multiplicative.ofAdd 1

Every generator has odd length parity.

theorem TauCeti.lengthParity_mk_singleton_false {α : Type u_1} (x : α) : (lengthParity α) (FreeGroup.mk [(x, false)]) = Multiplicative.ofAdd 1

The inverse of a generator has odd length parity.

theorem TauCeti.lengthParity_mk {α : Type u_1} (L : PresentationWord α) : (lengthParity α) (FreeGroup.mk L) = Multiplicative.ofAdd ↑(List.length L)

The length parity of a word is the parity of its length.

The rewrite

def TauCeti.schreierWord {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) : Bool → PresentationWord α → PresentationWord β

The Reidemeister--Schreier rewrite of a word for the transversal {1, a}, on the Schreier generators indexed by β through e. The Boolean positive records whether the current transversal representative is a: a source letter x ≠ a read at representative a contributes the generator a x and read at representative 1 contributes its inverse, the letter a contributes nothing, and every letter switches the representative. The sign of a source letter is ignored, the source generators being involutions.

Starting from false rewrites the word itself, starting from true rewrites its conjugate by a.

@[simp]

theorem TauCeti.schreierWord_nil {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (positive : Bool) : schreierWord a e positive [] = []

The empty word rewrites to the empty word.

@[simp]

theorem TauCeti.schreierWord_cons {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (positive : Bool) (x : α) (s : Bool) (w : PresentationWord α) : schreierWord a e positive ((x, s) :: w) = (if h : x = a then [] else [(e ⟨x, h⟩, positive)]) ++ schreierWord a e (!positive) w

One step of the rewrite: the letter a contributes nothing and any other letter contributes its Schreier generator, inverted exactly when the current representative is 1; the representative then switches.

theorem TauCeti.schreierWord_not {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (positive : Bool) (w : PresentationWord α) : schreierWord a e (!positive) w = List.map (fun (p : β × Bool) => (p.1, !p.2)) (schreierWord a e positive w)

Starting the rewrite from the other representative flips every sign.

theorem TauCeti.schreierWord_cons_eq_append {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (positive : Bool) (x : α) (s : Bool) (w : PresentationWord α) : schreierWord a e positive ((x, s) :: w) = schreierWord a e positive [(x, s)] ++ schreierWord a e (!positive) w

The rewrite of a word is the rewrite of its first letter followed by the rewrite of the rest from the other representative.

def TauCeti.schreierRelators {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) : Set (FreeGroup β)

The Reidemeister--Schreier relators of a set W of source words: the rewrites of every word of W from both transversal representatives, that is, the rewrites of w and of a w a for every w ∈ W.

@[simp]

theorem TauCeti.mem_schreierRelators {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) {W : Set (PresentationWord α)} {r : FreeGroup β} : r ∈ schreierRelators a e W ↔ ∃ (positive : Bool), ∃ w ∈ W, FreeGroup.mk (schreierWord a e positive w) = r

theorem TauCeti.mk_schreierWord_mem_schreierRelators {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) {W : Set (PresentationWord α)} (positive : Bool) {w : PresentationWord α} (hw : w ∈ W) : FreeGroup.mk (schreierWord a e positive w) ∈ schreierRelators a e W

def TauCeti.schreierGenerator {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) (x : α) : PresentedGroup (schreierRelators a e W)

The Schreier generator of a source generator in the rewritten presented group: the class of the generator indexed by x for x ≠ a, and the identity for x = a. It stands for the element a x of the source group, TauCeti.IsSchreierIndexTwoSource.toPresentedGroup_schreierGenerator.

@[simp]

theorem TauCeti.schreierGenerator_self {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) : schreierGenerator a e W a = 1

theorem TauCeti.schreierGenerator_of_ne {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) {x : α} (hx : x ≠ a) : schreierGenerator a e W x = PresentedGroup.of (e ⟨x, hx⟩)

@[simp]

theorem TauCeti.schreierGenerator_symm {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) (y : β) : schreierGenerator a e W ↑(e.symm y) = PresentedGroup.of y

The Schreier generator of the source generator indexed by y is the generator y.

theorem TauCeti.mk_mk_schreierWord_singleton {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) (x : α) (s : Bool) : (PresentedGroup.mk (schreierRelators a e W)) (FreeGroup.mk (schreierWord a e false [(x, s)])) = (schreierGenerator a e W x)⁻¹

The class of the singleton rewrite of a source letter read at representative 1 is the inverse of its Schreier generator.

Conjugation by the transversal element

def TauCeti.schreierInvHom {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) : PresentedGroup (schreierRelators a e W) →* PresentedGroup (schreierRelators a e W)

Inverting every Schreier generator, as an endomorphism of the rewritten presented group. It is the action of conjugation by a on the kernel, since a (a x) a⁻¹ = x a = (a x)⁻¹ for involutions; it is an automorphism, TauCeti.schreierInvAut.

@[simp]

theorem TauCeti.schreierInvHom_of {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) (y : β) : (schreierInvHom a e W) (PresentedGroup.of y) = (PresentedGroup.of y)⁻¹

@[simp]

theorem TauCeti.schreierInvHom_apply_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) (g : PresentedGroup (schreierRelators a e W)) : (schreierInvHom a e W) ((schreierInvHom a e W) g) = g

Inverting every generator is an involution.

@[simp]

theorem TauCeti.schreierInvHom_schreierGenerator {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) (x : α) : (schreierInvHom a e W) (schreierGenerator a e W x) = (schreierGenerator a e W x)⁻¹

Inverting every generator inverts every Schreier generator.

def TauCeti.schreierInvAut {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) : MulAut (PresentedGroup (schreierRelators a e W))

Inverting every Schreier generator, as an automorphism of the rewritten presented group.

@[simp]

theorem TauCeti.schreierInvAut_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) (g : PresentedGroup (schreierRelators a e W)) : (schreierInvAut a e W) g = (schreierInvHom a e W) g

theorem TauCeti.schreierInvAut_sq {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) : schreierInvAut a e W ^ 2 = 1

The inverting automorphism has order dividing two.

def TauCeti.schreierConjAction {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) : Multiplicative (ZMod 2) →* MulAut (PresentedGroup (schreierRelators a e W))

The action of C₂ on the rewritten presented group through the inverting automorphism: the nontrivial element acts by TauCeti.schreierInvAut.

theorem TauCeti.schreierConjAction_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) (g : Multiplicative (ZMod 2)) : (schreierConjAction a e W) g = schreierInvAut a e W ^ (Multiplicative.toAdd g).val

theorem TauCeti.schreierConjAction_ofAdd_one {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (W : Set (PresentationWord α)) : (schreierConjAction a e W) (Multiplicative.ofAdd 1) = schreierInvAut a e W

The nontrivial element of C₂ acts by inverting every Schreier generator.

The source presentation

structure TauCeti.IsSchreierIndexTwoSource {α : Type u_1} (R : Set (FreeGroup α)) (W : Set (PresentationWord α)) : Prop

The hypotheses of index-two Reidemeister--Schreier rewriting on a source presentation. The group is PresentedGroup R; W is the set of source words to rewrite. Every generator is an involution in the presented group, every word of W has even length and is a relation of the presented group, and every relator of R is either the class of a word of W or the square of a generator. The squares are what the rewrite leaves out: they rewrite to words that are trivial in the free group.

• of_mul_of (x : α) : PresentedGroup.of x * PresentedGroup.of x = 1

  Every generator is an involution in the presented group.

• even_length (w : PresentationWord α) : w ∈ W → Even (List.length w)

  Every source word has even length.

• mk_mk_eq_one (w : PresentationWord α) : w ∈ W → (PresentedGroup.mk R) (FreeGroup.mk w) = 1

  Every source word is a relation of the presented group.

• eq_mk_or_eq_of_mul_of (r : FreeGroup α) : r ∈ R → (∃ w ∈ W, FreeGroup.mk w = r) ∨ ∃ (x : α), FreeGroup.of x * FreeGroup.of x = r

  Every relator is the class of a source word or the square of a generator.

theorem TauCeti.IsSchreierIndexTwoSource.inv_of {α : Type u_1} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) (x : α) : (PresentedGroup.of x)⁻¹ = PresentedGroup.of x

theorem TauCeti.IsSchreierIndexTwoSource.mk_mk_cons {α : Type u_1} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) (x : α) (s : Bool) (L : PresentationWord α) : (PresentedGroup.mk R) (FreeGroup.mk ((x, s) :: L)) = PresentedGroup.of x * (PresentedGroup.mk R) (FreeGroup.mk L)

Reading one letter of a word in the source presented group, whichever sign it carries.

The parity homomorphism

theorem TauCeti.IsSchreierIndexTwoSource.lengthParity_eq_one {α : Type u_1} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) (r : FreeGroup α) : r ∈ R → (lengthParity α) r = 1

def TauCeti.IsSchreierIndexTwoSource.parityHom {α : Type u_1} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) : PresentedGroup R →* Multiplicative (ZMod 2)

The parity homomorphism of the source presented group: every generator goes to the nontrivial element of C₂.

@[simp]

theorem TauCeti.IsSchreierIndexTwoSource.parityHom_of {α : Type u_1} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) (x : α) : h.parityHom (PresentedGroup.of x) = Multiplicative.ofAdd 1

theorem TauCeti.IsSchreierIndexTwoSource.parityHom_mk_mk {α : Type u_1} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) (L : PresentationWord α) : h.parityHom ((PresentedGroup.mk R) (FreeGroup.mk L)) = Multiplicative.ofAdd ↑(List.length L)

The parity homomorphism reads the parity of the length of a word.

theorem TauCeti.IsSchreierIndexTwoSource.mk_mk_mem_ker_parityHom_iff {α : Type u_1} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) (L : PresentationWord α) : (PresentedGroup.mk R) (FreeGroup.mk L) ∈ h.parityHom.ker ↔ Even (List.length L)

The class of a word lies in the kernel of the parity homomorphism exactly when the word has even length.

The map from the rewritten presentation

theorem TauCeti.IsSchreierIndexTwoSource.lift_mk_schreierWord {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (positive : Bool) (w : PresentationWord α) : ((FreeGroup.lift fun (y : β) => PresentedGroup.of a * PresentedGroup.of ↑(e.symm y)) (FreeGroup.mk (schreierWord a e positive w)) * bif positive ^^ decide (Odd (List.length w)) then PresentedGroup.of a else 1) = (bif positive then PresentedGroup.of a else 1) * (PresentedGroup.mk R) (FreeGroup.mk w)

The lift of y ↦ a x_y to the free group evaluates a rewritten word against the source word, up to the transversal representatives at the two ends. Writing t true = a and t false = 1, the rewrite of w from representative t satisfies ρ(w) · t' = t · w, where t' is the representative reached after reading w.

theorem TauCeti.IsSchreierIndexTwoSource.lift_mk_schreierWord_of_mem {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) {w : PresentationWord α} (hw : w ∈ W) (positive : Bool) : (FreeGroup.lift fun (y : β) => PresentedGroup.of a * PresentedGroup.of ↑(e.symm y)) (FreeGroup.mk (schreierWord a e positive w)) = 1

def TauCeti.IsSchreierIndexTwoSource.toPresentedGroup {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) : PresentedGroup (schreierRelators a e W) →* PresentedGroup R

The homomorphism from the rewritten presented group to the source presented group, sending the Schreier generator indexed by y to a x_y, for x_y the source generator it names. It is injective, TauCeti.IsSchreierIndexTwoSource.toPresentedGroup_injective, with range the kernel of the parity homomorphism, TauCeti.IsSchreierIndexTwoSource.range_toPresentedGroup_eq_ker_parityHom.

@[simp]

theorem TauCeti.IsSchreierIndexTwoSource.toPresentedGroup_of {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (y : β) : (h.toPresentedGroup a e) (PresentedGroup.of y) = PresentedGroup.of a * PresentedGroup.of ↑(e.symm y)

theorem TauCeti.IsSchreierIndexTwoSource.toPresentedGroup_mk {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (z : FreeGroup β) : (h.toPresentedGroup a e) ((PresentedGroup.mk (schreierRelators a e W)) z) = (FreeGroup.lift fun (y : β) => PresentedGroup.of a * PresentedGroup.of ↑(e.symm y)) z

@[simp]

theorem TauCeti.IsSchreierIndexTwoSource.toPresentedGroup_schreierGenerator {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (x : α) : (h.toPresentedGroup a e) (schreierGenerator a e W x) = PresentedGroup.of a * PresentedGroup.of x

The Schreier generator of x goes to a x.

theorem TauCeti.IsSchreierIndexTwoSource.toPresentedGroup_mk_mk_schreierWord {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) {w : PresentationWord α} (hw : Even (List.length w)) : (h.toPresentedGroup a e) ((PresentedGroup.mk (schreierRelators a e W)) (FreeGroup.mk (schreierWord a e false w))) = (PresentedGroup.mk R) (FreeGroup.mk w)

The rewrite of an even-length word from representative 1 goes to the word itself.

theorem TauCeti.IsSchreierIndexTwoSource.parityHom_toPresentedGroup {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (g : PresentedGroup (schreierRelators a e W)) : h.parityHom ((h.toPresentedGroup a e) g) = 1

theorem TauCeti.IsSchreierIndexTwoSource.range_toPresentedGroup_eq_ker_parityHom {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) : (h.toPresentedGroup a e).range = h.parityHom.ker

The rewritten presented group maps onto the kernel of the parity homomorphism.

Injectivity, through the semidirect product H ⋊ C₂

theorem TauCeti.IsSchreierIndexTwoSource.toPresentedGroup_injective {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) : Function.Injective ⇑(h.toPresentedGroup a e)

The map from the rewritten presented group is injective: composed with the map of the source presented group into H ⋊ C₂ it is the inclusion of H.

The identification

noncomputable def TauCeti.IsSchreierIndexTwoSource.mulEquivKerParityHom {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) : PresentedGroup (schreierRelators a e W) ≃* ↥h.parityHom.ker

Index-two Reidemeister--Schreier rewriting. The group presented by the rewrites of the source words is the kernel of the parity homomorphism of the source presented group, the Schreier generator indexed by y going to a x_y.

@[simp]

theorem TauCeti.IsSchreierIndexTwoSource.coe_mulEquivKerParityHom_apply {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (g : PresentedGroup (schreierRelators a e W)) : ↑((h.mulEquivKerParityHom a e) g) = (h.toPresentedGroup a e) g

theorem TauCeti.IsSchreierIndexTwoSource.commutator_eq_ker_parityHom {α : Type u_1} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) (a : α) (habel : ∀ (x : α), Abelianization.of (PresentedGroup.of x) = Abelianization.of (PresentedGroup.of a)) : commutator (PresentedGroup R) = h.parityHom.ker

The kernel of the parity homomorphism is the commutator subgroup as soon as all generators agree in the abelianization: an even-length word is then an even power of one element of order at most two there.

noncomputable def TauCeti.IsSchreierIndexTwoSource.mulEquivCommutator {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (habel : ∀ (x : α), Abelianization.of (PresentedGroup.of x) = Abelianization.of (PresentedGroup.of a)) : PresentedGroup (schreierRelators a e W) ≃* ↥(commutator (PresentedGroup R))

Index-two Reidemeister--Schreier rewriting onto the commutator subgroup. When all generators agree in the abelianization, the group presented by the rewrites of the source words is the commutator subgroup of the source presented group.

@[simp]

theorem TauCeti.IsSchreierIndexTwoSource.coe_mulEquivCommutator_apply {α : Type u_1} {β : Type u_2} {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (h : IsSchreierIndexTwoSource R W) [DecidableEq α] (a : α) (e : { x : α // x ≠ a } ≃ β) (habel : ∀ (x : α), Abelianization.of (PresentedGroup.of x) = Abelianization.of (PresentedGroup.of a)) (g : PresentedGroup (schreierRelators a e W)) : ↑((h.mulEquivCommutator a e habel) g) = (h.toPresentedGroup a e) g

Presentation rows

noncomputable def TauCeti.GroupPresentation.mulEquivCommutator {α : Type u_1} [DecidableEq α] {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (P : GroupPresentation) (h : IsSchreierIndexTwoSource R W) (a : α) (e : { x : α // x ≠ a } ≃ Fin P.generatorCount) (habel : ∀ (x : α), Abelianization.of (PresentedGroup.of x) = Abelianization.of (PresentedGroup.of a)) (hrel : Subgroup.normalClosure (Relator.relatorSet P.transcribed) = Subgroup.normalClosure (schreierRelators a e W)) : P.Group ≃* ↥(commutator (PresentedGroup R))

A transcribed presentation row presents the commutator subgroup of a source presentation when its relations have the same normal closure as the Reidemeister--Schreier relators of the source words, indexed by the row's generators through e, and the source generators agree in the abelianization. This is TauCeti.IsSchreierIndexTwoSource.mulEquivCommutator for a row in the auditable format, so that a transcription can be identified with the subgroup its source describes.

@[simp]

theorem TauCeti.GroupPresentation.coe_mulEquivCommutator_of {α : Type u_1} [DecidableEq α] {R : Set (FreeGroup α)} {W : Set (PresentationWord α)} (P : GroupPresentation) (h : IsSchreierIndexTwoSource R W) (a : α) (e : { x : α // x ≠ a } ≃ Fin P.generatorCount) (habel : ∀ (x : α), Abelianization.of (PresentedGroup.of x) = Abelianization.of (PresentedGroup.of a)) (hrel : Subgroup.normalClosure (Relator.relatorSet P.transcribed) = Subgroup.normalClosure (schreierRelators a e W)) (i : Fin P.generatorCount) : ↑((P.mulEquivCommutator h a e habel hrel) (PresentedGroup.of i)) = PresentedGroup.of a * PresentedGroup.of ↑(e.symm i)

The row generator indexed by i goes to a x, for x the source generator it names.