Amalgam

Part of the dependency closure of the small undecidable group constructions.

@[reducible, inline]

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

The factor containing the old presented group and the new letters alpha, beta.

Equations

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

@[reducible, inline]

abbrev Undecidability.MillerTancer.Amalgam.RightFactor : Type

The free factor on the separate copies of beta and gamma.

Equations

• Undecidability.MillerTancer.Amalgam.RightFactor = Undecidability.MillerTancer.RightFactor

def Undecidability.MillerTancer.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.MillerTancer.Amalgam.oldLeft P = Monoid.Coprod.inl

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

The element alpha in the left factor.

Equations

• Undecidability.MillerTancer.Amalgam.alphaLeft P = Monoid.Coprod.inr (FreeGroup.of 0)

def Undecidability.MillerTancer.Amalgam.betaLeft {n m : ℕ} (P : FP n m) : LeftFactor P

The element beta in the left factor.

Equations

• Undecidability.MillerTancer.Amalgam.betaLeft P = Monoid.Coprod.inr (FreeGroup.of 1)

@[reducible, inline]

abbrev Undecidability.MillerTancer.Amalgam.betaRight : RightFactor

The element beta in the right factor.

Equations

• Undecidability.MillerTancer.Amalgam.betaRight = Undecidability.MillerTancer.rightBeta

@[reducible, inline]

abbrev Undecidability.MillerTancer.Amalgam.gammaRight : RightFactor

The element gamma in the right factor.

Equations

• Undecidability.MillerTancer.Amalgam.gammaRight = Undecidability.MillerTancer.rightGamma

def Undecidability.MillerTancer.Amalgam.leftBasis {n m : ℕ} (P : FP n m) (z w : Word n) : Fin 5 → LeftFactor P

The five proposed free generators in the left factor.

Equations

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

@[reducible, inline]

abbrev Undecidability.MillerTancer.Amalgam.rightBasis : Fin 5 → RightFactor

The five proposed free generators in the right factor.

Equations

• Undecidability.MillerTancer.Amalgam.rightBasis = Undecidability.MillerTancer.rightBasis

def Undecidability.MillerTancer.Amalgam.leftMap {n m : ℕ} (P : FP n m) (z w : Word n) : FreeGroup (Fin 5) →* LeftFactor P

The homomorphism freely extending the left amalgamating basis.

Equations

• Undecidability.MillerTancer.Amalgam.leftMap P z w = FreeGroup.lift (Undecidability.MillerTancer.Amalgam.leftBasis P z w)

@[reducible, inline]

abbrev Undecidability.MillerTancer.Amalgam.rightMap : FreeGroup (Fin 5) →* RightFactor

The homomorphism freely extending the right amalgamating basis.

Equations

• Undecidability.MillerTancer.Amalgam.rightMap = Undecidability.MillerTancer.rightBasisMap

inductive Undecidability.MillerTancer.Amalgam.Side : Type

The two sides of the amalgamation diagram.

• left : Side
• right : Side

def Undecidability.MillerTancer.Amalgam.Factor {n m : ℕ} (P : FP n m) : Side → Type

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

Equations

• Undecidability.MillerTancer.Amalgam.Factor P Undecidability.MillerTancer.Amalgam.Side.left = Undecidability.MillerTancer.Amalgam.LeftFactor P
• Undecidability.MillerTancer.Amalgam.Factor P Undecidability.MillerTancer.Amalgam.Side.right = Undecidability.MillerTancer.Amalgam.RightFactor

@[instance_reducible]

instance Undecidability.MillerTancer.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.

def Undecidability.MillerTancer.Amalgam.diagram {n m : ℕ} (P : FP n m) (z w : Word n) (s : Side) : FreeGroup (Fin 5) →* Factor P s

The two homomorphisms identifying the amalgamating subgroup.

Equations

• Undecidability.MillerTancer.Amalgam.diagram P z w Undecidability.MillerTancer.Amalgam.Side.left = Undecidability.MillerTancer.Amalgam.leftMap P z w
• Undecidability.MillerTancer.Amalgam.diagram P z w Undecidability.MillerTancer.Amalgam.Side.right = Undecidability.MillerTancer.Amalgam.rightMap

@[reducible, inline]

abbrev Undecidability.MillerTancer.Amalgam.Pushout {n m : ℕ} (P : FP n m) (z w : Word n) : Type

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

Equations

• Undecidability.MillerTancer.Amalgam.Pushout P z w = Monoid.PushoutI (Undecidability.MillerTancer.Amalgam.diagram P z w)

def Undecidability.MillerTancer.Amalgam.pushLeft {n m : ℕ} (P : FP n m) (z w : Word n) : LeftFactor P →* Pushout P z w

The canonical homomorphism from the left factor into the pushout.

Equations

• Undecidability.MillerTancer.Amalgam.pushLeft P z w = Monoid.PushoutI.of Undecidability.MillerTancer.Amalgam.Side.left

def Undecidability.MillerTancer.Amalgam.pushRight {n m : ℕ} (P : FP n m) (z w : Word n) : RightFactor →* Pushout P z w

