Reflection from a finite string-detector filtration

At every displayed vertex, the two endpoint-word filtrations form a finite lexicographic grid. Its successive quotients are pair detectors; invalid pairs vanish, while valid pairs are naturally ordinary string detectors. Reversal invariance then shows that the finite inversion-class family detects every layer. The successive-quotient theorem makes every vertex component bijective and hence reflects module isomorphisms.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.app_bijective_of_endpointDetectorLinearMap_bijective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [Finite (DetectorIndex S)] {f : M ⟶ N} [M.Additive] [N.Additive] (hdetector : ∀ {x : Q} {t : Bool} (C : EndpointWord S x t), Function.Bijective ⇑(detectorLinearMap f C)) (x : Q) : Function.Bijective ⇑(ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations x))))

The concrete ordered pair-grid filtration reflects bijectivity as soon as every literal endpoint detector map is bijective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.isIso_of_endpointDetectorLinearMap_bijective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [Finite (DetectorIndex S)] {f : M ⟶ N} [M.Additive] [N.Additive] (hdetector : ∀ {x : Q} {t : Bool} (C : EndpointWord S x t), Function.Bijective ⇑(detectorLinearMap f C)) : CategoryTheory.IsIso f

Literal endpoint detectors jointly reflect isomorphisms through the ordered pair-grid filtration.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.isIso_of_detectorIndexLinearMap_bijective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [Finite (DetectorIndex S)] {f : M ⟶ N} [M.Additive] [N.Additive] (hdetector : ∀ (i : DetectorIndex S), Function.Bijective ⇑(detectorLinearMap f i.endpointWord)) : CategoryTheory.IsIso f

The chosen finite detector indices jointly reflect isomorphisms. Reversal invariance supplies every literal endpoint detector required by the grid.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.isIso_of_finiteDetectorFunctor_map {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} [Finite (DetectorIndex S)] {M N : CoveringHom.FiniteDimensionalModuleCategory k} (f : M ⟶ N) (hdetector : ∀ (i : DetectorIndex S), CategoryTheory.IsIso (i.finiteDetectorFunctor.map f)) : CategoryTheory.IsIso f

On finite-dimensional modules, the finite family of chosen string detectors jointly reflects isomorphisms.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.isIso_reconstructionEvaluation {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} [Fintype (DetectorIndex S)] (N : CoveringHom.FiniteDimensionalModuleCategory k) : CategoryTheory.IsIso (reconstructionEvaluation N)

Every finite-dimensional module over a representation-finite string algebra is isomorphic to the finite direct sum reconstructed from all of its string detectors.