The four-relator Borisov group as an iterated HNN extension

This file gives a public HNN model for the presentation called BorisovIntersections.G0. The orientation of the final equivalence is

  BorisovIntersections.G0 ≃* G0HNN.

The two power embeddings of the rank-two free group are

  rightPowerMap : d ↦ d,   e ↦ e⁴,
  leftPowerMap  : d ↦ d⁴, e ↦ e.

Thus each HNN stable letter satisfies s * d = d⁴ * s and s * e⁴ = e * s, equivalently the two displayed relators in the paper.

Public HNN-model API

@[reducible, inline]

abbrev Undecidability.BorisovG0HNN.Base : Type

The free base group on the generators d and e.

Equations

• Undecidability.BorisovG0HNN.Base = Undecidability.BorisovHNNModel.Base

def Undecidability.BorisovG0HNN.baseD : Base

The first free base generator d.

Equations

• Undecidability.BorisovG0HNN.baseD = Undecidability.BorisovHNNModel.d

def Undecidability.BorisovG0HNN.baseE : Base

The second free base generator e.

Equations

• Undecidability.BorisovG0HNN.baseE = Undecidability.BorisovHNNModel.e

def Undecidability.BorisovG0HNN.rightPowerMap : Base →* Base

The injective base substitution fixing d and taking e to its fourth power.

Equations

• Undecidability.BorisovG0HNN.rightPowerMap = Undecidability.BorisovHNNModel.alpha

def Undecidability.BorisovG0HNN.leftPowerMap : Base →* Base

The injective base substitution taking d to its fourth power and fixing e.

Equations

• Undecidability.BorisovG0HNN.leftPowerMap = Undecidability.BorisovHNNModel.beta

@[reducible, inline]

abbrev Undecidability.BorisovG0HNN.G1 : Type

The first HNN-extension stage over the free base group.

Equations

• Undecidability.BorisovG0HNN.G1 = Undecidability.BorisovHNNModel.Stage1

@[reducible, inline]

abbrev Undecidability.BorisovG0HNN.G0HNN : Type

The two-HNN-extension model of the initial Borisov group.

Equations

• Undecidability.BorisovG0HNN.G0HNN = Undecidability.BorisovHNNModel.Gamma3

noncomputable def Undecidability.BorisovG0HNN.baseToG1 : Base →* G1

The inclusion of the free base group into the first HNN extension.

Equations

• Undecidability.BorisovG0HNN.baseToG1 = Undecidability.BorisovHNNModel.of0

noncomputable def Undecidability.BorisovG0HNN.g1ToG0HNN : G1 →* G0HNN

The inclusion of the first HNN extension into the second one.

Equations

• Undecidability.BorisovG0HNN.g1ToG0HNN = Undecidability.BorisovHNNModel.of1

noncomputable def Undecidability.BorisovG0HNN.baseToG0HNN : Base →* G0HNN

The composite inclusion of the free base group into the two-HNN-extension model.

Equations

• Undecidability.BorisovG0HNN.baseToG0HNN = Undecidability.BorisovG0HNN.g1ToG0HNN.comp Undecidability.BorisovG0HNN.baseToG1

noncomputable def Undecidability.BorisovG0HNN.hnnD : G0HNN

The image of d in the two-HNN-extension model.

Equations

• Undecidability.BorisovG0HNN.hnnD = Undecidability.BorisovHNNModel.d3

noncomputable def Undecidability.BorisovG0HNN.hnnE : G0HNN

The image of e in the two-HNN-extension model.

Equations

• Undecidability.BorisovG0HNN.hnnE = Undecidability.BorisovHNNModel.e3

noncomputable def Undecidability.BorisovG0HNN.hnnS1 : G0HNN

The first stable generator in the two-HNN-extension model.

Equations

• Undecidability.BorisovG0HNN.hnnS1 = Undecidability.BorisovHNNModel.firstStableInStageThree

