The second compression HNN extension

This file formalizes Lemma 3.2 of the paper using Proposition 3.8. The two subgroups which are to be identified by the new stable letter are

• DTC = ⟨d,t,c⟩, and
• TCY = ⟨t,c,y⟩

inside the proper y-stage. The first part of the file identifies TCY with the HNN extension obtained by restricting the y-stage to Kc = ⟨t,c,k⟩. In particular, the apparently extra generator k is eliminated by the defining equation y⁻¹ t y = k.

@[reducible, inline]

abbrev Undecidability.HostZStage.Y (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Type

The first compression HNN extension, adjoining the stable generator y.

Equations

• Undecidability.HostZStage.Y datum theta = Undecidability.HostYStage.YStage datum theta

noncomputable def Undecidability.HostZStage.dY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Y datum theta

The image of d in the first compression extension.

Equations

• Undecidability.HostZStage.dY datum theta = (Undecidability.HostYStage.toYStage datum theta) (Undecidability.HostYStage.d datum)

noncomputable def Undecidability.HostZStage.tY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Y datum theta

The image of t in the first compression extension.

Equations

• Undecidability.HostZStage.tY datum theta = (Undecidability.HostYStage.toYStage datum theta) (Undecidability.HostYStage.t datum)

noncomputable def Undecidability.HostZStage.cY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Y datum theta

The image of c in the first compression extension.

Equations

• Undecidability.HostZStage.cY datum theta = (Undecidability.HostYStage.toYStage datum theta) (Undecidability.HostYStage.c datum)

noncomputable def Undecidability.HostZStage.kY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Y datum theta

The image of k in the first compression extension.

Equations

• Undecidability.HostZStage.kY datum theta = (Undecidability.HostYStage.toYStage datum theta) (Undecidability.HostYStage.k datum)

noncomputable def Undecidability.HostZStage.y (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Y datum theta

The new stable generator y of the first compression extension.

Equations

• Undecidability.HostZStage.y datum theta = Undecidability.HostYStage.yLetter datum theta

noncomputable def Undecidability.HostZStage.DTC (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Subgroup (Y datum theta)

The source subgroup for the second HNN extension: ⟨d,t,c⟩.

Equations

• Undecidability.HostZStage.DTC datum theta = Subgroup.closure {Undecidability.HostZStage.dY datum theta, Undecidability.HostZStage.tY datum theta, Undecidability.HostZStage.cY datum theta}

noncomputable def Undecidability.HostZStage.TCY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Subgroup (Y datum theta)

The target subgroup for the second HNN extension: ⟨t,c,y⟩.

Equations

• Undecidability.HostZStage.TCY datum theta = Subgroup.closure {Undecidability.HostZStage.tY datum theta, Undecidability.HostZStage.cY datum theta, Undecidability.HostZStage.y datum theta}

@[simp]

theorem Undecidability.HostZStage.dY_mem_DTC (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : dY datum theta ∈ DTC datum theta

@[simp]

theorem Undecidability.HostZStage.tY_mem_DTC (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : tY datum theta ∈ DTC datum theta

@[simp]

theorem Undecidability.HostZStage.cY_mem_DTC (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : cY datum theta ∈ DTC datum theta

@[simp]

theorem Undecidability.HostZStage.tY_mem_TCY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : tY datum theta ∈ TCY datum theta

@[simp]

theorem Undecidability.HostZStage.cY_mem_TCY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : cY datum theta ∈ TCY datum theta

@[simp]

theorem Undecidability.HostZStage.y_mem_TCY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : y datum theta ∈ TCY datum theta

theorem Undecidability.HostZStage.kY_eq_y_inv_tY_y (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : kY datum theta = (y datum theta)⁻¹ * tY datum theta * y datum theta

@[simp]

theorem Undecidability.HostZStage.kY_mem_TCY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : kY datum theta ∈ TCY datum theta

Exact restricted presentation of ⟨t,c,y⟩

@[reducible, inline]

noncomputable abbrev Undecidability.HostZStage.YRestrictedA (datum : Thue.StandingDatum) : Subgroup ↥(HostZIntersections.Kc datum)

The first associated subgroup of the y extension restricted to the k,c subgroup.

Equations

• Undecidability.HostZStage.YRestrictedA datum = Undecidability.HNNLemmas.restrictedA (Undecidability.HostZIntersections.Kc datum)

@[reducible, inline]

noncomputable abbrev Undecidability.HostZStage.YRestrictedB (datum : Thue.StandingDatum) : Subgroup ↥(HostZIntersections.Kc datum)

The second associated subgroup of the y extension restricted to the k,c subgroup.

Equations

• Undecidability.HostZStage.YRestrictedB datum = Undecidability.HNNLemmas.restrictedB (Undecidability.HostZIntersections.Kc datum)

noncomputable def Undecidability.HostZStage.yRestrictedPhi (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(YRestrictedA datum) ≃* ↥(YRestrictedB datum)

The restricted associated-subgroup isomorphism for the y extension.

Equations

• Undecidability.HostZStage.yRestrictedPhi datum theta = Undecidability.HNNLemmas.restrictedPhi (Undecidability.HostZIntersections.Kc datum) ⋯

@[reducible, inline]

abbrev Undecidability.HostZStage.YRestricted (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Type

The HNN extension obtained by restricting the y-stage to Kc = ⟨t,c,k⟩.

Equations

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

noncomputable def Undecidability.HostZStage.yRestrictedEmbedding (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : YRestricted datum theta →* Y datum theta

The canonical embedding of the restricted model into the ambient y-stage.

Equations

• Undecidability.HostZStage.yRestrictedEmbedding datum theta = Undecidability.HNNLemmas.restrictedEmbedding (Undecidability.HostZIntersections.Kc datum) ⋯

theorem Undecidability.HostZStage.yRestrictedEmbedding_injective (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Function.Injective ⇑(yRestrictedEmbedding datum theta)

@[simp]

theorem Undecidability.HostZStage.yRestrictedEmbedding_of (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (x : ↥(HostZIntersections.Kc datum)) : (yRestrictedEmbedding datum theta) (HNNExtension.of x) = (HostYStage.toYStage datum theta) ↑x

@[simp]

theorem Undecidability.HostZStage.yRestrictedEmbedding_t (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (yRestrictedEmbedding datum theta) HNNExtension.t = HNNExtension.t

theorem Undecidability.HostZStage.restrictedGenerated_eq_TCY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : HNNLemmas.generatedWithStable (HostZIntersections.Kc datum) = TCY datum theta

noncomputable def Undecidability.HostZStage.yRestrictedEquivTCY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : YRestricted datum theta ≃* ↥(TCY datum theta)

Exact subgroup-presentation equivalence for ⟨t,c,y⟩. This is the formal Tietze elimination of the intermediate generator k at the second HNN stage.

Equations

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

@[simp]

theorem Undecidability.HostZStage.yRestrictedEquivTCY_coe (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (x : YRestricted datum theta) : ↑((yRestrictedEquivTCY datum theta) x) = (yRestrictedEmbedding datum theta) x

Exact restricted presentation of ⟨d,t,c⟩

@[reducible, inline]

noncomputable abbrev Undecidability.HostZStage.SourceRestrictedA (datum : Thue.StandingDatum) : Subgroup ↥(BorisovCStage.CD datum ⋯)

The first source-model associated subgroup restricted to the c,d subgroup.

Equations

• Undecidability.HostZStage.SourceRestrictedA datum = Undecidability.HNNLemmas.restrictedA (Undecidability.BorisovCStage.CD datum ⋯)

@[reducible, inline]

noncomputable abbrev Undecidability.HostZStage.SourceRestrictedB (datum : Thue.StandingDatum) : Subgroup ↥(BorisovCStage.CD datum ⋯)

The second source-model associated subgroup restricted to the c,d subgroup.

Equations

• Undecidability.HostZStage.SourceRestrictedB datum = Undecidability.HNNLemmas.restrictedB (Undecidability.BorisovCStage.CD datum ⋯)

theorem Undecidability.HostZStage.source_mem_iff (datum : Thue.StandingDatum) (a : ↥(BorisovCStage.CD datum ⋯)) : ↑a ∈ BorisovCStage.CD datum ⋯ ↔ ↑((MulEquiv.refl ↥(BorisovCStage.CD datum ⋯)) a) ∈ BorisovCStage.CD datum ⋯

noncomputable def Undecidability.HostZStage.sourceRestrictedPhi (datum : Thue.StandingDatum) : ↥(SourceRestrictedA datum) ≃* ↥(SourceRestrictedB datum)

The source-model associated-subgroup isomorphism restricted to the c,d subgroup.

Equations

• Undecidability.HostZStage.sourceRestrictedPhi datum = Undecidability.HNNLemmas.restrictedPhi (Undecidability.BorisovCStage.CD datum ⋯) ⋯

@[reducible, inline]

abbrev Undecidability.HostZStage.SourceModel (datum : Thue.StandingDatum) : Type

The restriction of the t-centralizer HNN extension to ⟨c,d⟩. It is the exact semantic path group underlying ⟨d,t,c⟩.

Equations

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

noncomputable def Undecidability.HostZStage.sourceToTStage (datum : Thue.StandingDatum) : SourceModel datum →* BorisovConverseCore.TStage datum ⋯

The embedding of the restricted source model into the t HNN stage.

Equations

• Undecidability.HostZStage.sourceToTStage datum = Undecidability.HNNLemmas.restrictedEmbedding (Undecidability.BorisovCStage.CD datum ⋯) ⋯

noncomputable def Undecidability.HostZStage.sourceEmbedding (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : SourceModel datum →* Y datum theta

The canonical realization of the source path model inside G_y.

Equations

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

theorem Undecidability.HostZStage.sourceEmbedding_injective (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Function.Injective ⇑(sourceEmbedding datum theta)

theorem Undecidability.HostZStage.sourceEmbedding_range (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (sourceEmbedding datum theta).range = DTC datum theta

noncomputable def Undecidability.HostZStage.sourceModelEquivDTC (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : SourceModel datum ≃* ↥(DTC datum theta)

Exact subgroup-presentation equivalence for ⟨d,t,c⟩.

Equations

• Undecidability.HostZStage.sourceModelEquivDTC datum theta = (MonoidHom.ofInjective ⋯).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem Undecidability.HostZStage.sourceModelEquivDTC_coe (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (x : SourceModel datum) : ↑((sourceModelEquivDTC datum theta) x) = (sourceEmbedding datum theta) x

noncomputable def Undecidability.HostZStage.sourceModelD (datum : Thue.StandingDatum) : SourceModel datum

The generator d in the restricted source model.

Equations

• Undecidability.HostZStage.sourceModelD datum = HNNExtension.of ⟨(Undecidability.BorisovCStage.of3 datum ⋯) Undecidability.BorisovHNNModel.d3, ⋯⟩

noncomputable def Undecidability.HostZStage.sourceModelT (datum : Thue.StandingDatum) : SourceModel datum

The centralizing stable generator t in the restricted source model.

Equations

• Undecidability.HostZStage.sourceModelT datum = HNNExtension.t

noncomputable def Undecidability.HostZStage.sourceModelC (datum : Thue.StandingDatum) : SourceModel datum

The generator c in the restricted source model.

Equations

• Undecidability.HostZStage.sourceModelC datum = HNNExtension.of ⟨Undecidability.BorisovCStage.c datum ⋯, ⋯⟩

@[simp]

theorem Undecidability.HostZStage.sourceModelEquivDTC_d (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (sourceModelEquivDTC datum theta) (sourceModelD datum) = ⟨dY datum theta, ⋯⟩

@[simp]

theorem Undecidability.HostZStage.sourceModelEquivDTC_t (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (sourceModelEquivDTC datum theta) (sourceModelT datum) = ⟨tY datum theta, ⋯⟩

@[simp]

theorem Undecidability.HostZStage.sourceModelEquivDTC_c (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (sourceModelEquivDTC datum theta) (sourceModelC datum) = ⟨cY datum theta, ⋯⟩

noncomputable def Undecidability.HostZStage.yRestrictedT (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : YRestricted datum theta

The generator t in the restricted y-extension model.

Equations

• Undecidability.HostZStage.yRestrictedT datum theta = HNNExtension.of ⟨Undecidability.HostYStage.t datum, ⋯⟩

noncomputable def Undecidability.HostZStage.yRestrictedC (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : YRestricted datum theta

The generator c in the restricted y-extension model.

Equations

• Undecidability.HostZStage.yRestrictedC datum theta = HNNExtension.of ⟨Undecidability.HostYStage.c datum, ⋯⟩

noncomputable def Undecidability.HostZStage.yRestrictedY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : YRestricted datum theta

The inverse stable letter representing the generator y in the restricted HNN model.

Equations

• Undecidability.HostZStage.yRestrictedY datum theta = HNNExtension.t⁻¹

@[simp]

theorem Undecidability.HostZStage.yRestrictedEquivTCY_t (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (yRestrictedEquivTCY datum theta) (yRestrictedT datum theta) = ⟨tY datum theta, ⋯⟩

@[simp]

theorem Undecidability.HostZStage.yRestrictedEquivTCY_c (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (yRestrictedEquivTCY datum theta) (yRestrictedC datum theta) = ⟨cY datum theta, ⋯⟩

@[simp]

theorem Undecidability.HostZStage.yRestrictedEquivTCY_y (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (yRestrictedEquivTCY datum theta) (yRestrictedY datum theta) = ⟨y datum theta, ⋯⟩

The forward path rotation on the exact source model

noncomputable def Undecidability.HostZStage.dFreeToGamma3 : FreeGroup Unit →* BorisovHNNModel.Gamma3

The homomorphism sending the generator of the rank-one free group to d₃.

Equations

• Undecidability.HostZStage.dFreeToGamma3 = FreeGroup.lift fun (x : Unit) => Undecidability.BorisovHNNModel.d3

def Undecidability.HostZStage.unitToBase : Unit → Fin 2

The inclusion of the rank-one alphabet into the first generator of the rank-two alphabet.

Equations

• Undecidability.HostZStage.unitToBase x✝ = 0

theorem Undecidability.HostZStage.dFreeToGamma3_injective : Function.Injective ⇑dFreeToGamma3

theorem Undecidability.HostZStage.dFreeToGamma3_range : dFreeToGamma3.range = BorisovCStage.dCyclic

noncomputable def Undecidability.HostZStage.freeEquivDCyclic : FreeGroup Unit ≃* ↥BorisovCStage.dCyclic

The equivalence between the rank-one free group and the cyclic subgroup generated by d₃.

Equations

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

noncomputable def Undecidability.HostZStage.dInCyclic : ↥BorisovCStage.dCyclic

The generator d₃, regarded as an element of its cyclic subgroup.

Equations

• Undecidability.HostZStage.dInCyclic = ⟨Undecidability.BorisovHNNModel.d3, Undecidability.HostZStage.dInCyclic._proof_2⟩

noncomputable def Undecidability.HostZStage.dCyclicToYRestricted (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥BorisovCStage.dCyclic →* YRestricted datum theta

The homomorphism from the cyclic d₃ subgroup to the restricted y model.

Equations

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

noncomputable def Undecidability.HostZStage.dRestrictedToYRestricted (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : BorisovContextNormalForm.DRestricted datum ⋯ ⋯ →* YRestricted datum theta

The homomorphism from the restricted d subgroup to the restricted y model.

Equations

• Undecidability.HostZStage.dRestrictedToYRestricted datum theta = HNNExtension.lift (Undecidability.HostZStage.dCyclicToYRestricted datum theta) HNNExtension.t ⋯

noncomputable def Undecidability.HostZStage.CDToYRestricted (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(BorisovCStage.CD datum ⋯) →* YRestricted datum theta

The homomorphism from the c,d subgroup to the restricted y model.

Equations

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

noncomputable def Undecidability.HostZStage.dInCD (datum : Thue.StandingDatum) : ↥(BorisovCStage.CD datum ⋯)

The image of d₃ in the subgroup generated by c and d.

Equations

• Undecidability.HostZStage.dInCD datum = ⟨(Undecidability.BorisovCStage.of3 datum ⋯) Undecidability.BorisovHNNModel.d3, ⋯⟩

noncomputable def Undecidability.HostZStage.cInCD (datum : Thue.StandingDatum) : ↥(BorisovCStage.CD datum ⋯)

The element c in the subgroup generated by c and d.

Equations

• Undecidability.HostZStage.cInCD datum = ⟨Undecidability.BorisovCStage.c datum ⋯, ⋯⟩

noncomputable def Undecidability.HostZStage.sourceModelToYRestricted (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : SourceModel datum →* YRestricted datum theta

The HNN-extension homomorphism from the source model to the restricted y model.

Equations

• Undecidability.HostZStage.sourceModelToYRestricted datum theta = HNNExtension.lift (Undecidability.HostZStage.CDToYRestricted datum theta) (Undecidability.HostZStage.yRestrictedC datum theta) ⋯

The reverse map on the exact CT and Kc models

noncomputable def Undecidability.HostZStage.C0ToSourceModel (datum : Thue.StandingDatum) : ↥(HostZBaseIntersections.C0 datum) →* SourceModel datum

The cyclic base map c ↦ T for the exact CT model. The sign in the exponent homomorphism compensates for the convention that the paper's c is Mathlib's first HNN stable letter inverse.

Equations

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

noncomputable def Undecidability.HostZStage.CTModelToSourceModel (datum : Thue.StandingDatum) : HostKcModel.CTModel datum →* SourceModel datum

The HNN-extension homomorphism from the c,t model to the source model.

Equations

• Undecidability.HostZStage.CTModelToSourceModel datum = HNNExtension.lift (Undecidability.HostZStage.C0ToSourceModel datum) (Undecidability.HostZStage.sourceModelD datum) ⋯

noncomputable def Undecidability.HostZStage.CTToSourceModel (datum : Thue.StandingDatum) : ↥(HostZBaseIntersections.CT datum) →* SourceModel datum

The homomorphism from the c,t subgroup to the source model.

Equations

• Undecidability.HostZStage.CTToSourceModel datum = (Undecidability.HostZStage.CTModelToSourceModel datum).comp (Undecidability.HostKcModel.ctModelEquivCT datum).symm.toMonoidHom

noncomputable def Undecidability.HostZStage.C0ToCT (datum : Thue.StandingDatum) : ↥(HostZBaseIntersections.C0 datum) →* ↥(HostZBaseIntersections.CT datum)

The homomorphism placing the cyclic c subgroup in the c,t subgroup.

Equations

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

noncomputable def Undecidability.HostZStage.sourceConjugatedD (datum : Thue.StandingDatum) : SourceModel datum

The conjugate c⁻¹ d c in the source model.

Equations

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

noncomputable def Undecidability.HostZStage.RestrictedToSourceModel (datum : Thue.StandingDatum) : HostKcModel.Restricted datum →* SourceModel datum

The homomorphism from the restricted k,c model to the source model.

Equations

• Undecidability.HostZStage.RestrictedToSourceModel datum = HNNExtension.lift (Undecidability.HostZStage.CTToSourceModel datum) (Undecidability.HostZStage.sourceConjugatedD datum) ⋯

noncomputable def Undecidability.HostZStage.kInKc (datum : Thue.StandingDatum) : ↥(HostZIntersections.Kc datum)

The generator k regarded as an element of the k,c subgroup.

Equations

• Undecidability.HostZStage.kInKc datum = ⟨Undecidability.HostYStage.k datum, ⋯⟩

noncomputable def Undecidability.HostZStage.tInKc (datum : Thue.StandingDatum) : ↥(HostZIntersections.Kc datum)

The generator t regarded as an element of the k,c subgroup.

Equations

• Undecidability.HostZStage.tInKc datum = ⟨Undecidability.HostYStage.t datum, ⋯⟩

noncomputable def Undecidability.HostZStage.cInKc (datum : Thue.StandingDatum) : ↥(HostZIntersections.Kc datum)

The generator c regarded as an element of the k,c subgroup.

Equations

• Undecidability.HostZStage.cInKc datum = ⟨Undecidability.HostYStage.c datum, ⋯⟩

noncomputable def Undecidability.HostZStage.KcToSourceModel (datum : Thue.StandingDatum) : ↥(HostZIntersections.Kc datum) →* SourceModel datum

The homomorphism from the k,c subgroup to the source model.

Equations

• Undecidability.HostZStage.KcToSourceModel datum = (Undecidability.HostZStage.RestrictedToSourceModel datum).comp (Undecidability.HostKcModel.restrictedEquivKc datum).symm.toMonoidHom

noncomputable def Undecidability.HostZStage.thetaThenKcToSourceModel (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(HostZBaseIntersections.CT datum) →* SourceModel datum

The homomorphism obtained by composing the subgroup map θ with the source-model map.

Equations

• Undecidability.HostZStage.thetaThenKcToSourceModel datum theta = (Undecidability.HostZStage.KcToSourceModel datum).comp (Undecidability.HostThetaCT.thetaCTtoKc datum theta)

noncomputable def Undecidability.HostZStage.conjugatedCTToSourceModel (datum : Thue.StandingDatum) : ↥(HostZBaseIntersections.CT datum) →* SourceModel datum

The conjugated homomorphism from the c,t subgroup to the source model.

Equations

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

noncomputable def Undecidability.HostZStage.CTToKc (datum : Thue.StandingDatum) : ↥(HostZBaseIntersections.CT datum) →* ↥(HostZIntersections.Kc datum)

The subgroup homomorphism from the c,t subgroup to the k,c subgroup.

Equations

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

theorem Undecidability.HostZStage.yRestrictedCompatibility (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (a : ↥(YRestrictedA datum)) : (sourceModelC datum)⁻¹ * (KcToSourceModel datum) ↑a = (KcToSourceModel datum) ↑((yRestrictedPhi datum theta) a) * (sourceModelC datum)⁻¹

noncomputable def Undecidability.HostZStage.YRestrictedToSourceModel (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : YRestricted datum theta →* SourceModel datum

The HNN-extension homomorphism from the restricted y model to the source model.

Equations

• Undecidability.HostZStage.YRestrictedToSourceModel datum theta = HNNExtension.lift (Undecidability.HostZStage.KcToSourceModel datum) (Undecidability.HostZStage.sourceModelC datum)⁻¹ ⋯

theorem Undecidability.HostZStage.YRestrictedToSourceModel_comp_sourceModelToYRestricted (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (YRestrictedToSourceModel datum theta).comp (sourceModelToYRestricted datum theta) = MonoidHom.id (SourceModel datum)

theorem Undecidability.HostZStage.sourceModelToYRestricted_comp_YRestrictedToSourceModel (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (sourceModelToYRestricted datum theta).comp (YRestrictedToSourceModel datum theta) = MonoidHom.id (YRestricted datum theta)

noncomputable def Undecidability.HostZStage.sourceModelEquivYRestricted (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : SourceModel datum ≃* YRestricted datum theta

The equivalence identifying the source model with the restricted y model.

Equations

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

Public interface for the path rotation

noncomputable def Undecidability.HostZStage.sourceD (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(DTC datum theta)

The source generator d in the subgroup generated by d,t,c.

Equations

• Undecidability.HostZStage.sourceD datum theta = ⟨Undecidability.HostZStage.dY datum theta, ⋯⟩

noncomputable def Undecidability.HostZStage.sourceT (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(DTC datum theta)

The source generator t in the subgroup generated by d,t,c.

Equations

• Undecidability.HostZStage.sourceT datum theta = ⟨Undecidability.HostZStage.tY datum theta, ⋯⟩

noncomputable def Undecidability.HostZStage.sourceC (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(DTC datum theta)

The source generator c in the subgroup generated by d,t,c.

Equations

• Undecidability.HostZStage.sourceC datum theta = ⟨Undecidability.HostZStage.cY datum theta, ⋯⟩

noncomputable def Undecidability.HostZStage.targetT (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(TCY datum theta)

The target generator t in the subgroup generated by t,c,y.

Equations

• Undecidability.HostZStage.targetT datum theta = ⟨Undecidability.HostZStage.tY datum theta, ⋯⟩

noncomputable def Undecidability.HostZStage.targetC (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(TCY datum theta)

The target generator c in the subgroup generated by t,c,y.

Equations

• Undecidability.HostZStage.targetC datum theta = ⟨Undecidability.HostZStage.cY datum theta, ⋯⟩

noncomputable def Undecidability.HostZStage.targetY (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(TCY datum theta)

The target generator y in the subgroup generated by t,c,y.

Equations

• Undecidability.HostZStage.targetY datum theta = ⟨Undecidability.HostZStage.y datum theta, ⋯⟩

noncomputable def Undecidability.HostZStage.pathEquiv (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ↥(DTC datum theta) ≃* ↥(TCY datum theta)

The path rotation following Lemma 3.2, obtained by transporting the exact restricted presentations of ⟨d,t,c⟩ and ⟨t,c,y⟩.

Equations

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

@[simp]

theorem Undecidability.HostZStage.pathEquiv_d (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (pathEquiv datum theta) (sourceD datum theta) = targetT datum theta

@[simp]

theorem Undecidability.HostZStage.pathEquiv_t (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (pathEquiv datum theta) (sourceT datum theta) = targetC datum theta

@[simp]

theorem Undecidability.HostZStage.pathEquiv_c (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : (pathEquiv datum theta) (sourceC datum theta) = targetY datum theta

structure Undecidability.HostZStage.ZetaData (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : Type

The exact output of the path-presentation calculation in Lemma 3.2. Keeping the generator equations with the equivalence makes all later Tietze calculations independent of its normal-form implementation.

• equiv : ↥(DTC datum theta) ≃* ↥(TCY datum theta)

  The subgroup equivalence used to define the final HNN extension.

• map_d : self.equiv (sourceD datum theta) = targetT datum theta
• map_t : self.equiv (sourceT datum theta) = targetC datum theta
• map_c : self.equiv (sourceC datum theta) = targetY datum theta

noncomputable def Undecidability.HostZStage.zetaData (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) : ZetaData datum theta

The canonical attaching equivalence for the second compression.

Equations

• Undecidability.HostZStage.zetaData datum theta = { equiv := Undecidability.HostZStage.pathEquiv datum theta, map_d := ⋯, map_t := ⋯, map_c := ⋯ }

@[reducible, inline]

abbrev Undecidability.HostZStage.ZStage (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : ZetaData datum theta) : Type

The proper second HNN extension, once the path rotation following Lemma 3.2 has been constructed.

Equations

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

noncomputable def Undecidability.HostZStage.toZStage (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : ZetaData datum theta) : Y datum theta →* ZStage datum theta zeta

The canonical inclusion G_y → G_z.

Equations

• Undecidability.HostZStage.toZStage datum theta zeta = HNNExtension.of

noncomputable def Undecidability.HostZStage.zLetter (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : ZetaData datum theta) : ZStage datum theta zeta

The paper's z; Mathlib's stable letter is z⁻¹.

Equations

• Undecidability.HostZStage.zLetter datum theta zeta = HNNExtension.t⁻¹

theorem Undecidability.HostZStage.toZStage_injective (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : ZetaData datum theta) : Function.Injective ⇑(toZStage datum theta zeta)

theorem Undecidability.HostZStage.z_conjugates_d (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : ZetaData datum theta) : (zLetter datum theta zeta)⁻¹ * (toZStage datum theta zeta) (dY datum theta) * zLetter datum theta zeta = (toZStage datum theta zeta) (tY datum theta)

theorem Undecidability.HostZStage.z_conjugates_t (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : ZetaData datum theta) : (zLetter datum theta zeta)⁻¹ * (toZStage datum theta zeta) (tY datum theta) * zLetter datum theta zeta = (toZStage datum theta zeta) (cY datum theta)

theorem Undecidability.HostZStage.z_conjugates_c (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : ZetaData datum theta) : (zLetter datum theta zeta)⁻¹ * (toZStage datum theta zeta) (cY datum theta) * zLetter datum theta zeta = (toZStage datum theta zeta) (y datum theta)