Isomorphism classification of literal finite string modules

The finite detector family separates inversion classes. Applying one detector to an isomorphism between two literal string modules therefore shows that the underlying words agree up to formal reversal.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteReverseRightModuleIso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} (C : Word P.relations) : C.finiteRightModule ⋯ ≅ (reverse P.relations C).finiteRightModule ⋯

Reversal of words, bundled in the finite-dimensional linear-module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.eq_or_eq_reverse_of_finiteRightModule_iso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} (S : P.ArrowPolarization) (C D : Word P.relations) (e : C.finiteRightModule ⋯ ≅ D.finiteRightModule ⋯) : C = D ∨ C = Word.reverse P.relations D

Two literal finite string modules are isomorphic only when their words agree up to formal reversal.