The exact path model for K_c = ⟨t,c,k⟩

The double-coset identity in the proof of Proposition 3.8 implies that the subgroup ⟨c,t⟩ of the t-stage meets the subgroup centralized by k in precisely ⟨c⟩. Consequently the restriction of the final centralizer HNN extension to ⟨c,t⟩ is the path HNN extension with base ⟨c,t⟩, associated subgroup ⟨c⟩, and stable letter k. This file identifies that model exactly with HostZIntersections.Kc.

@[reducible, inline]

abbrev Undecidability.HostKcModel.FreeInput (datum : Thue.StandingDatum) : BorisovCStage.RankFiveFree datum

The proved rank-five freeness input used to construct the concrete host models.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev Undecidability.HostKcModel.TBase (datum : Thue.StandingDatum) : Type

The HNN stage adjoining the centralizer generator t.

Equations

• Undecidability.HostKcModel.TBase datum = Undecidability.BorisovConverseCore.TStage datum ⋯

@[reducible, inline]

abbrev Undecidability.HostKcModel.Gamma (datum : Thue.StandingDatum) : Type

The final Borisov iterated-HNN model underlying the host.

Equations

• Undecidability.HostKcModel.Gamma datum = Undecidability.HostYStage.Gamma datum

theorem Undecidability.HostKcModel.CT_inf_Delta (datum : Thue.StandingDatum) : HostZBaseIntersections.CT datum ⊓ HostZBaseIntersections.Delta datum = HostZBaseIntersections.C0InT datum

A consequence of the double-coset identity in the proof of Proposition 3.8: in the t-stage, ⟨c,t⟩ ∩ Delta = ⟨c⟩.

noncomputable def Undecidability.HostKcModel.C0InCT (datum : Thue.StandingDatum) : Subgroup ↥(HostZBaseIntersections.CT datum)

The copy of ⟨c⟩ regarded as a subgroup of the base ⟨c,t⟩.

Equations

• Undecidability.HostKcModel.C0InCT datum = Subgroup.comap (Undecidability.HostZBaseIntersections.CT datum).subtype (Undecidability.HostZBaseIntersections.C0InT datum)

theorem Undecidability.HostKcModel.restrictedA_eq_C0InCT (datum : Thue.StandingDatum) : HNNLemmas.restrictedA (HostZBaseIntersections.CT datum) = C0InCT datum

The associated subgroup obtained by restricting Delta to ⟨c,t⟩ is exactly the copy of ⟨c⟩ in that base.

noncomputable def Undecidability.HostKcModel.baseT (datum : Thue.StandingDatum) : ↥(HostZBaseIntersections.CT datum)

The base generator t as an element of ⟨c,t⟩.

Equations

• Undecidability.HostKcModel.baseT datum = ⟨Undecidability.BorisovConverseCore.tLetter datum ⋯, ⋯⟩

noncomputable def Undecidability.HostKcModel.baseC (datum : Thue.StandingDatum) : ↥(HostZBaseIntersections.CT datum)

The base generator c as an element of ⟨c,t⟩.

Equations

• Undecidability.HostKcModel.baseC datum = ⟨(Undecidability.BorisovConverseCore.toTStage datum ⋯) (Undecidability.BorisovCStage.c datum ⋯), ⋯⟩

The exact ⟨c,t⟩ model

The preceding t-stage is itself a centralizer HNN extension, with stable letter t centralizing CD = ⟨c,d⟩. Restricting its base to ⟨c⟩ therefore gives an exact presentation of CT = ⟨c,t⟩. Since ⟨c⟩ ≤ CD, the associated subgroup in this restricted model is the whole base ⟨c⟩.

theorem Undecidability.HostKcModel.tCompatibility (datum : Thue.StandingDatum) (a : ↥(BorisovCStage.CD datum ⋯)) : ↑a ∈ HostZBaseIntersections.C0 datum ↔ ↑((MulEquiv.refl ↥(BorisovCStage.CD datum ⋯)) a) ∈ HostZBaseIntersections.C0 datum

@[reducible, inline]

abbrev Undecidability.HostKcModel.CTModel (datum : Thue.StandingDatum) : Type

The literal restriction of the t-centralizer HNN extension to the base ⟨c⟩.

Equations

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

noncomputable def Undecidability.HostKcModel.ctModelEmbedding (datum : Thue.StandingDatum) : CTModel datum →* TBase datum

The canonical realization of CTModel in the semantic t-stage.

Equations

• Undecidability.HostKcModel.ctModelEmbedding datum = Undecidability.HNNLemmas.restrictedEmbedding (Undecidability.HostZBaseIntersections.C0 datum) ⋯

theorem Undecidability.HostKcModel.ctModelGenerated_eq_CT (datum : Thue.StandingDatum) : HNNLemmas.generatedWithStable (HostZBaseIntersections.C0 datum) = HostZBaseIntersections.CT datum

noncomputable def Undecidability.HostKcModel.ctModelEquivCT (datum : Thue.StandingDatum) : CTModel datum ≃* ↥(HostZBaseIntersections.CT datum)

