Finite string-sum coverage from string detectors

The finite detector reconstruction writes every finite-dimensional module as a biproduct of coefficient-valued literal string modules. A finite coefficient space is a biproduct of copies of the ground field, so the reconstruction flattens to a finite biproduct of literal string modules.

This is the direct object-coverage input for hook and cohook irreducibility; it does not pass through a separate string-or-band classification theorem.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.reconstructionMultiplicity {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} (N : CoveringHom.FiniteDimensionalModuleCategory k) (i : DetectorIndex S) : ℕ

The multiplicity with which the detector representative i occurs in the reconstruction of N.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.ReconstructionCopyIndex {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} (N : CoveringHom.FiniteDimensionalModuleCategory k) : Type u

One label for each literal string copy occurring in the detector reconstruction.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.reconstructionCopyEquiv {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) : Fin (Fintype.card (ReconstructionCopyIndex N)) ≃ ReconstructionCopyIndex N

A numerical enumeration of all literal string copies in the detector reconstruction.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.reconstructionWord {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) (j : Fin (Fintype.card (ReconstructionCopyIndex N))) : Word P.relations

The literal word carried by a numerical reconstruction-copy label.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.reconstructionSummandIsoBiproduct {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} (N : CoveringHom.FiniteDimensionalModuleCategory k) (i : DetectorIndex S) : reconstructionSummand N i ≅ ⨁ fun (x : Fin (reconstructionMultiplicity N i)) => i.endpointWord.word.finiteRightModule ⋯

A coefficient-valued reconstruction summand is a finite biproduct of copies of its literal string module.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.reconstructionSourceIsoFiniteStringBiproduct {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) : reconstructionSource N ≅ ⨁ fun (j : Fin (Fintype.card (ReconstructionCopyIndex N))) => (reconstructionWord N j).finiteRightModule ⋯

The complete reconstruction source is a single finite biproduct of literal string modules, with nested detector/coefficient indices flattened and enumerated by a Fin type.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.reconstructionIsoFiniteStringBiproduct {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) : N ≅ ⨁ fun (j : Fin (Fintype.card (ReconstructionCopyIndex N))) => (reconstructionWord N j).finiteRightModule ⋯

The detector reconstruction identifies a finite-dimensional module itself with a finite biproduct of literal string modules.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.everyFiniteModuleIsFiniteStringSum {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)] : Word.EveryFiniteModuleIsFiniteStringSum ⋯

Every finite-dimensional module is a finite biproduct of literal string modules. This follows directly from the detector reconstruction theorem.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.finiteModuleMap_isIrreducible {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 D : Word P.relations} (hook : C.HookExtension D) (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (hook.finiteModuleMap ⋯)

The canonical right-hook projection is irreducible once the finite detector family exists.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.finiteModuleMap_isIrreducible {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 D : Word P.relations} (cohook : C.CohookExtension D) (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (cohook.finiteModuleMap ⋯)

The canonical right-cohook inclusion is irreducible once the finite detector family exists.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.finiteModuleMap_isIrreducible {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} (hook : C.LeftHookExtension) (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (hook.finiteModuleMap ⋯)

The canonical left-hook projection is irreducible once the finite detector family exists.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.finiteModuleMap_isIrreducible {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} (cohook : C.LeftCohookExtension) (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (cohook.finiteModuleMap ⋯)

The canonical left-cohook inclusion is irreducible once the finite detector family exists.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.finiteModuleMap_isIrreducible_of_finiteIndecomposableSkeleton {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 D : Word P.relations} (hook : C.HookExtension D) (S : P.ArrowPolarization) (T : DetectorIndex.FiniteIndecomposableSkeleton) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (hook.finiteModuleMap ⋯)

A finite complete indecomposable skeleton makes the right-hook projection irreducible, with detector finiteness discharged internally.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.finiteModuleMap_isIrreducible_of_finiteIndecomposableSkeleton {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 D : Word P.relations} (cohook : C.CohookExtension D) (S : P.ArrowPolarization) (T : DetectorIndex.FiniteIndecomposableSkeleton) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (cohook.finiteModuleMap ⋯)

A finite complete indecomposable skeleton makes the right-cohook inclusion irreducible, with detector finiteness discharged internally.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.finiteModuleMap_isIrreducible_of_finiteIndecomposableSkeleton {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} (hook : C.LeftHookExtension) (S : P.ArrowPolarization) (T : DetectorIndex.FiniteIndecomposableSkeleton) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (hook.finiteModuleMap ⋯)

A finite complete indecomposable skeleton makes the left-hook projection irreducible, with detector finiteness discharged internally.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.finiteModuleMap_isIrreducible_of_finiteIndecomposableSkeleton {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} (cohook : C.LeftCohookExtension) (S : P.ArrowPolarization) (T : DetectorIndex.FiniteIndecomposableSkeleton) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (cohook.finiteModuleMap ⋯)

A finite complete indecomposable skeleton makes the left-cohook inclusion irreducible, with detector finiteness discharged internally.