A mod-five quotient of Borisov's two-HNN group

Both stable letters act on the free product C₅ * C₅ by inverting each free factor. Since 4 = -1 (mod 5), the four power-conjugation relations of Gamma3 hold in the resulting semidirect product. This quotient is useful because every positive displayed rule contributes two nontrivial alternating free-product syllables.

@[reducible, inline]

abbrev Undecidability.BorisovModFiveQuotient.C5 : Type

The cyclic group of order five, written multiplicatively.

Equations

• Undecidability.BorisovModFiveQuotient.C5 = Multiplicative (ZMod 5)

@[reducible, inline]

abbrev Undecidability.BorisovModFiveQuotient.ModFiveBase : Type

The free product of the two order-five base factors.

Equations

• Undecidability.BorisovModFiveQuotient.ModFiveBase = Monoid.CoprodI fun (x : Fin 2) => Undecidability.BorisovModFiveQuotient.C5

def Undecidability.BorisovModFiveQuotient.c5Generator : C5

The standard generator of the multiplicative order-five cyclic group.

Equations

• Undecidability.BorisovModFiveQuotient.c5Generator = Multiplicative.ofAdd 1

def Undecidability.BorisovModFiveQuotient.modD : ModFiveBase

The generator of the first order-five factor, representing d.

Equations

• Undecidability.BorisovModFiveQuotient.modD = Monoid.CoprodI.of Undecidability.BorisovModFiveQuotient.c5Generator

def Undecidability.BorisovModFiveQuotient.modE : ModFiveBase

The generator of the second order-five factor, representing e.

Equations

• Undecidability.BorisovModFiveQuotient.modE = Monoid.CoprodI.of Undecidability.BorisovModFiveQuotient.c5Generator

def Undecidability.BorisovModFiveQuotient.c5Inverse : C5 →* C5

The inversion homomorphism of the abelian order-five cyclic group.

Equations

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

def Undecidability.BorisovModFiveQuotient.invertFactorsHom : ModFiveBase →* ModFiveBase

The homomorphism inverting both cyclic free-product factors.

Equations

• Undecidability.BorisovModFiveQuotient.invertFactorsHom = Monoid.CoprodI.lift fun (i : Fin 2) => Monoid.CoprodI.of.comp Undecidability.BorisovModFiveQuotient.c5Inverse

@[simp]

theorem Undecidability.BorisovModFiveQuotient.invertFactorsHom_of (i : Fin 2) (x : C5) : invertFactorsHom (Monoid.CoprodI.of x) = Monoid.CoprodI.of x⁻¹

theorem Undecidability.BorisovModFiveQuotient.invertFactorsHom_involutive (x : ModFiveBase) : invertFactorsHom (invertFactorsHom x) = x

def Undecidability.BorisovModFiveQuotient.invertFactors : MulAut ModFiveBase

The involutive automorphism inverting both cyclic free-product factors.

Equations

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

@[simp]

theorem Undecidability.BorisovModFiveQuotient.invertFactors_modD : invertFactors modD = modD⁻¹

@[simp]

theorem Undecidability.BorisovModFiveQuotient.invertFactors_modE : invertFactors modE = modE⁻¹

def Undecidability.BorisovModFiveQuotient.inversionAction : Multiplicative ℤ →* MulAut ModFiveBase

The infinite cyclic action generated by factorwise inversion. Using an infinite cyclic acting group avoids any quotient bookkeeping; the action still has period two because invertFactors is involutive.

Equations

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

@[reducible, inline]

abbrev Undecidability.BorisovModFiveQuotient.QuotientGroup : Type

The semidirect product of the order-five free product by simultaneous inversion.

Equations

• Undecidability.BorisovModFiveQuotient.QuotientGroup = (Undecidability.BorisovModFiveQuotient.ModFiveBase ⋊[Undecidability.BorisovModFiveQuotient.inversionAction] Multiplicative ℤ)

def Undecidability.BorisovModFiveQuotient.quotientBase : ModFiveBase →* QuotientGroup

The inclusion of the order-five free product into the semidirect product.

Equations

• Undecidability.BorisovModFiveQuotient.quotientBase = SemidirectProduct.inl

def Undecidability.BorisovModFiveQuotient.quotientStable : QuotientGroup

The semidirect-product stable generator implementing simultaneous inversion.

Equations

• Undecidability.BorisovModFiveQuotient.quotientStable = SemidirectProduct.inr (Multiplicative.ofAdd 1)

@[simp]

