The Q₂ presentation words, as data (Stage A)

The manuscript's marked generators σ, τ, x₀, x₁, the auxiliary words σ₂, u₀, u₁, d₀, z₀, c₀, g₀, d_g, h_c, h₀, and the two displayed relators (tameRelator, wildRelator) are recorded here as elements of the abstract syntax GExpr. They are deliberately boring data: every theorem about them is obtained by evaluating and applying GExpr.eval_map / GExpr.eval_pi, so there is no hand-simplification here (plan §2).

Conventions (manuscript): right conjugation x^g = g⁻¹ x g (rconjExpr) and the commutator (x, y) = x⁻¹ y⁻¹ x y (commExpr).

def Q2Presentation.Q2Word.sigma : GExpr

The tame generator σ.

Equations

• Q2Presentation.Q2Word.sigma = Q2Presentation.GExpr.gen Q2Presentation.Gen.sigma

def Q2Presentation.Q2Word.tau : GExpr

The tame generator τ.

Equations

• Q2Presentation.Q2Word.tau = Q2Presentation.GExpr.gen Q2Presentation.Gen.tau

def Q2Presentation.Q2Word.x0 : GExpr

The wild generator x₀.

Equations

• Q2Presentation.Q2Word.x0 = Q2Presentation.GExpr.gen Q2Presentation.Gen.x0

def Q2Presentation.Q2Word.x1 : GExpr

The wild generator x₁.

Equations

• Q2Presentation.Q2Word.x1 = Q2Presentation.GExpr.gen Q2Presentation.Gen.x1

def Q2Presentation.Q2Word.rconjExpr (x g : GExpr) : GExpr

Right conjugation as a word: x^g = g⁻¹ x g.

Equations

• Q2Presentation.Q2Word.rconjExpr x g = (g.inv.mul x).mul g

def Q2Presentation.Q2Word.commExpr (x y : GExpr) : GExpr

Commutator as a word: (x, y) = x⁻¹ y⁻¹ x y.

Equations

• Q2Presentation.Q2Word.commExpr x y = ((x.inv.mul y.inv).mul x).mul y

def Q2Presentation.Q2Word.sigma2 : GExpr

σ₂ := σ^{ω₂}. (GExpr.powOmega2 qualified to avoid the clash with the group-level Q2Presentation.powOmega2.)

Equations

• Q2Presentation.Q2Word.sigma2 = Q2Presentation.Q2Word.sigma.powOmega2

def Q2Presentation.Q2Word.u0 : GExpr

u₀ := (x₀ τ)^{ω₂}.

Equations

• Q2Presentation.Q2Word.u0 = (Q2Presentation.Q2Word.x0.mul Q2Presentation.Q2Word.tau).powOmega2

def Q2Presentation.Q2Word.u1 : GExpr

u₁ := (x₁ τ)^{ω₂}.

Equations

• Q2Presentation.Q2Word.u1 = (Q2Presentation.Q2Word.x1.mul Q2Presentation.Q2Word.tau).powOmega2

def Q2Presentation.Q2Word.d0 : GExpr

d₀ := u₀ x₀⁻¹.

Equations

• Q2Presentation.Q2Word.d0 = Q2Presentation.Q2Word.u0.mul Q2Presentation.Q2Word.x0.inv

def Q2Presentation.Q2Word.z0 : GExpr

z₀ := x₀^{σ₂}.

Equations

• Q2Presentation.Q2Word.z0 = Q2Presentation.Q2Word.rconjExpr Q2Presentation.Q2Word.x0 Q2Presentation.Q2Word.sigma2

def Q2Presentation.Q2Word.c0 : GExpr

c₀ := (d₀, z₀).

Equations

• Q2Presentation.Q2Word.c0 = Q2Presentation.Q2Word.commExpr Q2Presentation.Q2Word.d0 Q2Presentation.Q2Word.z0

def Q2Presentation.Q2Word.g0 : GExpr

g₀ := σ₂².

Equations

• Q2Presentation.Q2Word.g0 = Q2Presentation.Q2Word.sigma2.powNat 2

def Q2Presentation.Q2Word.dg : GExpr

d_g := d₀^{g₀}.

Equations

• Q2Presentation.Q2Word.dg = Q2Presentation.Q2Word.rconjExpr Q2Presentation.Q2Word.d0 Q2Presentation.Q2Word.g0

def Q2Presentation.Q2Word.hc : GExpr

h_c := (d_g, d₀).

Equations

• Q2Presentation.Q2Word.hc = Q2Presentation.Q2Word.commExpr Q2Presentation.Q2Word.dg Q2Presentation.Q2Word.d0

def Q2Presentation.Q2Word.h0 : GExpr

h₀ := x₀^{g₀} · x₀ · d_g · d₀ · d₀² · h_c.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Q2Word.tameRelator : GExpr

The tame relator τ^σ · (τ²)⁻¹ (the relation τ^σ = τ²).

Equations

• Q2Presentation.Q2Word.tameRelator = (Q2Presentation.Q2Word.rconjExpr Q2Presentation.Q2Word.tau Q2Presentation.Q2Word.sigma).mul (Q2Presentation.Q2Word.tau.powNat 2).inv

def Q2Presentation.Q2Word.wildRelator : GExpr

The wild relator h₀ · u₁⁻¹ · x₁^σ · c₀ (the relation h₀ u₁⁻¹ x₁^σ c₀ = 1).

Equations

• One or more equations did not get rendered due to their size.