Indecomposability of string modules

The endomorphism algebra of a literal string module is the direct sum of its scalar identity direction and the nilpotent ideal spanned by proper graph components. It is therefore local, so every string module is indecomposable.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightModule_end_isLocalRing {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : IsLocalRing (CategoryTheory.End (C.rightModule hmono))

The endomorphism ring of every literal string module is local.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isIso_of_diagonalMorphismCoefficientLinearMap_ne_zero {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) (hf : (C.diagonalMorphismCoefficientLinearMap hmono) f ≠ 0) : CategoryTheory.IsIso f

A string-module endomorphism with nonzero diagonal graph coordinate is an isomorphism.

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

Every literal string module is indecomposable in the raw functor category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModule_indecomposable {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) : CategoryTheory.Indecomposable (C.finiteRightModule hmono)

Every literal string module is indecomposable in the finite-dimensional linear-module category used by the campaign.