theorem Undecidability.BorisovModFiveQuotient.inversionAction_one : inversionAction (Multiplicative.ofAdd 1) = invertFactors

@[simp]

theorem Undecidability.BorisovModFiveQuotient.quotientStable_mul_base (x : ModFiveBase) : quotientStable * quotientBase x = quotientBase (invertFactors x) * quotientStable

def Undecidability.BorisovModFiveQuotient.baseModFive : BorisovHNNModel.Base →* ModFiveBase

The free-group homomorphism reducing both base generators modulo five.

Equations

• Undecidability.BorisovModFiveQuotient.baseModFive = FreeGroup.lift ![Undecidability.BorisovModFiveQuotient.modD, Undecidability.BorisovModFiveQuotient.modE]

@[simp]

theorem Undecidability.BorisovModFiveQuotient.baseModFive_d : baseModFive BorisovHNNModel.d = modD

@[simp]

theorem Undecidability.BorisovModFiveQuotient.baseModFive_e : baseModFive BorisovHNNModel.e = modE

theorem Undecidability.BorisovModFiveQuotient.modD_pow_four : modD ^ 4 = modD⁻¹

theorem Undecidability.BorisovModFiveQuotient.modE_pow_four : modE ^ 4 = modE⁻¹

theorem Undecidability.BorisovModFiveQuotient.baseModFive_beta_eq_invert_alpha (x : BorisovHNNModel.Base) : baseModFive (BorisovHNNModel.beta x) = invertFactors (baseModFive (BorisovHNNModel.alpha x))

def Undecidability.BorisovModFiveQuotient.baseToQuotient : BorisovHNNModel.Base →* QuotientGroup

The base-group homomorphism into the mod-five semidirect-product quotient.

Equations

• Undecidability.BorisovModFiveQuotient.baseToQuotient = Undecidability.BorisovModFiveQuotient.quotientBase.comp Undecidability.BorisovModFiveQuotient.baseModFive

theorem Undecidability.BorisovModFiveQuotient.stable_power_relation (x : BorisovHNNModel.Base) : quotientStable * baseToQuotient (BorisovHNNModel.alpha x) = baseToQuotient (BorisovHNNModel.beta x) * quotientStable

theorem Undecidability.BorisovModFiveQuotient.firstLiftCondition (a : ↥BorisovHNNModel.A0) : quotientStable * baseToQuotient ↑a = baseToQuotient ↑(BorisovHNNModel.phi0 a) * quotientStable

noncomputable def Undecidability.BorisovModFiveQuotient.stageOneToQuotient : BorisovHNNModel.Stage1 →* QuotientGroup

Extend the base quotient map across the first HNN extension.

Equations

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

@[simp]

theorem Undecidability.BorisovModFiveQuotient.stageOneToQuotient_of0 (x : BorisovHNNModel.Base) : stageOneToQuotient (BorisovHNNModel.of0 x) = baseToQuotient x

@[simp]

theorem Undecidability.BorisovModFiveQuotient.stageOneToQuotient_s1 : stageOneToQuotient BorisovHNNModel.s1 = quotientStable

theorem Undecidability.BorisovModFiveQuotient.secondLiftCondition (a : ↥BorisovHNNModel.A1) : quotientStable * stageOneToQuotient ↑a = stageOneToQuotient ↑(BorisovHNNModel.phi1 a) * quotientStable

noncomputable def Undecidability.BorisovModFiveQuotient.gamma3ToQuotient : BorisovHNNModel.Gamma3 →* QuotientGroup

Extend the quotient map across the second HNN extension.

Equations

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

@[simp]

theorem Undecidability.BorisovModFiveQuotient.gamma3ToQuotient_of1 (x : BorisovHNNModel.Stage1) : gamma3ToQuotient (BorisovHNNModel.of1 x) = stageOneToQuotient x

@[simp]

theorem Undecidability.BorisovModFiveQuotient.gamma3ToQuotient_d3 : gamma3ToQuotient BorisovHNNModel.d3 = quotientBase modD

@[simp]

theorem Undecidability.BorisovModFiveQuotient.gamma3ToQuotient_e3 : gamma3ToQuotient BorisovHNNModel.e3 = quotientBase modE

@[simp]

theorem Undecidability.BorisovModFiveQuotient.gamma3ToQuotient_s1 : gamma3ToQuotient BorisovHNNModel.firstStableInStageThree = quotientStable

@[simp]

theorem Undecidability.BorisovModFiveQuotient.gamma3ToQuotient_s2 : gamma3ToQuotient BorisovHNNModel.secondStableInStageThree = quotientStable