Gordon 2022: the right-hand free basis

The right-hand amalgamating words in Gordon's Lemma 2.1 are words in the free group on b, beta. This file proves that they freely generate. The proof maps that free group to the coproduct Z * Z and assigns an explicit reduced normal form to every reduced word in nonzero powers of the proposed basis elements.

@[reducible, inline]

abbrev Undecidability.Gordon.RightNormalForm.ZMul : Type

The infinite cyclic group, written multiplicatively.

Equations

• Undecidability.Gordon.RightNormalForm.ZMul = Multiplicative ℤ

@[reducible, inline]

abbrev Undecidability.Gordon.RightNormalForm.CyclicFamily (d : ℕ) : Fin d → Type

An indexed family of infinite cyclic groups.

Equations

• Undecidability.Gordon.RightNormalForm.CyclicFamily d x✝ = Undecidability.Gordon.RightNormalForm.ZMul

@[reducible, inline]

abbrev Undecidability.Gordon.RightNormalForm.CyclicCoprod (d : ℕ) : Type

The free product of the indicated number of infinite cyclic groups.

Equations

• Undecidability.Gordon.RightNormalForm.CyclicCoprod d = Monoid.CoprodI (Undecidability.Gordon.RightNormalForm.CyclicFamily d)

@[reducible, inline]

abbrev Undecidability.Gordon.RightNormalForm.BasisFamily (n : ℕ) : BasisIndex n → Type

The cyclic factor assigned to each proposed basis element.

Equations

• Undecidability.Gordon.RightNormalForm.BasisFamily n x✝ = Undecidability.Gordon.RightNormalForm.ZMul

@[reducible, inline]

abbrev Undecidability.Gordon.RightNormalForm.BasisCoprod (n : ℕ) : Type

The free product with one cyclic factor for each proposed basis element.

Equations

• Undecidability.Gordon.RightNormalForm.BasisCoprod n = Monoid.CoprodI (Undecidability.Gordon.RightNormalForm.BasisFamily n)

@[reducible, inline]

abbrev Undecidability.Gordon.RightNormalForm.R : Type

The indexed free product realizing the right-hand free group.

Equations

• Undecidability.Gordon.RightNormalForm.R = Undecidability.Gordon.RightNormalForm.CyclicCoprod 2

def Undecidability.Gordon.RightNormalForm.b : R

The generator b in Gordon’s right normal form construction.

Equations

• Undecidability.Gordon.RightNormalForm.b = Monoid.CoprodI.of (Multiplicative.ofAdd 1)

def Undecidability.Gordon.RightNormalForm.beta : R

The generator beta in Gordon’s right normal form construction.

Equations

• Undecidability.Gordon.RightNormalForm.beta = Monoid.CoprodI.of (Multiplicative.ofAdd 1)

def Undecidability.Gordon.RightNormalForm.u (r : ℕ) : R

The conjugate beta⁻ʳ * b * betaʳ in the right-hand normal-form model.

Equations

• Undecidability.Gordon.RightNormalForm.u r = (Undecidability.Gordon.RightNormalForm.beta ^ r)⁻¹ * Undecidability.Gordon.RightNormalForm.b * Undecidability.Gordon.RightNormalForm.beta ^ r

def Undecidability.Gordon.RightNormalForm.elt {n : ℕ} : BasisIndex n → R

The right-hand proposed basis, represented in the indexed free product.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Gordon.RightNormalForm.elt Undecidability.Gordon.BasisIndex.conjugateA = Undecidability.Gordon.RightNormalForm.b ^ 2
• Undecidability.Gordon.RightNormalForm.elt (Undecidability.Gordon.BasisIndex.old i) = Undecidability.Gordon.RightNormalForm.u (↑i + 1)
• Undecidability.Gordon.RightNormalForm.elt Undecidability.Gordon.BasisIndex.commutator = Undecidability.Gordon.RightNormalForm.u (n + 1)

def Undecidability.Gordon.RightNormalForm.side {n : ℕ} : BasisIndex n → Fin 2

The free factor containing both endpoints of the normal-form block.

Equations