noncomputable def Undecidability.BorisovG0HNN.hnnS2 : G0HNN

The second stable generator in the two-HNN-extension model.

Equations

• Undecidability.BorisovG0HNN.hnnS2 = Undecidability.BorisovHNNModel.secondStableInStageThree

theorem Undecidability.BorisovG0HNN.hnn_d_four_mul_s1 : hnnD ^ 4 * hnnS1 = hnnS1 * hnnD

theorem Undecidability.BorisovG0HNN.hnn_e_mul_s1 : hnnE * hnnS1 = hnnS1 * hnnE ^ 4

theorem Undecidability.BorisovG0HNN.hnn_d_four_mul_s2 : hnnD ^ 4 * hnnS2 = hnnS2 * hnnD

theorem Undecidability.BorisovG0HNN.hnn_e_mul_s2 : hnnE * hnnS2 = hnnS2 * hnnE ^ 4

The homomorphism from the presentation to the HNN model

noncomputable def Undecidability.BorisovG0HNN.hnnGenerator : Fin 4 → G0HNN

The four model generators, ordered d, e, s₁, s₂.

Equations

• Undecidability.BorisovG0HNN.hnnGenerator = ![Undecidability.BorisovG0HNN.hnnD, Undecidability.BorisovG0HNN.hnnE, Undecidability.BorisovG0HNN.hnnS1, Undecidability.BorisovG0HNN.hnnS2]

theorem Undecidability.BorisovG0HNN.hnn_relators (r : FreeGroup (Fin 4)) : r ∈ BorisovIntersections.presentation.relSet → (FreeGroup.lift hnnGenerator) r = 1

noncomputable def Undecidability.BorisovG0HNN.toHNN : BorisovIntersections.G0 →* G0HNN

The homomorphism from the four-relator presentation to its iterated-HNN model.

Equations

• Undecidability.BorisovG0HNN.toHNN = PresentedGroup.toGroup Undecidability.BorisovG0HNN.hnn_relators

@[simp]

theorem Undecidability.BorisovG0HNN.toHNN_of (i : Fin 4) : toHNN (PresentedGroup.of i) = hnnGenerator i

The homomorphism from the HNN model to the presentation

def Undecidability.BorisovG0HNN.presentedD : BorisovIntersections.G0

The first base generator in the four-relator presented group.

Equations

• Undecidability.BorisovG0HNN.presentedD = Undecidability.BorisovIntersections.d

def Undecidability.BorisovG0HNN.presentedE : BorisovIntersections.G0

The second base generator in the four-relator presented group.

Equations

• Undecidability.BorisovG0HNN.presentedE = Undecidability.BorisovIntersections.e

def Undecidability.BorisovG0HNN.presentedS1 : BorisovIntersections.G0

The first stable generator in the four-relator presented group.

Equations

• Undecidability.BorisovG0HNN.presentedS1 = Undecidability.BorisovIntersections.evalWord Undecidability.BorisovIntersections.s1Word

def Undecidability.BorisovG0HNN.presentedS2 : BorisovIntersections.G0

The second stable generator in the four-relator presented group.

Equations

• Undecidability.BorisovG0HNN.presentedS2 = Undecidability.BorisovIntersections.evalWord Undecidability.BorisovIntersections.s2Word

@[simp]

theorem Undecidability.BorisovG0HNN.presentedD_eq_of : presentedD = PresentedGroup.of 0

@[simp]

theorem Undecidability.BorisovG0HNN.presentedE_eq_of : presentedE = PresentedGroup.of 1

@[simp]

theorem Undecidability.BorisovG0HNN.presentedS1_eq_of : presentedS1 = PresentedGroup.of 2

@[simp]

theorem Undecidability.BorisovG0HNN.presentedS2_eq_of : presentedS2 = PresentedGroup.of 3

def Undecidability.BorisovG0HNN.baseToPresented : Base →* BorisovIntersections.G0

The homomorphism from the free base group to the four-relator presented group.

