Diagonal coefficients of string-module endomorphisms

Naturality makes the diagonal coefficient of any endomorphism constant along the complete word, including when displayed vertices repeat. The source position also shows directly that every literal string representation is a nonzero object.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.endomorphismCoefficient {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ C.rightModule hmono) {x : Q} (i : C.PositionAt x) : k

The diagonal coefficient of a natural endomorphism at a position basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.endomorphismCoefficient_eq_of_arrowStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ C.rightModule hmono) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.ArrowStep a i j) : C.endomorphismCoefficient hmono f i = C.endomorphismCoefficient hmono f j

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.endomorphismCoefficient_eq_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ C.rightModule hmono) {x : Q} (i : C.PositionAt x) : C.endomorphismCoefficient hmono f i = C.endomorphismCoefficient hmono f C.sourcePosition

The diagonal coefficient of an endomorphism is constant along every string word, including words with repeated displayed vertices.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightModule_not_isZero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : ¬CategoryTheory.Limits.IsZero (C.rightModule hmono)

Every string representation is a nonzero object of the raw functor category.