Exact parametrization of CT = ⟨c,t⟩ by the restricted t-centralizer model.

Equations

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

@[simp]

theorem Undecidability.HostKcModel.ctModelEquivCT_coe (datum : Thue.StandingDatum) (x : CTModel datum) : ↑((ctModelEquivCT datum) x) = (ctModelEmbedding datum) x

noncomputable def Undecidability.HostKcModel.cInC0 (datum : Thue.StandingDatum) : ↥(HostZBaseIntersections.C0 datum)

The generator c in the base of CTModel.

Equations

• Undecidability.HostKcModel.cInC0 datum = ⟨Undecidability.BorisovCStage.c datum ⋯, ⋯⟩

noncomputable def Undecidability.HostKcModel.ctModelC (datum : Thue.StandingDatum) : CTModel datum

The two displayed generators of the exact CT model.

Equations

• Undecidability.HostKcModel.ctModelC datum = HNNExtension.of (Undecidability.HostKcModel.cInC0 datum)

noncomputable def Undecidability.HostKcModel.ctModelT (datum : Thue.StandingDatum) : CTModel datum

The stable generator t in the restricted c,t model.

Equations

• Undecidability.HostKcModel.ctModelT datum = HNNExtension.t

@[simp]

theorem Undecidability.HostKcModel.ctModelEquivCT_c (datum : Thue.StandingDatum) : (ctModelEquivCT datum) (ctModelC datum) = baseC datum

@[simp]

theorem Undecidability.HostKcModel.ctModelEquivCT_t (datum : Thue.StandingDatum) : (ctModelEquivCT datum) (ctModelT datum) = baseT datum

theorem Undecidability.HostKcModel.kCompatibility (datum : Thue.StandingDatum) (a : ↥(BorisovConverseCore.KSubgroup datum ⋯)) : ↑a ∈ HostZBaseIntersections.CT datum ↔ ↑((MulEquiv.refl ↥(BorisovConverseCore.KSubgroup datum ⋯)) a) ∈ HostZBaseIntersections.CT datum

@[reducible, inline]

abbrev Undecidability.HostKcModel.Restricted (datum : Thue.StandingDatum) : Type

The literal restricted HNN extension inside Borisov's final k-stage.

Equations

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

noncomputable def Undecidability.HostKcModel.restrictedEmbeddingToGamma (datum : Thue.StandingDatum) : Restricted datum →* Gamma datum

The canonical embedding of the literal restricted model in the final k-stage.

Equations

• Undecidability.HostKcModel.restrictedEmbeddingToGamma datum = Undecidability.HNNLemmas.restrictedEmbedding (Undecidability.HostZBaseIntersections.CT datum) ⋯

theorem Undecidability.HostKcModel.restrictedGenerated_eq_Kc (datum : Thue.StandingDatum) : HNNLemmas.generatedWithStable (HostZBaseIntersections.CT datum) = HostZIntersections.Kc datum

noncomputable def Undecidability.HostKcModel.restrictedEquivKc (datum : Thue.StandingDatum) : Restricted datum ≃* ↥(HostZIntersections.Kc datum)

Exact parametrization of Kc = ⟨t,c,k⟩ by the literal restricted final HNN extension.

Equations

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

@[simp]

theorem Undecidability.HostKcModel.restrictedEquivKc_coe (datum : Thue.StandingDatum) (x : Restricted datum) : ↑((restrictedEquivKc datum) x) = (restrictedEmbeddingToGamma datum) x

noncomputable def Undecidability.HostKcModel.restrictedT (datum : Thue.StandingDatum) : Restricted datum

The three path generators in the literal restricted model.

Equations

• Undecidability.HostKcModel.restrictedT datum = HNNExtension.of (Undecidability.HostKcModel.baseT datum)

noncomputable def Undecidability.HostKcModel.restrictedC (datum : Thue.StandingDatum) : Restricted datum

The base generator c in the restricted k,c model.

Equations

• Undecidability.HostKcModel.restrictedC datum = HNNExtension.of (Undecidability.HostKcModel.baseC datum)

noncomputable def Undecidability.HostKcModel.restrictedK (datum : Thue.StandingDatum) : Restricted datum

The stable generator k in the restricted k,c model.

Equations

• Undecidability.HostKcModel.restrictedK datum = HNNExtension.t

@[simp]

theorem Undecidability.HostKcModel.restrictedEquivKc_t (datum : Thue.StandingDatum) : (restrictedEquivKc datum) (restrictedT datum) = ⟨HostYStage.t datum, ⋯⟩

@[simp]

theorem Undecidability.HostKcModel.restrictedEquivKc_c (datum : Thue.StandingDatum) : (restrictedEquivKc datum) (restrictedC datum) = ⟨HostYStage.c datum, ⋯⟩

@[simp]

theorem Undecidability.HostKcModel.restrictedEquivKc_k (datum : Thue.StandingDatum) : (restrictedEquivKc datum) (restrictedK datum) = ⟨HostYStage.k datum, ⋯⟩