Normal-form infrastructure for the left separated-conjugates map.

theorem Undecidability.MillerTancer.LeftNormalForm.FreeGroup.lift_injective_of_coprodI_neWord {I Q : Type} [Group Q] (a : I → Q) (hne : ∀ (i j : I) (u : Monoid.CoprodI.NeWord (fun (x : I) => FreeGroup Unit) i j), (Monoid.CoprodI.lift fun (i : I) => FreeGroup.lift fun (x : Unit) => a i) u.prod ≠ 1) : Function.Injective ⇑(FreeGroup.lift a)

theorem Undecidability.MillerTancer.LeftNormalForm.FreeGroup.lift_injective_of_reduced_zpow_products {I Q : Type} [Group Q] (a : I → Q) (hprod : ∀ (l : List (I × ℤ)), l ≠ [] → (∀ p ∈ l, p.2 ≠ 0) → List.IsChain (fun (p q : I × ℤ) => p.1 ≠ q.1) l → (List.map (fun (p : I × ℤ) => a p.1 ^ p.2) l).prod ≠ 1) : Function.Injective ⇑(FreeGroup.lift a)

A list-of-nonzero-powers formulation of the normal-form criterion. This is the form used by the separated-conjugates calculation: adjacent runs use different proposed basis elements.

inductive Undecidability.MillerTancer.LeftNormalForm.LeftIndex : Type

The labels of the original group and the two cyclic factors.

• old : LeftIndex
• alpha : LeftIndex
• beta : LeftIndex

@[instance_reducible]

instance Undecidability.MillerTancer.LeftNormalForm.instDecidableEqLeftIndex : DecidableEq LeftIndex

Equations

• Undecidability.MillerTancer.LeftNormalForm.instDecidableEqLeftIndex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Undecidability.MillerTancer.LeftNormalForm.LeftFactor (G : Type) : LeftIndex → Type

The original group or cyclic group corresponding to a left-factor label.

Equations

• Undecidability.MillerTancer.LeftNormalForm.LeftFactor G Undecidability.MillerTancer.LeftNormalForm.LeftIndex.old = G
• Undecidability.MillerTancer.LeftNormalForm.LeftFactor G Undecidability.MillerTancer.LeftNormalForm.LeftIndex.alpha = FreeGroup Unit
• Undecidability.MillerTancer.LeftNormalForm.LeftFactor G Undecidability.MillerTancer.LeftNormalForm.LeftIndex.beta = FreeGroup Unit

@[instance_reducible]

instance Undecidability.MillerTancer.LeftNormalForm.leftFactorGroup {G : Type} [Group G] (i : LeftIndex) : Group (LeftFactor G i)

Equations

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

@[reducible, inline]

abbrev Undecidability.MillerTancer.LeftNormalForm.LeftProduct (G : Type) [Group G] : Type

The indexed free product separating the original group and the cyclic factors.

Equations

• Undecidability.MillerTancer.LeftNormalForm.LeftProduct G = Monoid.CoprodI (Undecidability.MillerTancer.LeftNormalForm.LeftFactor G)

def Undecidability.MillerTancer.LeftNormalForm.old {G : Type} [Group G] (g : G) : LeftProduct G

The inclusion of the original group into the indexed free product.

Equations

• Undecidability.MillerTancer.LeftNormalForm.old g = Monoid.CoprodI.of g

def Undecidability.MillerTancer.LeftNormalForm.alpha {G : Type} [Group G] : LeftProduct G

The generator of the cyclic factor labeled alpha.

Equations

• Undecidability.MillerTancer.LeftNormalForm.alpha = Monoid.CoprodI.of (FreeGroup.of ())

def Undecidability.MillerTancer.LeftNormalForm.beta {G : Type} [Group G] : LeftProduct G

The generator beta in Miller–Tancer’s left normal form construction.

Equations

• Undecidability.MillerTancer.LeftNormalForm.beta = Monoid.CoprodI.of (FreeGroup.of ())

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.of_inv {G : Type} [Group G] {i : LeftIndex} (x : LeftFactor G i) : Monoid.CoprodI.of x⁻¹ = (Monoid.CoprodI.of x)⁻¹

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.old_inv {G : Type} [Group G] (g : G) : old g⁻¹ = (old g)⁻¹

theorem Undecidability.MillerTancer.LeftNormalForm.freeGenerator_ne_one : FreeGroup.of () ≠ 1

theorem Undecidability.MillerTancer.LeftNormalForm.beta_ne_one {G : Type} [Group G] : beta ≠ 1

def Undecidability.MillerTancer.LeftNormalForm.leftFactorToBeta {G : Type} [Group G] (i : LeftIndex) : LeftFactor G i →* FreeGroup Unit

The component maps retaining the beta factor and killing the other factors.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.MillerTancer.LeftNormalForm.leftFactorToBeta Undecidability.MillerTancer.LeftNormalForm.LeftIndex.old = 1
• Undecidability.MillerTancer.LeftNormalForm.leftFactorToBeta Undecidability.MillerTancer.LeftNormalForm.LeftIndex.alpha = 1

