The shared right factor, free basis and lift used by the amalgam and normal-form models.

@[reducible, inline]

abbrev Undecidability.MillerTancer.RightFactor : Type

The right free factor used to construct the amalgam.

Equations

• Undecidability.MillerTancer.RightFactor = FreeGroup (Fin 2)

def Undecidability.MillerTancer.rightBeta : RightFactor

The right-factor free generator beta.

Equations

• Undecidability.MillerTancer.rightBeta = FreeGroup.of 0

def Undecidability.MillerTancer.rightGamma : RightFactor

The right-factor free generator gamma.

Equations

• Undecidability.MillerTancer.rightGamma = FreeGroup.of 1

def Undecidability.MillerTancer.rightBasis : Fin 5 → RightFactor

The five right-hand amalgamating generators of the Miller–Tancer construction.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.MillerTancer.rightBasis 0 = Undecidability.MillerTancer.rightBeta
• Undecidability.MillerTancer.rightBasis 3 = (Undecidability.MillerTancer.rightGamma ^ 3)⁻¹ * Undecidability.MillerTancer.rightBeta * Undecidability.MillerTancer.rightGamma ^ 3
• Undecidability.MillerTancer.rightBasis 4 = (Undecidability.MillerTancer.rightGamma ^ 4)⁻¹ * Undecidability.MillerTancer.rightBeta * Undecidability.MillerTancer.rightGamma ^ 4

def Undecidability.MillerTancer.rightBasisMap : FreeGroup (Fin 5) →* RightFactor

The homomorphism freely extending the five right-hand amalgamating generators.

Equations

• Undecidability.MillerTancer.rightBasisMap = FreeGroup.lift Undecidability.MillerTancer.rightBasis