The two-stage HNN model for Borisov's four-relator group

The base is the free group on d and e. Two injective substitutions encode the power maps

  alpha : d ↦ d,  e ↦ e⁴,
  beta  : d ↦ d⁴, e ↦ e.

The first HNN extension adjoins s₁ along these substitutions. The second adjoins s₂ along the transported copies of the same associated subgroups. The resulting group Gamma3, together with d3, e3, firstStableInStageThree, and secondStableInStageThree, is the low-level semantic model used by the Borisov normal-form arguments. The presentation-facing equivalence is constructed separately in GroupUndecidability.Borisov.Model.G0HNN.

The rank-two free base and the two injective substitutions

@[reducible, inline]

abbrev Undecidability.BorisovHNNModel.Base : Type

The free group on the two base generators.

Equations

• Undecidability.BorisovHNNModel.Base = FreeGroup (Fin 2)

def Undecidability.BorisovHNNModel.d : Base

The first free base generator d.

Equations

• Undecidability.BorisovHNNModel.d = FreeGroup.of 0

def Undecidability.BorisovHNNModel.e : Base

The second free base generator e.

Equations

• Undecidability.BorisovHNNModel.e = FreeGroup.of 1

def Undecidability.BorisovHNNModel.intFour : Multiplicative ℤ →* Multiplicative ℤ

The infinite-cyclic-group homomorphism multiplying an exponent by four.

Equations

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

def Undecidability.BorisovHNNModel.cyclicFour : FreeGroup Unit →* FreeGroup Unit

The injective endomorphism taking the cyclic free generator to its fourth power.

Equations

• Undecidability.BorisovHNNModel.cyclicFour = FreeGroup.mulEquivIntOfUnique.symm.toMonoidHom.comp (Undecidability.BorisovHNNModel.intFour.comp FreeGroup.mulEquivIntOfUnique.toMonoidHom)

def Undecidability.BorisovHNNModel.componentA (i : Fin 2) : FreeGroup Unit →* FreeGroup Unit

The component substitutions fixing the first cyclic generator and powering the second.

Equations

• Undecidability.BorisovHNNModel.componentA 0 = MonoidHom.id (FreeGroup Unit)
• Undecidability.BorisovHNNModel.componentA 1 = Undecidability.BorisovHNNModel.cyclicFour

def Undecidability.BorisovHNNModel.componentB (i : Fin 2) : FreeGroup Unit →* FreeGroup Unit

The component substitutions powering the first cyclic generator and fixing the second.

Equations

• Undecidability.BorisovHNNModel.componentB 0 = Undecidability.BorisovHNNModel.cyclicFour
• Undecidability.BorisovHNNModel.componentB 1 = MonoidHom.id (FreeGroup Unit)

def Undecidability.BorisovHNNModel.freeProductSubstitution (f : Fin 2 → FreeGroup Unit →* FreeGroup Unit) : Base →* Base

The free-base substitution induced componentwise through the cyclic free-product representation.

Equations

• Undecidability.BorisovHNNModel.freeProductSubstitution f = freeGroupEquivCoprodI.symm.toMonoidHom.comp ((Monoid.CoprodI.familyMap f).comp freeGroupEquivCoprodI.toMonoidHom)

def Undecidability.BorisovHNNModel.alpha : Base →* Base

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

Equations

• Undecidability.BorisovHNNModel.alpha = Undecidability.BorisovHNNModel.freeProductSubstitution Undecidability.BorisovHNNModel.componentA

def Undecidability.BorisovHNNModel.beta : Base →* Base

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

Equations

• Undecidability.BorisovHNNModel.beta = Undecidability.BorisovHNNModel.freeProductSubstitution Undecidability.BorisovHNNModel.componentB

theorem Undecidability.BorisovHNNModel.alpha_injective : Function.Injective ⇑alpha

theorem Undecidability.BorisovHNNModel.beta_injective : Function.Injective ⇑beta

@[simp]

theorem Undecidability.BorisovHNNModel.alpha_d : alpha d = d

@[simp]

theorem Undecidability.BorisovHNNModel.alpha_e : alpha e = e ^ 4

@[simp]

theorem Undecidability.BorisovHNNModel.beta_d : beta d = d ^ 4

@[simp]

theorem Undecidability.BorisovHNNModel.beta_e : beta e = e

theorem Undecidability.BorisovHNNModel.alpha_eq_lift : alpha = FreeGroup.lift ![d, e ^ 4]

