Restricting the first attaching map to `⟨t,c⟩` #

The isomorphism following Lemma 3.1 sends the copy of ⟨t,c⟩ in HMinus into Kc = ⟨t,c,k⟩. This file packages that restriction as a homomorphism whose source is the exact CT model used by the second compression stage.

source

noncomputable def Undecidability.HostThetaCT.ctToHMinus (datum : Thue.StandingDatum) :

↥(HostZBaseIntersections.CT datum) →* ↥(HostYStage.HMinus datum)

Regard the exact ⟨t,c⟩ subgroup of the t-stage as a subgroup of HMinus, after applying the final-stage base embedding.

Equations

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

Instances For

source

noncomputable def Undecidability.HostThetaCT.thetaCTtoKc (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) :

↥(HostZBaseIntersections.CT datum) →* ↥(HostZIntersections.Kc datum)

The restriction of the attaching isomorphism following Lemma 3.1 to the path base ⟨t,c⟩, with codomain enlarged to Kc = ⟨t,c,k⟩.

Equations

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

Instances For

source

@[simp]

theorem Undecidability.HostThetaCT.thetaCTtoKc_coe (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (x : ↥(HostZBaseIntersections.CT datum)) :

↑((thetaCTtoKc datum theta) x) = ↑(theta.equiv ((ctToHMinus datum) x))

Coercing the restricted map back to the ambient semantic Borisov group is literally the original attaching map following Lemma 3.1 on the corresponding element of HMinus.

source

@[simp]

theorem Undecidability.HostThetaCT.ctToHMinus_baseT (datum : Thue.StandingDatum) :

(ctToHMinus datum) (HostKcModel.baseT datum) = HostYStage.minusT datum

source

@[simp]

theorem Undecidability.HostThetaCT.ctToHMinus_baseC (datum : Thue.StandingDatum) :

(ctToHMinus datum) (HostKcModel.baseC datum) = HostYStage.minusC datum

source

@[simp]