Documentation

LeanPool.SmallUndecidableGroups.AdianRabin.Gordon.Embedding

The free-product embeddings needed for Gordon's nontriviality direction.

source
def Undecidability.Gordon.LeftBridge.oldToSplit {n m : ℕ} (P : FP n m) :
P.Group →* LeftNormalForm.SplitLeft P.Group

The inclusion of the original group into the separated free factors.

Equations
Instances For
    source
    def Undecidability.Gordon.LeftBridge.newToSplit {n m : ℕ} (P : FP n m) :
    FreeGroup (Fin 2) →* LeftNormalForm.SplitLeft P.Group

    The homomorphism assigning the new free generators to their separated factors.

    Equations
    Instances For
      source
      def Undecidability.Gordon.LeftBridge.comparison {n m : ℕ} (P : FP n m) :
      Amalgam.LeftFactor P →* LeftNormalForm.SplitLeft P.Group

      The homomorphism comparing the two bracketings of the free product.

      Equations
      Instances For
        source
        @[simp]
        theorem Undecidability.Gordon.LeftBridge.comparison_old {n m : ℕ} (P : FP n m) (g : P.Group) :
        (comparison P) ((Amalgam.oldLeft P) g) = MillerTancer.LeftNormalForm.old g
        source
        @[simp]
        theorem Undecidability.Gordon.LeftBridge.comparison_a {n m : ℕ} (P : FP n m) :
        (comparison P) (Amalgam.aLeft P) = LeftNormalForm.a
        source
        @[simp]
        theorem Undecidability.Gordon.LeftBridge.comparison_alpha {n m : ℕ} (P : FP n m) :
        (comparison P) (Amalgam.alphaLeft P) = LeftNormalForm.auxiliaryAlpha
        source
        theorem Undecidability.Gordon.LeftBridge.comparison_leftBasis {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (i : BasisIndex n) :
        (comparison P) (Amalgam.leftBasis P data w i) = LeftNormalForm.splitBasis data.degree (fun (j : Fin n) => PresentedGroup.of j) (P.evalWord w) i
        source
        theorem Undecidability.Gordon.LeftBridge.comparison_comp_leftMap {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) :
        (comparison P).comp (Amalgam.leftMap P data w) = FreeGroup.lift (LeftNormalForm.splitBasis data.degree (fun (j : Fin n) => PresentedGroup.of j) (P.evalWord w))
        source
        theorem Undecidability.Gordon.LeftBridge.leftMap_injective {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (hw : P.evalWord w ≠ 1) :
        Function.Injective ⇑(Amalgam.leftMap P data w)
        source
        theorem Undecidability.Gordon.amalgam_rightMap_eq (n : ℕ) :
        Amalgam.rightMap n = rightBasisMap n
        source
        theorem Undecidability.Gordon.amalgam_rightMap_injective (n : ℕ) :
        Function.Injective ⇑(Amalgam.rightMap n)
        source
        theorem Undecidability.Gordon.transform_not_trivial_of_not_wordProblem {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (hw : ¬P.wordProblem w) :
        ¬(transform P data w).presentsTrivial

        The hard implication in Gordon's Lemma 2.1: a nontrivial input word remains visible in the amalgamated-product witness.