Positive ordinary paths as string words

The positive embedding of the displayed quiver into its symmetrification is injective on paths. Moreover, an ordinary path which survives the relation quotient is a string when every arrow is read positively. The latter fact uses ordinary path factorization: a positive signed subpath of a positive path is an ordinary subpath, so a killed subpath would kill the whole path.

theorem MagnitudeConjecture.BoundQuiver.StringWord.positivePath_injective {Q : Type u} [Quiver Q] {x y : Q} (p q : Quiver.Path x y) (h : positivePath p = positivePath q) : p = q

The positive embedding of the displayed quiver is injective on paths.

theorem MagnitudeConjecture.BoundQuiver.StringWord.avoidsRelations_positivePath_of_pathMap_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {x y : Q} (p : Quiver.Path x y) (hp : pathMap R p ≠ 0) : AvoidsRelations R (positivePath p)

Every positive ordinary subpath of a surviving positive path also survives the relation quotient.

theorem MagnitudeConjecture.BoundQuiver.StringWord.isReduced_positivePath {Q : Type u} [Quiver Q] {x y : Q} (p : Quiver.Path x y) : IsReduced (positivePath p)

A path containing only positive signed letters is reduced.

theorem MagnitudeConjecture.BoundQuiver.StringWord.avoidsRelations_reverse_positivePath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {x y : Q} (p : Quiver.Path x y) : AvoidsRelations R (Quiver.Path.reverse (positivePath p))

The reverse of a positive path contains no nontrivial positive ordinary subpath.

theorem MagnitudeConjecture.BoundQuiver.StringWord.isString_positivePath_of_pathMap_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {x y : Q} (p : Quiver.Path x y) (hp : pathMap R p ≠ 0) : IsString R (positivePath p)

A surviving ordinary path, read entirely positively, is a string.