Q₂ presentation — the four marked generators and the manuscript's right-conjugation / commutator conventions. (Stage A, packet 1 core.)

inductive Q2Presentation.Gen : Type

The four marked generators of the candidate presentation.

• sigma : Gen
• tau : Gen
• x0 : Gen
• x1 : Gen

instance Q2Presentation.instDecidableEqGen : DecidableEq Gen

Equations

• Q2Presentation.instDecidableEqGen x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Q2Presentation.rconj {G : Type u_1} [Group G] (x g : G) : G

Right conjugation x^g = g⁻¹ * x * g (manuscript convention).

Equations

• Q2Presentation.rconj x g = g⁻¹ * x * g

def Q2Presentation.commutatorW {G : Type u_1} [Group G] (x y : G) : G

Commutator (x, y) = x⁻¹ * y⁻¹ * x * y (manuscript convention).

Equations

• Q2Presentation.commutatorW x y = x⁻¹ * y⁻¹ * x * y

@[simp]

theorem Q2Presentation.rconj_one {G : Type u_1} [Group G] (x : G) : rconj x 1 = x