LeanPool.SmallUndecidableGroups.AdianRabin.Gordon.Amalgam

Gordon's uncompressed presentation as a free product with amalgamation.

source

@[reducible, inline]

abbrev Undecidability.Gordon.Amalgam.LeftFactor {n m : ℕ} (P : FP n m) :

Type

The left factor of the free product used to construct the amalgam.

Equations

Undecidability.Gordon.Amalgam.LeftFactor P = Monoid.Coprod P.Group (FreeGroup (Fin 2))

Instances For

source

@[reducible, inline]

abbrev Undecidability.Gordon.Amalgam.RightFactor :

Type

The right free factor used to construct the amalgam.

Equations

Undecidability.Gordon.Amalgam.RightFactor = Undecidability.Gordon.RightFactor

Instances For

source

def Undecidability.Gordon.Amalgam.oldLeft {n m : ℕ} (P : FP n m) :

P.Group →* LeftFactor P

The inclusion of the original presented group into the left factor.

Equations

Undecidability.Gordon.Amalgam.oldLeft P = Monoid.Coprod.inl

Instances For

source

def Undecidability.Gordon.Amalgam.aLeft {n m : ℕ} (P : FP n m) :

LeftFactor P

The element a in the left factor.

Equations

Undecidability.Gordon.Amalgam.aLeft P = Monoid.Coprod.inr (FreeGroup.of 0)

Instances For

source

def Undecidability.Gordon.Amalgam.alphaLeft {n m : ℕ} (P : FP n m) :

LeftFactor P

The element alpha in the left factor.

Equations

Undecidability.Gordon.Amalgam.alphaLeft P = Monoid.Coprod.inr (FreeGroup.of 1)

Instances For

source

@[reducible, inline]

abbrev Undecidability.Gordon.Amalgam.bRight :

RightFactor

The element b in the right factor.

Equations

Undecidability.Gordon.Amalgam.bRight = Undecidability.Gordon.rightB

Instances For

source

@[reducible, inline]

abbrev Undecidability.Gordon.Amalgam.betaRight :

RightFactor

The element beta in the right factor.

Equations

Undecidability.Gordon.Amalgam.betaRight = Undecidability.Gordon.rightBeta

Instances For

source

@[reducible, inline]

abbrev Undecidability.Gordon.Amalgam.rightConjugate (r : ℕ) :

RightFactor

The conjugate of b by the indicated power of beta.

Equations

Undecidability.Gordon.Amalgam.rightConjugate r = Undecidability.Gordon.rightU r

Instances For

source

