The final, formal bookkeeping step in the left separated-conjugates lemma.

Generator 0 is split off from generators 1, ..., 4. Its nonzero powers have outer normal form from the base factor to the base factor. The remaining four generators are assumed to send every nontrivial word to a normal form from the alpha factor to the alpha factor. Alternating words in the resulting two-factor coproduct are therefore reduced.

inductive Undecidability.MillerTancer.LeftSplit.SplitIndex : Type

The first-generator and four-generator-tail components of the source free group.

• zero : SplitIndex
• tail : SplitIndex

@[implicit_reducible]

def Undecidability.MillerTancer.LeftSplit.SplitFactor : SplitIndex → Type

The cyclic first-generator factor or the free four-generator tail factor.

Equations

• Undecidability.MillerTancer.LeftSplit.SplitFactor Undecidability.MillerTancer.LeftSplit.SplitIndex.zero = FreeGroup Unit
• Undecidability.MillerTancer.LeftSplit.SplitFactor Undecidability.MillerTancer.LeftSplit.SplitIndex.tail = FreeGroup (Fin 4)

@[instance_reducible]

instance Undecidability.MillerTancer.LeftSplit.splitFactorGroup (i : SplitIndex) : Group (SplitFactor i)

Equations

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

@[reducible, inline]

abbrev Undecidability.MillerTancer.LeftSplit.SplitProduct : Type

The free product separating the first source generator from its four-generator tail.

Equations

• Undecidability.MillerTancer.LeftSplit.SplitProduct = Monoid.CoprodI Undecidability.MillerTancer.LeftSplit.SplitFactor

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

The four proposed basis elements remaining after separating the first generator.

Equations

• Undecidability.MillerTancer.LeftSplit.tailBasis w z i = Undecidability.MillerTancer.LeftNormalForm.outerLeftBasis w z i.succ

def Undecidability.MillerTancer.LeftSplit.tailMap {G : Type} [Group G] (w z : G) : FreeGroup (Fin 4) →* LeftNormalForm.MillerLeft G

The homomorphism freely extending the four-generator tail basis.

Equations

• Undecidability.MillerTancer.LeftSplit.tailMap w z = FreeGroup.lift (Undecidability.MillerTancer.LeftSplit.tailBasis w z)

def Undecidability.MillerTancer.LeftSplit.zeroMap {G : Type} [Group G] : FreeGroup Unit →* LeftNormalForm.MillerLeft G

The homomorphism sending the first cyclic generator to the base letter beta.

Equations

• Undecidability.MillerTancer.LeftSplit.zeroMap = FreeGroup.lift fun (x : Unit) => Undecidability.MillerTancer.LeftNormalForm.baseOf Undecidability.MillerTancer.LeftNormalForm.beta

def Undecidability.MillerTancer.LeftSplit.splitFactorMap {G : Type} [Group G] (w z : G) (i : SplitIndex) : SplitFactor i →* LeftNormalForm.MillerLeft G

The component homomorphisms from the separated source factors.

Equations

• Undecidability.MillerTancer.LeftSplit.splitFactorMap w z Undecidability.MillerTancer.LeftSplit.SplitIndex.zero = Undecidability.MillerTancer.LeftSplit.zeroMap
• Undecidability.MillerTancer.LeftSplit.splitFactorMap w z Undecidability.MillerTancer.LeftSplit.SplitIndex.tail = Undecidability.MillerTancer.LeftSplit.tailMap w z

def Undecidability.MillerTancer.LeftSplit.splitLift {G : Type} [Group G] (w z : G) : SplitProduct →* LeftNormalForm.MillerLeft G

The homomorphism induced by the separated first-generator and tail maps.

Equations

• Undecidability.MillerTancer.LeftSplit.splitLift w z = Monoid.CoprodI.lift (Undecidability.MillerTancer.LeftSplit.splitFactorMap w z)

def Undecidability.MillerTancer.LeftSplit.splitSide : SplitIndex → LeftNormalForm.OuterIndex

The endpoint factor corresponding to a separated source-factor label.

Equations

• Undecidability.MillerTancer.LeftSplit.splitSide Undecidability.MillerTancer.LeftSplit.SplitIndex.zero = Undecidability.MillerTancer.LeftNormalForm.OuterIndex.base
• Undecidability.MillerTancer.LeftSplit.splitSide Undecidability.MillerTancer.LeftSplit.SplitIndex.tail = Undecidability.MillerTancer.LeftNormalForm.OuterIndex.alpha

theorem Undecidability.MillerTancer.LeftSplit.splitSide_ne {i j : SplitIndex} (hij : i ≠ j) : splitSide i ≠ splitSide j

theorem Undecidability.MillerTancer.LeftSplit.unitExponent_ne_zero (x : FreeGroup Unit) (hx : x ≠ 1) : FreeGroup.freeGroupUnitEquivInt x ≠ 0

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