Equations

• Undecidability.BorisovG0HNN.baseToPresented = FreeGroup.lift ![Undecidability.BorisovG0HNN.presentedD, Undecidability.BorisovG0HNN.presentedE]

@[simp]

theorem Undecidability.BorisovG0HNN.baseToPresented_baseD : baseToPresented baseD = presentedD

@[simp]

theorem Undecidability.BorisovG0HNN.baseToPresented_baseE : baseToPresented baseE = presentedE

theorem Undecidability.BorisovG0HNN.first_lift_condition (a : ↥BorisovHNNModel.A0) : presentedS1 * baseToPresented ↑a = baseToPresented ↑(BorisovHNNModel.phi0 a) * presentedS1

noncomputable def Undecidability.BorisovG0HNN.g1ToPresented : G1 →* BorisovIntersections.G0

Extend the base interpretation across the first HNN-extension stage.

Equations

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

@[simp]

theorem Undecidability.BorisovG0HNN.g1ToPresented_of (x : Base) : g1ToPresented (baseToG1 x) = baseToPresented x

@[simp]

theorem Undecidability.BorisovG0HNN.g1ToPresented_s1 : g1ToPresented BorisovHNNModel.s1 = presentedS1

theorem Undecidability.BorisovG0HNN.second_lift_condition (a : ↥BorisovHNNModel.A1) : presentedS2 * g1ToPresented ↑a = g1ToPresented ↑(BorisovHNNModel.phi1 a) * presentedS2

noncomputable def Undecidability.BorisovG0HNN.fromHNN : G0HNN →* BorisovIntersections.G0

The inverse interpretation of the two-HNN-extension model in the four-relator presentation.

Equations

• Undecidability.BorisovG0HNN.fromHNN = HNNExtension.lift Undecidability.BorisovG0HNN.g1ToPresented Undecidability.BorisovG0HNN.presentedS2 Undecidability.BorisovG0HNN.second_lift_condition

@[simp]

theorem Undecidability.BorisovG0HNN.fromHNN_of (x : G1) : fromHNN (g1ToG0HNN x) = g1ToPresented x

@[simp]

theorem Undecidability.BorisovG0HNN.fromHNN_hnnD : fromHNN hnnD = presentedD

@[simp]

theorem Undecidability.BorisovG0HNN.fromHNN_hnnE : fromHNN hnnE = presentedE

@[simp]

theorem Undecidability.BorisovG0HNN.fromHNN_hnnS1 : fromHNN hnnS1 = presentedS1

@[simp]

theorem Undecidability.BorisovG0HNN.fromHNN_hnnS2 : fromHNN hnnS2 = presentedS2

theorem Undecidability.BorisovG0HNN.toHNN_presentedD : toHNN presentedD = hnnD

theorem Undecidability.BorisovG0HNN.toHNN_presentedE : toHNN presentedE = hnnE

theorem Undecidability.BorisovG0HNN.toHNN_presentedS1 : toHNN presentedS1 = hnnS1

theorem Undecidability.BorisovG0HNN.toHNN_presentedS2 : toHNN presentedS2 = hnnS2

theorem Undecidability.BorisovG0HNN.fromHNN_comp_toHNN : fromHNN.comp toHNN = MonoidHom.id BorisovIntersections.G0

theorem Undecidability.BorisovG0HNN.toHNN_comp_fromHNN : toHNN.comp fromHNN = MonoidHom.id G0HNN

noncomputable def Undecidability.BorisovG0HNN.g0Equiv : BorisovIntersections.G0 ≃* G0HNN

The concrete four-generator, four-relator presentation is the iterated HNN extension above. The forward direction sends the four presentation generators to hnnD, hnnE, hnnS1, and hnnS2.

Equations

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

@[simp]

theorem Undecidability.BorisovG0HNN.g0Equiv_apply (x : BorisovIntersections.G0) : g0Equiv x = toHNN x