def Undecidability.MillerTancer.LeftNormalForm.betaProjection {G : Type} [Group G] : LeftProduct G →* FreeGroup Unit

The projection onto the beta cyclic factor.

Equations

• Undecidability.MillerTancer.LeftNormalForm.betaProjection = Monoid.CoprodI.lift Undecidability.MillerTancer.LeftNormalForm.leftFactorToBeta

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.betaProjection_old {G : Type} [Group G] (g : G) : betaProjection (old g) = 1

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.betaProjection_beta {G : Type} [Group G] : betaProjection beta = FreeGroup.of ()

theorem Undecidability.MillerTancer.LeftNormalForm.beta_zpow_ne_one {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : beta ^ k ≠ 1

theorem Undecidability.MillerTancer.LeftNormalForm.old_mul_beta_ne_one {G : Type} [Group G] (z : G) : old z * beta ≠ 1

theorem Undecidability.MillerTancer.LeftNormalForm.beta_mul_old_mul_beta_ne_one {G : Type} [Group G] (z : G) : beta * (old z * beta) ≠ 1

theorem Undecidability.MillerTancer.LeftNormalForm.inv_old_mul_beta_inv_mul_beta_inv_ne_one {G : Type} [Group G] (z : G) : (old z * beta)⁻¹ * beta⁻¹ ≠ 1

The inner commutator is cyclically reduced of free-product length four.

def Undecidability.MillerTancer.LeftNormalForm.commutatorWord {G : Type} [Group G] (w : G) (hw : w ≠ 1) : Monoid.CoprodI.NeWord (LeftFactor G) LeftIndex.old LeftIndex.beta

The nonempty reduced word representing the distinguished commutator.

Equations

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

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.commutatorWord_prod {G : Type} [Group G] (w : G) (hw : w ≠ 1) : (commutatorWord w hw).prod = (old w)⁻¹ * beta⁻¹ * old w * beta

Powers of a cyclically reduced nonempty free-product word are nonempty. This is the first reusable normal-form lemma needed for L₃.

def Undecidability.MillerTancer.LeftNormalForm.positivePowerWord {G : Type} [Group G] {i j : LeftIndex} (u : Monoid.CoprodI.NeWord (LeftFactor G) i j) (hij : j ≠ i) (k : ℕ) : Monoid.CoprodI.NeWord (LeftFactor G) i j

The reduced word representing a positive power of a cyclically reduced word.

Equations

• Undecidability.MillerTancer.LeftNormalForm.positivePowerWord u hij 0 = u
• Undecidability.MillerTancer.LeftNormalForm.positivePowerWord u hij k.succ = (Undecidability.MillerTancer.LeftNormalForm.positivePowerWord u hij k).append hij u

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.positivePowerWord_prod {G : Type} [Group G] {i j : LeftIndex} (u : Monoid.CoprodI.NeWord (LeftFactor G) i j) (hij : j ≠ i) (k : ℕ) : (positivePowerWord u hij k).prod = u.prod ^ (k + 1)

theorem Undecidability.MillerTancer.LeftNormalForm.positivePowerWord_prod_ne_one {G : Type} [Group G] {i j : LeftIndex} (u : Monoid.CoprodI.NeWord (LeftFactor G) i j) (hij : j ≠ i) (k : ℕ) : u.prod ^ (k + 1) ≠ 1

theorem Undecidability.MillerTancer.LeftNormalForm.zpow_ne_one_of_cyclicallyReduced {G : Type} [Group G] {i j : LeftIndex} (u : Monoid.CoprodI.NeWord (LeftFactor G) i j) (hij : j ≠ i) (k : ℤ) (hk : k ≠ 0) : u.prod ^ k ≠ 1

theorem Undecidability.MillerTancer.LeftNormalForm.commutator_zpow_ne_one {G : Type} [Group G] (w : G) (hw : w ≠ 1) (k : ℤ) (hk : k ≠ 0) : ((old w)⁻¹ * beta⁻¹ * old w * beta) ^ k ≠ 1

A nested two-factor presentation is convenient for the outer alpha normal-form calculation. LeftProduct G is used as the base factor; its extra unused free generator is harmless.

inductive Undecidability.MillerTancer.LeftNormalForm.OuterIndex : Type

The labels of the base factor and the outer conjugating cyclic factor.

• base : OuterIndex
• alpha : OuterIndex

@[instance_reducible]

instance Undecidability.MillerTancer.LeftNormalForm.instDecidableEqOuterIndex : DecidableEq OuterIndex

Equations

• Undecidability.MillerTancer.LeftNormalForm.instDecidableEqOuterIndex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Undecidability.MillerTancer.LeftNormalForm.OuterFactor (G : Type) [Group G] : OuterIndex → Type

The group corresponding to the base or outer cyclic factor.

Equations

• Undecidability.MillerTancer.LeftNormalForm.OuterFactor G Undecidability.MillerTancer.LeftNormalForm.OuterIndex.base = Undecidability.MillerTancer.LeftNormalForm.LeftProduct G
• Undecidability.MillerTancer.LeftNormalForm.OuterFactor G Undecidability.MillerTancer.LeftNormalForm.OuterIndex.alpha = FreeGroup Unit

@[reducible]

instance Undecidability.MillerTancer.LeftNormalForm.outerFactorGroup {G : Type} [Group G] (i : OuterIndex) : Group (OuterFactor G i)

Equations

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

@[reducible, inline]

abbrev Undecidability.MillerTancer.LeftNormalForm.MillerLeft (G : Type) [Group G] : Type

The outer free product separating the conjugating generator from the base group.

Equations

• Undecidability.MillerTancer.LeftNormalForm.MillerLeft G = Monoid.CoprodI (Undecidability.MillerTancer.LeftNormalForm.OuterFactor G)

def Undecidability.MillerTancer.LeftNormalForm.baseOf {G : Type} [Group G] (x : LeftProduct G) : MillerLeft G

The inclusion of the base free product into the outer free product.

Equations

• Undecidability.MillerTancer.LeftNormalForm.baseOf x = Monoid.CoprodI.of x

def Undecidability.MillerTancer.LeftNormalForm.outerAlpha {G : Type} [Group G] : MillerLeft G

The generator of the outer cyclic factor.

Equations

• Undecidability.MillerTancer.LeftNormalForm.outerAlpha = Monoid.CoprodI.of (FreeGroup.of ())

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.baseOf_inv {G : Type} [Group G] (x : LeftProduct G) : baseOf x⁻¹ = (baseOf x)⁻¹

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.baseOf_zpow {G : Type} [Group G] (x : LeftProduct G) (k : ℤ) : baseOf (x ^ k) = baseOf x ^ k

def Undecidability.MillerTancer.LeftNormalForm.outerLeftBasis {G : Type} [Group G] (w z : G) : Fin 5 → MillerLeft G

The five proposed left-hand amalgamating generators in the outer free product.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.MillerTancer.LeftNormalForm.outerLeftBasis w z 0 = Undecidability.MillerTancer.LeftNormalForm.baseOf Undecidability.MillerTancer.LeftNormalForm.beta

def Undecidability.MillerTancer.LeftNormalForm.baseSingleton {G : Type} [Group G] (x : LeftProduct G) (hx : x ≠ 1) : Monoid.CoprodI.NeWord (OuterFactor G) OuterIndex.base OuterIndex.base

The one-letter reduced word for a nonidentity base-group element.

Equations

• Undecidability.MillerTancer.LeftNormalForm.baseSingleton x hx = Monoid.CoprodI.NeWord.singleton x hx

def Undecidability.MillerTancer.LeftNormalForm.alphaSingleton {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (OuterFactor G) OuterIndex.alpha OuterIndex.alpha

The one-letter reduced word in the alpha factor.

Equations

• Undecidability.MillerTancer.LeftNormalForm.alphaSingleton k hk = Monoid.CoprodI.NeWord.singleton (FreeGroup.of () ^ k) ⋯

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.baseSingleton_prod {G : Type} [Group G] (x : LeftProduct G) (hx : x ≠ 1) : (baseSingleton x hx).prod = baseOf x

@[simp]

theorem Undecidability.MillerTancer.LeftNormalForm.alphaSingleton_prod {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : (alphaSingleton k hk).prod = outerAlpha ^ k

def Undecidability.MillerTancer.LeftNormalForm.leftPowerWord1 {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (OuterFactor G) OuterIndex.alpha OuterIndex.alpha

The reduced block representing a power of the first conjugated left generator.

Equations

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

def Undecidability.MillerTancer.LeftNormalForm.leftPowerWord2 {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (OuterFactor G) OuterIndex.alpha OuterIndex.alpha

The reduced block representing a power of the second conjugated left generator.

Equations

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

def Undecidability.MillerTancer.LeftNormalForm.leftPowerWord3 {G : Type} [Group G] (w : G) (hw : w ≠ 1) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (OuterFactor G) OuterIndex.alpha OuterIndex.alpha

The reduced block representing a power of the commutator-conjugated left generator.

Equations

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

theorem Undecidability.MillerTancer.LeftNormalForm.leftPowerWord1_prod {G : Type} [Group G] (w z : G) (k : ℤ) (hk : k ≠ 0) : (leftPowerWord1 k hk).prod = outerLeftBasis w z 1 ^ k

theorem Undecidability.MillerTancer.LeftNormalForm.leftPowerWord2_prod {G : Type} [Group G] (w z : G) (k : ℤ) (hk : k ≠ 0) : (leftPowerWord2 k hk).prod = outerLeftBasis w z 2 ^ k

theorem Undecidability.MillerTancer.LeftNormalForm.leftPowerWord3_prod {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (k : ℤ) (hk : k ≠ 0) : (leftPowerWord3 w hw k hk).prod = outerLeftBasis w z 3 ^ k