The reduced image of a nonidentity element of the first cyclic source factor.

Equations

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

@[simp]

theorem Undecidability.MillerTancer.LeftSplit.zeroImage_prod {G : Type} [Group G] (x : FreeGroup Unit) (hx : x ≠ 1) : (zeroImage x hx).prod = zeroMap x

structure Undecidability.MillerTancer.LeftSplit.Image {G : Type} [Group G] (w z : G) (tailImage : (x : FreeGroup (Fin 4)) → x ≠ 1 → Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha) {i j : SplitIndex} (u : Monoid.CoprodI.NeWord SplitFactor i j) : Type

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

• word : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) (splitSide i) (splitSide j)

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

• prod_eq : self.word.prod = (splitLift w z) u.prod

noncomputable def Undecidability.MillerTancer.LeftSplit.image {G : Type} [Group G] (w z : G) (tailImage : (x : FreeGroup (Fin 4)) → x ≠ 1 → Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha) (tailImage_prod : ∀ (x : FreeGroup (Fin 4)) (hx : x ≠ 1), (tailImage x hx).prod = (tailMap w z) x) {i j : SplitIndex} (u : Monoid.CoprodI.NeWord SplitFactor i j) : Image w z tailImage u

Construct the reduced image using the first-factor word and the supplied tail images.

Equations

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

theorem Undecidability.MillerTancer.LeftSplit.splitLift_injective_of_tailImage {G : Type} [Group G] (w z : G) (tailImage : (x : FreeGroup (Fin 4)) → x ≠ 1 → Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha) (tailImage_prod : ∀ (x : FreeGroup (Fin 4)) (hx : x ≠ 1), (tailImage x hx).prod = (tailMap w z) x) : Function.Injective ⇑(splitLift w z)

def Undecidability.MillerTancer.LeftSplit.splitGenerator : Fin 5 → SplitProduct

The five source generators interpreted in the separated free product.

Equations

• Undecidability.MillerTancer.LeftSplit.splitGenerator 0 = Monoid.CoprodI.of (FreeGroup.of ())
• Undecidability.MillerTancer.LeftSplit.splitGenerator ⟨n.succ, h⟩ = Monoid.CoprodI.of (FreeGroup.of ⟨n, ⋯⟩)

def Undecidability.MillerTancer.LeftSplit.sourceSplit : FreeGroup (Fin 5) →* SplitProduct

The homomorphism separating the first source generator from the remaining four.

Equations

• Undecidability.MillerTancer.LeftSplit.sourceSplit = FreeGroup.lift Undecidability.MillerTancer.LeftSplit.splitGenerator

def Undecidability.MillerTancer.LeftSplit.zeroJoin : FreeGroup Unit →* FreeGroup (Fin 5)

The inclusion of the first cyclic factor into the five-generator free group.

Equations

• Undecidability.MillerTancer.LeftSplit.zeroJoin = FreeGroup.lift fun (x : Unit) => FreeGroup.of 0

def Undecidability.MillerTancer.LeftSplit.tailJoin : FreeGroup (Fin 4) →* FreeGroup (Fin 5)

The inclusion of the four-generator tail into the five-generator free group.

Equations

• Undecidability.MillerTancer.LeftSplit.tailJoin = FreeGroup.lift fun (i : Fin 4) => FreeGroup.of i.succ

def Undecidability.MillerTancer.LeftSplit.sourceJoin : SplitProduct →* FreeGroup (Fin 5)

The homomorphism recombining the separated source factors.

Equations

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

theorem Undecidability.MillerTancer.LeftSplit.sourceJoin_comp_sourceSplit : sourceJoin.comp sourceSplit = MonoidHom.id (FreeGroup (Fin 5))

theorem Undecidability.MillerTancer.LeftSplit.sourceSplit_injective : Function.Injective ⇑sourceSplit

theorem Undecidability.MillerTancer.LeftSplit.splitLift_comp_sourceSplit {G : Type} [Group G] (w z : G) : (splitLift w z).comp sourceSplit = FreeGroup.lift (LeftNormalForm.outerLeftBasis w z)

theorem Undecidability.MillerTancer.LeftSplit.outerLeftBasis_injective_of_tailImage {G : Type} [Group G] (w z : G) (tailImage : (x : FreeGroup (Fin 4)) → x ≠ 1 → Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha) (tailImage_prod : ∀ (x : FreeGroup (Fin 4)) (hx : x ≠ 1), (tailImage x hx).prod = (tailMap w z) x) : Function.Injective ⇑(FreeGroup.lift (LeftNormalForm.outerLeftBasis w z))

Reduce the five-generator left-basis check to normal forms for the tail four-generator map.