The canonical homomorphism from the right factor into the pushout.

Equations

• Undecidability.MillerTancer.Amalgam.pushRight P z w = Monoid.PushoutI.of Undecidability.MillerTancer.Amalgam.Side.right

theorem Undecidability.MillerTancer.Amalgam.identifies_basis {n m : ℕ} (P : FP n m) (z w : Word n) (i : Fin 5) : (pushLeft P z w) (leftBasis P z w i) = (pushRight P z w) (rightBasis i)

theorem Undecidability.MillerTancer.Amalgam.identifies_beta {n m : ℕ} (P : FP n m) (z w : Word n) : (pushLeft P z w) (betaLeft P) = (pushRight P z w) betaRight

def Undecidability.MillerTancer.Amalgam.witnessGenerator {n m : ℕ} (P : FP n m) (z w : Word n) : Fin (n + 3) → Pushout P z w

Interpretation of the generators of the transformed presentation in the amalgam.

Equations

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

@[simp]

theorem Undecidability.MillerTancer.Amalgam.witnessGenerator_old {n m : ℕ} (P : FP n m) (z w : Word n) (i : Fin n) : witnessGenerator P z w (oldGenerator i) = (pushLeft P z w) ((oldLeft P) (PresentedGroup.of i))

@[simp]

theorem Undecidability.MillerTancer.Amalgam.witnessGenerator_alpha {n m : ℕ} (P : FP n m) (z w : Word n) : witnessGenerator P z w (Fin.natAdd n 0) = (pushLeft P z w) (alphaLeft P)

@[simp]

theorem Undecidability.MillerTancer.Amalgam.witnessGenerator_beta {n m : ℕ} (P : FP n m) (z w : Word n) : witnessGenerator P z w (Fin.natAdd n 1) = (pushLeft P z w) (betaLeft P)

@[simp]

theorem Undecidability.MillerTancer.Amalgam.witnessGenerator_gamma {n m : ℕ} (P : FP n m) (z w : Word n) : witnessGenerator P z w (Fin.natAdd n 2) = (pushRight P z w) gammaRight

theorem Undecidability.MillerTancer.Amalgam.eval_oldWord_witness {n m : ℕ} (P : FP n m) (z w u : Word n) : Word.eval (witnessGenerator P z w) (oldWord u) = (pushLeft P z w) ((oldLeft P) (P.evalWord u))

theorem Undecidability.MillerTancer.Amalgam.eval_oldGenerators_witness {n m : ℕ} (P : FP n m) (z w u : Word n) : Word.eval (fun (i : Fin n) => (pushLeft P z w) ((oldLeft P) (PresentedGroup.of i))) u = (pushLeft P z w) ((oldLeft P) (P.evalWord u))

theorem Undecidability.MillerTancer.Amalgam.eval_sigma₁_witness {n m : ℕ} (P : FP n m) (z w : Word n) : Word.eval (witnessGenerator P z w) (sigma₁ n) = 1

theorem Undecidability.MillerTancer.Amalgam.eval_sigma₂_witness {n m : ℕ} (P : FP n m) (z w : Word n) : Word.eval (witnessGenerator P z w) (sigma₂ n) = 1

theorem Undecidability.MillerTancer.Amalgam.eval_sigma₃_witness {n m : ℕ} (P : FP n m) (z w : Word n) : Word.eval (witnessGenerator P z w) (sigma₃ w) = 1

theorem Undecidability.MillerTancer.Amalgam.eval_sigma₄_witness {n m : ℕ} (P : FP n m) (z w : Word n) : Word.eval (witnessGenerator P z w) (sigma₄ z) = 1

theorem Undecidability.MillerTancer.Amalgam.transformed_relator_eq_one {n m : ℕ} (P : FP n m) (z w : Word n) (i : Fin (m + 4)) : Word.eval (witnessGenerator P z w) ((transform P z w).relator i) = 1

def Undecidability.MillerTancer.Amalgam.witnessHom {n m : ℕ} (P : FP n m) (z w : Word n) : (transform P z w).Group →* Pushout P z w

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

Equations

• Undecidability.MillerTancer.Amalgam.witnessHom P z w = (Undecidability.MillerTancer.transform P z w).homOfRelators (Undecidability.MillerTancer.Amalgam.witnessGenerator P z w) ⋯

@[simp]

theorem Undecidability.MillerTancer.Amalgam.witnessHom_of {n m : ℕ} (P : FP n m) (z w : Word n) (i : Fin (n + 3)) : (witnessHom P z w) (PresentedGroup.of i) = witnessGenerator P z w i

theorem Undecidability.MillerTancer.Amalgam.transform_not_trivial_of_basis_injective {n m : ℕ} (P : FP n m) (z w : Word n) (hleft : Function.Injective ⇑(leftMap P z w)) (hright : Function.Injective ⇑rightMap) (hw : ¬P.wordProblem w) : ¬(transform P z w).presentsTrivial

The amalgamated-product half of the Miller--Tancer construction, conditional only on the two separated-conjugates maps being injective.