• Undecidability.Gordon.RightNormalForm.side Undecidability.Gordon.BasisIndex.conjugateA = 0
• Undecidability.Gordon.RightNormalForm.side Undecidability.Gordon.BasisIndex.conjugateAlpha = 0
• Undecidability.Gordon.RightNormalForm.side (Undecidability.Gordon.BasisIndex.old i) = 1
• Undecidability.Gordon.RightNormalForm.side Undecidability.Gordon.BasisIndex.commutator = 1

def Undecidability.Gordon.RightNormalForm.app {i j k l : Fin 2} (x : Monoid.CoprodI.NeWord (CyclicFamily 2) i j) (h : j ≠ k) (y : Monoid.CoprodI.NeWord (CyclicFamily 2) k l) : Monoid.CoprodI.NeWord (CyclicFamily 2) i l

Concatenate nonempty reduced words whose adjacent factor labels differ.

Equations

• Undecidability.Gordon.RightNormalForm.app x h y = x.append h y

def Undecidability.Gordon.RightNormalForm.blockA (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 0 0

The reduced block representing a power of the first basis element.

Equations

• Undecidability.Gordon.RightNormalForm.blockA k hk = Monoid.CoprodI.NeWord.singletonZ 0 (2 * k) ⋯

def Undecidability.Gordon.RightNormalForm.blockAlpha (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 0 0

The reduced block representing a power of the conjugated cyclic basis element.

Equations

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

def Undecidability.Gordon.RightNormalForm.oldExponent {n : ℕ} (i : Fin n) : ℤ

The positive exponent i + 1 assigned to an original generator.

Equations

• Undecidability.Gordon.RightNormalForm.oldExponent i = ↑↑i + 1

theorem Undecidability.Gordon.RightNormalForm.oldExponent_pos {n : ℕ} (i : Fin n) : 0 < oldExponent i

def Undecidability.Gordon.RightNormalForm.commutatorExponent (n : ℕ) : ℤ

The exponent n + 1 reserved for the distinguished commutator.

Equations

• Undecidability.Gordon.RightNormalForm.commutatorExponent n = ↑n + 1

theorem Undecidability.Gordon.RightNormalForm.commutatorExponent_pos (n : ℕ) : 0 < commutatorExponent n

def Undecidability.Gordon.RightNormalForm.blockU (r : ℤ) (hr : 0 < r) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 1 1

The reduced block conjugating a nonzero power by the indicated cyclic power.

Equations

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

def Undecidability.Gordon.RightNormalForm.blockOld {n : ℕ} (i : Fin n) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 1 1

The reduced block representing a power of the encoded original generator.

Equations

• Undecidability.Gordon.RightNormalForm.blockOld i k hk = Undecidability.Gordon.RightNormalForm.blockU (Undecidability.Gordon.RightNormalForm.oldExponent i) ⋯ k hk

def Undecidability.Gordon.RightNormalForm.blockCommutator (n : ℕ) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 1 1

The reduced block representing a power of the distinguished commutator element.

Equations

• Undecidability.Gordon.RightNormalForm.blockCommutator n k hk = Undecidability.Gordon.RightNormalForm.blockU (Undecidability.Gordon.RightNormalForm.commutatorExponent n) ⋯ k hk

def Undecidability.Gordon.RightNormalForm.block {n : ℕ} (i : BasisIndex n) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) (side i) (side i)

The reduced block associated with a basis element and a nonzero exponent.

Equations

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

@[simp]

theorem Undecidability.Gordon.RightNormalForm.block_prod {n : ℕ} (i : BasisIndex n) (k : ℤ) (hk : k ≠ 0) : (block i k hk).prod = elt i ^ k

def Undecidability.Gordon.RightNormalForm.headValue {n : ℕ} : BasisIndex n → ZMul → ZMul

The value prescribed for the first letter of a basis-power block.

Equations

• Undecidability.Gordon.RightNormalForm.headValue Undecidability.Gordon.BasisIndex.conjugateA x✝ = Multiplicative.ofAdd (2 * Multiplicative.toAdd x✝)
• Undecidability.Gordon.RightNormalForm.headValue Undecidability.Gordon.BasisIndex.conjugateAlpha x✝ = Multiplicative.ofAdd 1
• Undecidability.Gordon.RightNormalForm.headValue (Undecidability.Gordon.BasisIndex.old i) x✝ = Multiplicative.ofAdd (-Undecidability.Gordon.RightNormalForm.oldExponent i)
• Undecidability.Gordon.RightNormalForm.headValue Undecidability.Gordon.BasisIndex.commutator x✝ = Multiplicative.ofAdd (-Undecidability.Gordon.RightNormalForm.commutatorExponent n)

def Undecidability.Gordon.RightNormalForm.lastValue {n : ℕ} : BasisIndex n → ZMul → ZMul

The value prescribed for the last letter of a basis-power block.

Equations

• Undecidability.Gordon.RightNormalForm.lastValue Undecidability.Gordon.BasisIndex.conjugateA x✝ = Multiplicative.ofAdd (2 * Multiplicative.toAdd x✝)
• Undecidability.Gordon.RightNormalForm.lastValue Undecidability.Gordon.BasisIndex.conjugateAlpha x✝ = Multiplicative.ofAdd (-1)
• Undecidability.Gordon.RightNormalForm.lastValue (Undecidability.Gordon.BasisIndex.old i) x✝ = Multiplicative.ofAdd (Undecidability.Gordon.RightNormalForm.oldExponent i)
• Undecidability.Gordon.RightNormalForm.lastValue Undecidability.Gordon.BasisIndex.commutator x✝ = Multiplicative.ofAdd (Undecidability.Gordon.RightNormalForm.commutatorExponent n)

@[simp]

theorem Undecidability.Gordon.RightNormalForm.block_head {n : ℕ} (i : BasisIndex n) (k : ℤ) (hk : k ≠ 0) : (block i k hk).head = headValue i (Multiplicative.ofAdd k)

@[simp]

theorem Undecidability.Gordon.RightNormalForm.block_last {n : ℕ} (i : BasisIndex n) (k : ℤ) (hk : k ≠ 0) : (block i k hk).last = lastValue i (Multiplicative.ofAdd k)

theorem Undecidability.Gordon.RightNormalForm.side_eq_zero_iff {n : ℕ} (i : BasisIndex n) : side i = 0 ↔ i = BasisIndex.conjugateA ∨ i = BasisIndex.conjugateAlpha

theorem Undecidability.Gordon.RightNormalForm.block_append_or_small {n : ℕ} (i : BasisIndex n) (k : ℤ) (hk : k ≠ 0) : i = BasisIndex.conjugateA ∨ (block i k hk).IsAppend

def Undecidability.Gordon.RightNormalForm.GoodHead {n : ℕ} : BasisIndex n → ZMul → Prop

The initial letter satisfies the boundary condition for the specified basis element.

Equations

• Undecidability.Gordon.RightNormalForm.GoodHead Undecidability.Gordon.BasisIndex.conjugateA x✝ = (Multiplicative.toAdd x✝ ≠ 1)
• Undecidability.Gordon.RightNormalForm.GoodHead Undecidability.Gordon.BasisIndex.conjugateAlpha x✝ = (x✝ = Multiplicative.ofAdd 1)
• Undecidability.Gordon.RightNormalForm.GoodHead (Undecidability.Gordon.BasisIndex.old i) x✝ = (x✝ = Multiplicative.ofAdd (-Undecidability.Gordon.RightNormalForm.oldExponent i))
• Undecidability.Gordon.RightNormalForm.GoodHead Undecidability.Gordon.BasisIndex.commutator x✝ = (x✝ = Multiplicative.ofAdd (-Undecidability.Gordon.RightNormalForm.commutatorExponent n))

def Undecidability.Gordon.RightNormalForm.GoodLast {n : ℕ} : BasisIndex n → ZMul → Prop

The final letter satisfies the boundary condition for the specified basis element.

Equations

• Undecidability.Gordon.RightNormalForm.GoodLast Undecidability.Gordon.BasisIndex.conjugateA x✝ = (Multiplicative.toAdd x✝ ≠ -1)
• Undecidability.Gordon.RightNormalForm.GoodLast Undecidability.Gordon.BasisIndex.conjugateAlpha x✝ = (x✝ = Multiplicative.ofAdd (-1))
• Undecidability.Gordon.RightNormalForm.GoodLast (Undecidability.Gordon.BasisIndex.old i) x✝ = (x✝ = Multiplicative.ofAdd (Undecidability.Gordon.RightNormalForm.oldExponent i))
• Undecidability.Gordon.RightNormalForm.GoodLast Undecidability.Gordon.BasisIndex.commutator x✝ = (x✝ = Multiplicative.ofAdd (Undecidability.Gordon.RightNormalForm.commutatorExponent n))

@[simp]

theorem Undecidability.Gordon.RightNormalForm.goodHead_headValue {n : ℕ} (i : BasisIndex n) (x : ZMul) : GoodHead i (headValue i x)

@[simp]

theorem Undecidability.Gordon.RightNormalForm.goodLast_lastValue {n : ℕ} (i : BasisIndex n) (x : ZMul) : GoodLast i (lastValue i x)

theorem Undecidability.Gordon.RightNormalForm.boundary_ne_one {n : ℕ} (i j : BasisIndex n) (hij : i ≠ j) (hside : side i = side j) (x y : ZMul) (hx : GoodLast i x) (hy : GoodHead j y) : x * y ≠ 1

def Undecidability.Gordon.RightNormalForm.cyclicMap {n : ℕ} (i : BasisIndex n) : ZMul →* R

The homomorphism sending an integer exponent to a power of the corresponding basis element.

Equations

• Undecidability.Gordon.RightNormalForm.cyclicMap i = (zpowersHom Undecidability.Gordon.RightNormalForm.R) (Undecidability.Gordon.RightNormalForm.elt i)

def Undecidability.Gordon.RightNormalForm.lift (n : ℕ) : BasisCoprod n →* R

The homomorphism induced by the power maps for the proposed cyclic factors.

Equations

• Undecidability.Gordon.RightNormalForm.lift n = Monoid.CoprodI.lift Undecidability.Gordon.RightNormalForm.cyclicMap

structure Undecidability.Gordon.RightNormalForm.Image {n : ℕ} {i j : BasisIndex n} (w : Monoid.CoprodI.NeWord (BasisFamily n) i j) : Type

A reduced representative of a mapped word, together with its evaluation and boundary properties.

• word : Monoid.CoprodI.NeWord (CyclicFamily 2) (side i) (side j)

  The reduced-word representative carrying the stated evaluation and boundary properties.

• head_good : GoodHead i self.word.head
• last_good : GoodLast j self.word.last
• prod_eq : self.word.prod = (lift n) w.prod
• append_or_zero : i = BasisIndex.conjugateA ∧ j = BasisIndex.conjugateA ∨ self.word.IsAppend

noncomputable def Undecidability.Gordon.RightNormalForm.image {n : ℕ} {i j : BasisIndex n} (w : Monoid.CoprodI.NeWord (BasisFamily n) i j) : Image w

Construct the reduced image of an arbitrary nonempty source normal form.

Equations

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

theorem Undecidability.Gordon.RightNormalForm.lift_injective (n : ℕ) : Function.Injective ⇑(lift n)

def Undecidability.Gordon.RightNormalForm.freeMap (n : ℕ) : FreeGroup (BasisIndex n) →* R

The homomorphism freely extending the displayed group-valued basis.

Equations

• Undecidability.Gordon.RightNormalForm.freeMap n = FreeGroup.lift Undecidability.Gordon.RightNormalForm.elt

theorem Undecidability.Gordon.RightNormalForm.freeMap_eq (n : ℕ) : freeMap n = (lift n).comp (Monoid.CoprodI.intOfFree (BasisIndex n))

theorem Undecidability.Gordon.RightNormalForm.freeMap_injective (n : ℕ) : Function.Injective ⇑(freeMap n)

theorem Undecidability.Gordon.RightNormalForm.rightBasisMap_comp (n : ℕ) : (Monoid.CoprodI.intOfFree (Fin 2)).comp (rightBasisMap n) = freeMap n

theorem Undecidability.Gordon.rightBasisMap_injective (n : ℕ) : Function.Injective ⇑(rightBasisMap n)

Gordon's right-hand amalgamating words freely generate.