theorem Undecidability.BorisovHNNModel.beta_eq_lift : beta = FreeGroup.lift ![d ^ 4, e]

The first HNN extension, adjoining s₁

@[reducible, inline]

abbrev Undecidability.BorisovHNNModel.A0 : Subgroup Base

The image subgroup of the first injective base substitution.

Equations

• Undecidability.BorisovHNNModel.A0 = Undecidability.BorisovHNNModel.alpha.range

@[reducible, inline]

abbrev Undecidability.BorisovHNNModel.B0 : Subgroup Base

The image subgroup of the second injective base substitution.

Equations

• Undecidability.BorisovHNNModel.B0 = Undecidability.BorisovHNNModel.beta.range

noncomputable def Undecidability.BorisovHNNModel.inA0 : Base ≃* ↥A0

The equivalence between the free base group and the first image subgroup.

Equations

• Undecidability.BorisovHNNModel.inA0 = MonoidHom.ofInjective Undecidability.BorisovHNNModel.alpha_injective

noncomputable def Undecidability.BorisovHNNModel.inB0 : Base ≃* ↥B0

The equivalence between the free base group and the second image subgroup.

Equations

• Undecidability.BorisovHNNModel.inB0 = MonoidHom.ofInjective Undecidability.BorisovHNNModel.beta_injective

noncomputable def Undecidability.BorisovHNNModel.phi0 : ↥A0 ≃* ↥B0

The isomorphism between the two associated image subgroups.

Equations

• Undecidability.BorisovHNNModel.phi0 = Undecidability.BorisovHNNModel.inA0.symm.trans Undecidability.BorisovHNNModel.inB0

@[simp]

theorem Undecidability.BorisovHNNModel.phi0_inA0 (x : Base) : phi0 (inA0 x) = inB0 x

@[simp]

theorem Undecidability.BorisovHNNModel.coe_inA0 (x : Base) : ↑(inA0 x) = alpha x

@[simp]

theorem Undecidability.BorisovHNNModel.coe_inB0 (x : Base) : ↑(inB0 x) = beta x

@[reducible, inline]

abbrev Undecidability.BorisovHNNModel.Stage1 : Type

The HNN extension adjoining the first stable generator.

Equations

• Undecidability.BorisovHNNModel.Stage1 = HNNExtension Undecidability.BorisovHNNModel.Base Undecidability.BorisovHNNModel.A0 Undecidability.BorisovHNNModel.B0 Undecidability.BorisovHNNModel.phi0

noncomputable def Undecidability.BorisovHNNModel.of0 : Base →* Stage1

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

Equations

• Undecidability.BorisovHNNModel.of0 = HNNExtension.of

noncomputable def Undecidability.BorisovHNNModel.s1 : Stage1

The first HNN stable generator.

Equations

• Undecidability.BorisovHNNModel.s1 = HNNExtension.t

theorem Undecidability.BorisovHNNModel.of0_injective : Function.Injective ⇑of0

theorem Undecidability.BorisovHNNModel.stage1_s1_mul_d : s1 * of0 d = of0 (d ^ 4) * s1

theorem Undecidability.BorisovHNNModel.stage1_s1_mul_e_four : s1 * of0 (e ^ 4) = of0 e * s1

theorem Undecidability.BorisovHNNModel.stage1_d_four_mul_s1 : of0 (d ^ 4) * s1 = s1 * of0 d

theorem Undecidability.BorisovHNNModel.stage1_e_mul_s1 : of0 e * s1 = s1 * of0 (e ^ 4)

The second HNN extension

This adjoins s₂ to a transported copy of the same pair of associated subgroups.

@[reducible, inline]

noncomputable abbrev Undecidability.BorisovHNNModel.A1 : Subgroup Stage1

The first associated subgroup carried into the first HNN extension.

Equations

• Undecidability.BorisovHNNModel.A1 = Subgroup.map Undecidability.BorisovHNNModel.of0 Undecidability.BorisovHNNModel.A0

@[reducible, inline]

noncomputable abbrev Undecidability.BorisovHNNModel.B1 : Subgroup Stage1

The second associated subgroup carried into the first HNN extension.

Equations

• Undecidability.BorisovHNNModel.B1 = Subgroup.map Undecidability.BorisovHNNModel.of0 Undecidability.BorisovHNNModel.B0

