Finite-string detector reconstruction map

When the inversion-class index of finite strings is finite, the coherent evaluations assemble into one map from the biproduct of all detector-generated string summands. Applying any matching detector to this total map is an isomorphism.

@[instance_reducible]

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.instDecidableEq_2 {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} : DecidableEq (DetectorIndex S)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.reconstructionSummand {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) : CoveringHom.FiniteDimensionalModuleCategory k

The string summand generated by the ith detector of N.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.reconstructionSource {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) : CoveringHom.FiniteDimensionalModuleCategory k

The finite biproduct of all detector-generated string summands.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.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) : reconstructionSource N ⟶ N

The total coherent evaluation from all detector-generated string summands to N.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.reconstruction_inclusion_comp_evaluation {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) (i : DetectorIndex S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (reconstructionSummand N) i) (reconstructionEvaluation N) = coherentFiniteDetectorEvaluation N i

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorFunctor_map_reconstructionEvaluation_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} [Fintype (DetectorIndex S)] (N : CoveringHom.FiniteDimensionalModuleCategory k) (j : DetectorIndex S) : Function.Surjective ⇑(ModuleCat.Hom.hom (j.finiteDetectorFunctor.map (reconstructionEvaluation N)).hom)

Every matching detector of the total reconstruction map is surjective: its matching summand already maps onto the target detector.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorFunctorReconstructionSourceIso {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 : DetectorIndex S) : j.finiteDetectorFunctor.obj (reconstructionSource N) ≅ ⨁ fun (i : DetectorIndex S) => (j.finiteDetectorEmbeddingFunctor i).obj (i.finiteDetectorFunctor.obj N)

Applying a finite detector to the reconstruction source commutes with its finite biproduct decomposition.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finrank_finiteDetectorFunctor_reconstructionSource {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 : DetectorIndex S) : Module.finrank k ↑(j.finiteDetectorFunctor.obj (reconstructionSource N)) = Module.finrank k ↑(j.finiteDetectorFunctor.obj N)

Orthogonality makes the detector of the total reconstruction source have the same dimension as the corresponding detector of N.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.isIso_finiteDetectorFunctor_map_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) (j : DetectorIndex S) : CategoryTheory.IsIso (j.finiteDetectorFunctor.map (reconstructionEvaluation N))

Every finite-string detector sees the total reconstruction evaluation as an isomorphism.