Magnitude conjecture

MagnitudeConjecture.Algebra.StringReducedReverse

A reduced signed path is not a nontrivial reverse palindrome #

We forget the vertices of a signed path but retain each displayed arrow and its orientation. This gives a word in a free group. String reducedness is exactly enough to make this free-group word reduced, while formal path reversal becomes inverse-word reversal. Torsion-freeness of free groups then excludes a positive-length reduced path equal to its own reverse.

source
def MagnitudeConjecture.BoundQuiver.StringWord.SignedGenerator (Q : Type u) [Quiver Q] :
Type u

A displayed-quiver arrow with its two endpoints retained.

Instances For
    source
    def MagnitudeConjecture.BoundQuiver.StringWord.signedArrowLetter {Q : Type u} [Quiver Q] {x y : Q} (e : SignedArrow x y) :
    SignedGenerator Q × Bool

    Forget the signed endpoints of a symmetrified arrow while retaining its underlying displayed arrow and whether it is traversed inversely.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowLetter_reverse {Q : Type u} [Quiver Q] {x y : Q} (e : SignedArrow x y) :
      signedArrowLetter (Quiver.reverse e) = ((signedArrowLetter e).1, !(signedArrowLetter e).2)
      source
      theorem MagnitudeConjecture.BoundQuiver.StringWord.heq_of_signedArrowLetter_eq {Q : Type u} [Quiver Q] {x y x' y' : Q} {e : SignedArrow x y} {f : SignedArrow x' y'} (h : signedArrowLetter e = signedArrowLetter f) :
      e ≍ f

      The erased signed-arrow letter retains the whole dependent signed arrow.

      source
      theorem MagnitudeConjecture.BoundQuiver.StringWord.heq_of_signedArrowLetter_negativeArrow_eq {Q : Type u} [Quiver Q] {x y x' y' : Q} {a : x ⟶ y} {b : x' ⟶ y'} (h : signedArrowLetter (negativeArrow a) = signedArrowLetter (negativeArrow b)) :
      a ≍ b

      Equality of erased negative letters retains the underlying displayed arrows, including their dependent endpoints.

      source
      theorem MagnitudeConjecture.BoundQuiver.StringWord.heq_positiveArrow_reverse_negativeArrow_of_signedArrowLetter_eq {Q : Type u} [Quiver Q] {x y x' y' : Q} {a : x ⟶ y} {b : x' ⟶ y'} (h : signedArrowLetter (negativeArrow a) = signedArrowLetter (negativeArrow b)) :
      positiveArrow b ≍ Quiver.reverse (negativeArrow a)

      Equality of erased negative letters identifies the positive copy of the second arrow with the formal reverse of the negative copy of the first.

      source
      def MagnitudeConjecture.BoundQuiver.StringWord.signedPathWord {Q : Type u} [Quiver Q] {x y : Quiver.Symmetrify Q} :
      Quiver.Path x y → List (SignedGenerator Q × Bool)

      The free-group word of a signed path, listed from its final letter backwards to match Quiver.Path recursion.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathWord_comp {Q : Type u} [Quiver Q] {x y z : Quiver.Symmetrify Q} (p : Quiver.Path x y) (q : Quiver.Path y z) :
        signedPathWord (p.comp q) = signedPathWord q ++ signedPathWord p
        source
        @[simp]
        theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathWord_toPath {Q : Type u} [Quiver Q] {x y : Q} (e : SignedArrow x y) :
        signedPathWord (Quiver.Hom.toPath e) = [signedArrowLetter e]
        source
        @[simp]
        theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathWord_reverse {Q : Type u} [Quiver Q] {x y : Q} (p : SignedPath x y) :
        signedPathWord (Quiver.Path.reverse p) = FreeGroup.invRev (signedPathWord p)
        source
        @[simp]
        theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathWord_length {Q : Type u} [Quiver Q] {x y : Quiver.Symmetrify Q} (p : Quiver.Path x y) :
        (signedPathWord p).length = p.length
        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.IsReduced.signedArrowLetter_sign_eq_of_cons {Q : Type u} [Quiver Q] {a b c d : Q} (q : SignedPath a b) (f : SignedArrow b c) (e : SignedArrow c d) (hred : IsReduced ((Quiver.Path.cons q f).cons e)) (hgenerator : (signedArrowLetter e).1 = (signedArrowLetter f).1) :
        (signedArrowLetter e).2 = (signedArrowLetter f).2

        Adjacent letters in a reduced signed path cannot be opposite orientations of the same displayed generator.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.IsReduced.signedPathWord_isReduced {Q : Type u} [Quiver Q] {x y : Q} (p : SignedPath x y) (hred : IsReduced p) :
        FreeGroup.IsReduced (signedPathWord p)

        A reduced signed path gives a reduced word in the free group on all displayed arrows.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.IsReduced.length_eq_zero_of_signedPathWord_eq_invRev {Q : Type u} [Quiver Q] {x y : Q} (p : SignedPath x y) (hred : IsReduced p) (hreverse : signedPathWord p = FreeGroup.invRev (signedPathWord p)) :
        Quiver.Path.length p = 0

        A reduced signed path whose erased signed-arrow word is equal to its inverse reversal has length zero. This form is useful before the two path endpoints have been identified.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.IsReduced.length_eq_zero_of_eq_reverse {Q : Type u} [Quiver Q] {x : Q} (p : SignedPath x x) (hred : IsReduced p) (hreverse : p = Quiver.Path.reverse p) :
        Quiver.Path.length p = 0

        A reduced loop which is equal to its formal reverse has length zero.