Classification of a finite indecomposable skeleton by strings

Detector reconstruction writes every finite-dimensional module as a finite biproduct of literal string modules. If the module is indecomposable, its local endomorphism ring forces one coordinate projection of this biproduct to be an isomorphism. Consequently the already injective map from detector indices to any complete finite indecomposable skeleton is also surjective.

This is the duplicate-free object-classification interface needed by the Butler--Ringel almost-split argument. It introduces no periodic-string or band-module compatibility layer.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteSkeletonLabel_surjective {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} (T : FiniteIndecomposableSkeleton) : Function.Surjective (finiteSkeletonLabel T)

Every label of a complete finite indecomposable skeleton is represented by the literal string belonging to a detector index.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteSkeletonEquiv {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} (T : FiniteIndecomposableSkeleton) : DetectorIndex S ≃ Fin T.n

Detector indices and the labels of any complete duplicate-free finite indecomposable skeleton are canonically equivalent after making the existing classical choices.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.detectorIndexOfFiniteSkeletonLabel {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} (T : FiniteIndecomposableSkeleton) (j : Fin T.n) : DetectorIndex S

The detector index chosen to represent one finite-skeleton label.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteSkeletonLabel_detectorIndexOfFiniteSkeletonLabel {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} (T : FiniteIndecomposableSkeleton) (j : Fin T.n) : finiteSkeletonLabel T (detectorIndexOfFiniteSkeletonLabel T j) = j

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteSkeletonStringIso {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} (T : FiniteIndecomposableSkeleton) (j : Fin T.n) : (detectorIndexOfFiniteSkeletonLabel T j).endpointWord.word.finiteRightModule ⋯ ≅ T.obj j

The literal string canonically selected for a finite-skeleton label is isomorphic to that skeleton object.