Documentation

LeanPool.SmallUndecidableGroups.AdianRabin.Gordon.RightBasis

The shared right factor, free basis and lift used by the amalgam and normal-form models.

source
inductive Undecidability.Gordon.BasisIndex (n : ℕ) :
Type

The common free basis used to describe Gordon's uncompressed free-product-with-amalgamation presentation.

Instances For
    source
    def Undecidability.Gordon.instDecidableEqBasisIndex.decEq {n✝ : ℕ} (x✝ x✝¹ : BasisIndex n✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Undecidability.Gordon.instDecidableEqBasisIndex {n✝ : ℕ} :
      DecidableEq (BasisIndex n✝)
      Equations
      source
      @[reducible, inline]
      abbrev Undecidability.Gordon.RightFactor :
      Type

      The right free factor used to construct the amalgam.

      Equations
      Instances For
        source
        def Undecidability.Gordon.rightB :
        RightFactor

        The free generator b of the right-hand factor.

        Equations
        Instances For
          source
          def Undecidability.Gordon.rightBeta :
          RightFactor

          The free generator beta of the right-hand factor.

          Equations
          Instances For
            source
            def Undecidability.Gordon.rightU (r : ℕ) :
            RightFactor

            Gordon's right-hand conjugate beta^(-r) * b * beta^r.

            Equations
            Instances For
              source
              def Undecidability.Gordon.rightBasis {n : ℕ} :
              BasisIndex n → RightFactor

              The right-hand amalgamating elements in Gordon's construction.

              Equations
              Instances For
                source
                def Undecidability.Gordon.rightBasisMap (n : ℕ) :
                FreeGroup (BasisIndex n) →* RightFactor

                The homomorphism freely extending Gordon’s right-hand amalgamating basis.

                Equations
                Instances For