noncomputable def Undecidability.BorisovHNNModel.inA1 : ↥A0 ≃* ↥A1

The equivalence onto the carried first associated subgroup.

Equations

• Undecidability.BorisovHNNModel.inA1 = Undecidability.BorisovHNNModel.A0.equivMapOfInjective Undecidability.BorisovHNNModel.of0 Undecidability.BorisovHNNModel.of0_injective

noncomputable def Undecidability.BorisovHNNModel.inB1 : ↥B0 ≃* ↥B1

The equivalence onto the carried second associated subgroup.

Equations

• Undecidability.BorisovHNNModel.inB1 = Undecidability.BorisovHNNModel.B0.equivMapOfInjective Undecidability.BorisovHNNModel.of0 Undecidability.BorisovHNNModel.of0_injective

noncomputable def Undecidability.BorisovHNNModel.phi1 : ↥A1 ≃* ↥B1

The associated-subgroup isomorphism transported into the first HNN extension.

Equations

• Undecidability.BorisovHNNModel.phi1 = Undecidability.BorisovHNNModel.inA1.symm.trans (Undecidability.BorisovHNNModel.phi0.trans Undecidability.BorisovHNNModel.inB1)

@[simp]

theorem Undecidability.BorisovHNNModel.phi1_inA1 (a : ↥A0) : phi1 (inA1 a) = inB1 (phi0 a)

@[simp]

theorem Undecidability.BorisovHNNModel.coe_inA1 (a : ↥A0) : ↑(inA1 a) = of0 ↑a

@[simp]

theorem Undecidability.BorisovHNNModel.coe_inB1 (b : ↥B0) : ↑(inB1 b) = of0 ↑b

@[reducible, inline]

abbrev Undecidability.BorisovHNNModel.Gamma3 : Type

The HNN extension adjoining the second stable generator.

Equations

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

noncomputable def Undecidability.BorisovHNNModel.of1 : Stage1 →* Gamma3

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

Equations

• Undecidability.BorisovHNNModel.of1 = HNNExtension.of

noncomputable def Undecidability.BorisovHNNModel.d3 : Gamma3

The image of d after the two HNN extensions.

Equations

• Undecidability.BorisovHNNModel.d3 = Undecidability.BorisovHNNModel.of1 (Undecidability.BorisovHNNModel.of0 Undecidability.BorisovHNNModel.d)

noncomputable def Undecidability.BorisovHNNModel.e3 : Gamma3

The image of e after the two HNN extensions.

Equations

• Undecidability.BorisovHNNModel.e3 = Undecidability.BorisovHNNModel.of1 (Undecidability.BorisovHNNModel.of0 Undecidability.BorisovHNNModel.e)

noncomputable def Undecidability.BorisovHNNModel.firstStableInStageThree : Gamma3

The image of the first stable generator after adjoining the second.

Equations

• Undecidability.BorisovHNNModel.firstStableInStageThree = Undecidability.BorisovHNNModel.of1 Undecidability.BorisovHNNModel.s1

noncomputable def Undecidability.BorisovHNNModel.secondStableInStageThree : Gamma3

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

Equations

• Undecidability.BorisovHNNModel.secondStableInStageThree = HNNExtension.t

theorem Undecidability.BorisovHNNModel.of1_injective : Function.Injective ⇑of1

theorem Undecidability.BorisovHNNModel.baseEmbedding_injective : Function.Injective ⇑(of1.comp of0)

theorem Undecidability.BorisovHNNModel.gamma3_d_four_mul_s1 : d3 ^ 4 * firstStableInStageThree = firstStableInStageThree * d3

theorem Undecidability.BorisovHNNModel.gamma3_e_mul_s1 : e3 * firstStableInStageThree = firstStableInStageThree * e3 ^ 4

theorem Undecidability.BorisovHNNModel.gamma3_s2_mul_d : secondStableInStageThree * d3 = d3 ^ 4 * secondStableInStageThree

theorem Undecidability.BorisovHNNModel.gamma3_s2_mul_e_four : secondStableInStageThree * e3 ^ 4 = e3 * secondStableInStageThree

theorem Undecidability.BorisovHNNModel.gamma3_d_four_mul_s2 : d3 ^ 4 * secondStableInStageThree = secondStableInStageThree * d3

theorem Undecidability.BorisovHNNModel.gamma3_e_mul_s2 : e3 * secondStableInStageThree = secondStableInStageThree * e3 ^ 4