def Undecidability.Gordon.Amalgam.leftBasis {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

BasisIndex n → LeftFactor P

The left-hand amalgamating words in Gordon's Lemma 2.1.

Equations

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

Instances For

source

@[reducible, inline]

abbrev Undecidability.Gordon.Amalgam.rightBasis (n : ℕ) :

BasisIndex n → RightFactor

The corresponding right-hand free basis.

Equations

Undecidability.Gordon.Amalgam.rightBasis n = Undecidability.Gordon.rightBasis

Instances For

source

def Undecidability.Gordon.Amalgam.leftMap {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

FreeGroup (BasisIndex n) →* LeftFactor P

The homomorphism freely extending the left amalgamating basis.

Equations

Undecidability.Gordon.Amalgam.leftMap P data w = FreeGroup.lift (Undecidability.Gordon.Amalgam.leftBasis P data w)

Instances For

source

@[reducible, inline]

abbrev Undecidability.Gordon.Amalgam.rightMap (n : ℕ) :

FreeGroup (BasisIndex n) →* RightFactor

The homomorphism freely extending the right amalgamating basis.

Equations

Undecidability.Gordon.Amalgam.rightMap n = Undecidability.Gordon.rightBasisMap n

Instances For

source

inductive Undecidability.Gordon.Amalgam.Side :

Type

The two sides of the amalgamation diagram.

left : Side
right : Side

Instances For

source

def Undecidability.Gordon.Amalgam.Factor {n m : ℕ} (P : FP n m) :

Side → Type

The free-product factor on the chosen side of the diagram.

Equations

Instances For

source

@[instance_reducible]

instance Undecidability.Gordon.Amalgam.factorGroup {n m : ℕ} (P : FP n m) (s : Side) :

Group (Factor P s)

Equations

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

source

def Undecidability.Gordon.Amalgam.diagram {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (s : Side) :

FreeGroup (BasisIndex n) →* Factor P s

The two homomorphisms identifying the amalgamating subgroup.

Equations

Instances For

source

@[reducible, inline]

abbrev Undecidability.Gordon.Amalgam.Pushout {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

Type

The group obtained by taking the pushout of the amalgamation diagram.

Equations

Undecidability.Gordon.Amalgam.Pushout P data w = Monoid.PushoutI (Undecidability.Gordon.Amalgam.diagram P data w)

Instances For

source

def Undecidability.Gordon.Amalgam.pushLeft {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

LeftFactor P →* Pushout P data w

The canonical homomorphism from the left factor into the pushout.

Equations

Undecidability.Gordon.Amalgam.pushLeft P data w = Monoid.PushoutI.of Undecidability.Gordon.Amalgam.Side.left

Instances For

source

def Undecidability.Gordon.Amalgam.pushRight {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

RightFactor →* Pushout P data w

The canonical homomorphism from the right factor into the pushout.

Equations

Undecidability.Gordon.Amalgam.pushRight P data w = Monoid.PushoutI.of Undecidability.Gordon.Amalgam.Side.right

Instances For

source

theorem Undecidability.Gordon.Amalgam.identifies_basis {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (i : BasisIndex n) :

(pushLeft P data w) (leftBasis P data w i) = (pushRight P data w) (rightBasis n i)

source

def Undecidability.Gordon.Amalgam.witnessGenerator {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

Fin 2 → Pushout P data w

Interpret the two generators of the compressed presentation.

Equations

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

Instances For

source

@[simp]

theorem Undecidability.Gordon.Amalgam.witnessGenerator_a {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

witnessGenerator P data w 0 = (pushLeft P data w) (aLeft P)

source

@[simp]

theorem Undecidability.Gordon.Amalgam.witnessGenerator_b {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

witnessGenerator P data w 1 = (pushRight P data w) bRight

source

theorem Undecidability.Gordon.Amalgam.eval_alpha_witness {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

Word.eval (witnessGenerator P data w) alphaWord = (pushLeft P data w) (alphaLeft P)

source

theorem Undecidability.Gordon.Amalgam.eval_beta_witness {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

Word.eval (witnessGenerator P data w) betaWord = (pushRight P data w) betaRight

source

theorem Undecidability.Gordon.Amalgam.eval_rightConjugateWord_witness {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (r : ℕ) :

Word.eval (witnessGenerator P data w) (rightConjugateWord r) = (pushRight P data w) (rightConjugate r)

source

theorem Undecidability.Gordon.Amalgam.eval_encodedGenerator_witness {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (i : Fin n) :

Word.eval (witnessGenerator P data w) (encodedGenerator data i) = (pushLeft P data w) ((oldLeft P) (PresentedGroup.of i))

source

theorem Undecidability.Gordon.Amalgam.eval_encodeWord_witness {n m : ℕ} (P : FP n m) (data : TorsionData P) (w u : Word n) :

Word.eval (witnessGenerator P data w) (encodeWord data u) = (pushLeft P data w) ((oldLeft P) (P.evalWord u))

source

theorem Undecidability.Gordon.Amalgam.eval_additional {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

Word.eval (witnessGenerator P data w) (additionalRelator data w) = 1

source

theorem Undecidability.Gordon.Amalgam.transformed_relator_eq_one {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (i : Fin (m + 1)) :

Word.eval (witnessGenerator P data w) ((transform P data w).relator i) = 1

source

def Undecidability.Gordon.Amalgam.witnessHom {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :

(transform P data w).Group →* Pushout P data w

The relator-preserving homomorphism from the transformed presentation into the amalgam.

Equations

Undecidability.Gordon.Amalgam.witnessHom P data w = (Undecidability.Gordon.transform P data w).homOfRelators (Undecidability.Gordon.Amalgam.witnessGenerator P data w) ⋯

Instances For

source

@[simp]

theorem Undecidability.Gordon.Amalgam.witnessHom_of {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (i : Fin 2) :

(witnessHom P data w) (PresentedGroup.of i) = witnessGenerator P data w i

source

theorem Undecidability.Gordon.Amalgam.transform_not_trivial_of_basis_injective {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (hleft : Function.Injective ⇑(leftMap P data w)) (hright : Function.Injective ⇑(rightMap n)) (hw : ¬P.wordProblem w) :

¬(transform P data w).presentsTrivial

The amalgamated-product argument, conditional on the two free-basis injectivity lemmas.