Comparison between the two equivalent models of the left factor used in the Miller--Tancer amalgam argument.

Amalgam.LeftFactor P is the paper-like bracketing P.Group * FreeGroup {alpha, beta},

whereas LeftNormalForm.MillerLeft P.Group brackets the same three free factors as (P.Group * <beta>) * <alpha>.

For the injectivity argument we only need the canonical homomorphism from the first model to the second and its action on the five distinguished elements.

def Undecidability.MillerTancer.LeftBridge.oldToMiller {n m : ℕ} (P : FP n m) : P.Group →* LeftNormalForm.MillerLeft P.Group

The old presented group included into the base of the nested model.

Equations

• Undecidability.MillerTancer.LeftBridge.oldToMiller P = Monoid.CoprodI.of.comp Monoid.CoprodI.of

def Undecidability.MillerTancer.LeftBridge.newToMiller {n m : ℕ} (P : FP n m) : FreeGroup (Fin 2) →* LeftNormalForm.MillerLeft P.Group

Send the two new generators of the paper-like left factor to the corresponding alpha and beta in the nested normal-form model.

Equations

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

def Undecidability.MillerTancer.LeftBridge.comparison {n m : ℕ} (P : FP n m) : Amalgam.LeftFactor P →* LeftNormalForm.MillerLeft P.Group

Reassociate the left factor, with the generator convention required by the five basis elements.

Equations

• Undecidability.MillerTancer.LeftBridge.comparison P = Monoid.Coprod.lift (Undecidability.MillerTancer.LeftBridge.oldToMiller P) (Undecidability.MillerTancer.LeftBridge.newToMiller P)

@[simp]

theorem Undecidability.MillerTancer.LeftBridge.comparison_old {n m : ℕ} (P : FP n m) (g : P.Group) : (comparison P) ((Amalgam.oldLeft P) g) = LeftNormalForm.baseOf (LeftNormalForm.old g)

@[simp]

theorem Undecidability.MillerTancer.LeftBridge.comparison_alpha {n m : ℕ} (P : FP n m) : (comparison P) (Amalgam.alphaLeft P) = LeftNormalForm.outerAlpha

@[simp]

theorem Undecidability.MillerTancer.LeftBridge.comparison_beta {n m : ℕ} (P : FP n m) : (comparison P) (Amalgam.betaLeft P) = LeftNormalForm.baseOf LeftNormalForm.beta

@[simp]

theorem Undecidability.MillerTancer.LeftBridge.baseOf_mul {n m : ℕ} (P : FP n m) (x y : LeftNormalForm.LeftProduct P.Group) : LeftNormalForm.baseOf (x * y) = LeftNormalForm.baseOf x * LeftNormalForm.baseOf y

theorem Undecidability.MillerTancer.LeftBridge.comparison_leftBasis {n m : ℕ} (P : FP n m) (z w : Word n) (i : Fin 5) : (comparison P) (Amalgam.leftBasis P z w i) = LeftNormalForm.outerLeftBasis (P.evalWord w) (P.evalWord z) i

The comparison sends the paper's five left-hand amalgamating elements to the exact five elements used by the nested normal-form proof.

theorem Undecidability.MillerTancer.LeftBridge.comparison_comp_leftMap {n m : ℕ} (P : FP n m) (z w : Word n) : (comparison P).comp (Amalgam.leftMap P z w) = FreeGroup.lift (LeftNormalForm.outerLeftBasis (P.evalWord w) (P.evalWord z))

theorem Undecidability.MillerTancer.LeftBridge.leftMap_injective_of_outerLeftBasis_injective {n m : ℕ} (P : FP n m) (z w : Word n) (hinj : Function.Injective ⇑(FreeGroup.lift (LeftNormalForm.outerLeftBasis (P.evalWord w) (P.evalWord z)))) : Function.Injective ⇑(Amalgam.leftMap P z w)

Injectivity in the nested normal-form model implies injectivity of the paper-like left map.

The nontrivial half of the Miller--Tancer construction, specialized to one extra relation z that normally generates the old group.

The two lists of five words freely generate subgroups of the left and right factors. Identifying those subgroups forms a free product with amalgamation. The old group embeds in that pushout, so a nontrivial w remains nontrivial after the four new relations are imposed.

theorem Undecidability.MillerTancer.pushout_rightMap_eq : Amalgam.rightMap = rightBasisMap

Both models use the same shared right-basis lift.

theorem Undecidability.MillerTancer.pushout_rightMap_injective : Function.Injective ⇑Amalgam.rightMap

theorem Undecidability.MillerTancer.transform_not_trivial_of_leftMap_injective {n m : ℕ} (P : FP n m) (z w : Word n) (hleft : Function.Injective ⇑(Amalgam.leftMap P z w)) (hw : ¬P.wordProblem w) : ¬(transform P z w).presentsTrivial

Reduce the nontriviality implication to injectivity of the left list of five amalgamating words.

theorem Undecidability.MillerTancer.transform_not_trivial_of_not_wordProblem {n m : ℕ} (P : FP n m) (z w : Word n) (hw : ¬P.wordProblem w) : ¬(transform P z w).presentsTrivial

If w is nontrivial in the old presentation, its transformed presentation is nontrivial. This is the amalgamated-free-product argument in the proof of Tancer's Theorem 9, for the Miller commutator variant used in the paper.