Translation of arrow multiplicities in a finite tau-category

Compatibility of the chosen left and right meshes identifies the middle term of the left mesh at a noninjective label X with the middle term of the right mesh ending at tauMinus X. Comparing the resulting left-mesh unit equation with the corresponding row of the inverse Hom matrix proves the usual translation identity for the official arrow multiplicities:

a(X,Y) = a(Y,tauMinus X).

theorem MagnitudeConjecture.FiniteTauMatrix.leftMeshLabelWeightDefect_eq_translationSum {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (weight : Ind → ℤ) (X : T.Noninjective) : leftMeshLabelWeightDefect T weight ↑X = weight ↑X - ∑ Y : Ind, ↑(arrowMultiplicity T.toFiniteRightTauCategoryData Y (T.tauMinus X)) * weight Y + weight (T.tauMinus X)

The categorical left-mesh defect at a noninjective label, expressed using the right-mesh decomposition at its negative translate.

theorem MagnitudeConjecture.FiniteTauMatrix.meshContribution_row_sum_of_noninjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) [DecidablePred T.IsProjective] (weight : Ind → ℤ) (X : T.Noninjective) : ∑ target : Ind, ARCount.meshContribution T.IsProjective (tau T) (↑X) target * weight target = weight (T.tauMinus X)

The mesh contribution in the row of a noninjective label is the single unit contribution ending at its negative translate.

theorem MagnitudeConjecture.FiniteTauMatrix.meshContribution_row_sum_of_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) [DecidablePred T.IsProjective] (weight : Ind → ℤ) (X : Ind) (hX : T.IsInjective X) : ∑ target : Ind, ARCount.meshContribution T.IsProjective (tau T) X target * weight target = 0

An injective label cannot occur as the translated source of a right mesh, so its row has no mesh contribution.

theorem MagnitudeConjecture.FiniteTauMatrix.meshRowWeight_eq_of_noninjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) [DecidablePred T.IsProjective] (weight : Ind → ℤ) (X : T.Noninjective) : meshRowWeight T weight ↑X = weight ↑X - ∑ Y : Ind, ↑(arrowMultiplicity T.toFiniteRightTauCategoryData (↑X) Y) * weight Y + weight (T.tauMinus X)

A noninjective row of the mesh matrix is identity minus outgoing arrows plus the unit entry at the negative translate.

theorem MagnitudeConjecture.FiniteTauMatrix.meshRowWeight_eq_of_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) [DecidablePred T.IsProjective] (weight : Ind → ℤ) (X : Ind) (hX : T.IsInjective X) : meshRowWeight T weight X = weight X - ∑ Y : Ind, ↑(arrowMultiplicity T.toFiniteRightTauCategoryData X Y) * weight Y

An injective row of the mesh matrix is identity minus its outgoing arrow row, with no translation contribution.

theorem MagnitudeConjecture.FiniteTauMatrix.outgoingArrow_homToWeight_eq_translation {k : Type s} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) [DecidablePred T.IsProjective] (D : HomMeshInverseData T) (leftEpi : ∀ (A : Ind), CategoryTheory.Epi (T.leftMesh (T.obj A)).g) (X : T.Noninjective) (I : Ind) : ∑ Y : Ind, ↑(arrowMultiplicity T.toFiniteRightTauCategoryData (↑X) Y) * homDimensionMatrix T.toFiniteRightTauCategoryData k Y I = ∑ Y : Ind, ↑(arrowMultiplicity T.toFiniteRightTauCategoryData Y (T.tauMinus X)) * homDimensionMatrix T.toFiniteRightTauCategoryData k Y I

Every represented Hom column gives the same weighted sum for arrows out of X and arrows into its negative translate.

theorem MagnitudeConjecture.FiniteTauMatrix.arrowMultiplicity_eq_translation {k : Type s} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) [DecidablePred T.IsProjective] (D : HomMeshInverseData T) (leftEpi : ∀ (A : Ind), CategoryTheory.Epi (T.leftMesh (T.obj A)).g) (X : T.Noninjective) (Y : Ind) : arrowMultiplicity T.toFiniteRightTauCategoryData (↑X) Y = arrowMultiplicity T.toFiniteRightTauCategoryData Y (T.tauMinus X)

Arrow multiplicity is preserved by translation across a mesh: a(X,Y) = a(Y,tauMinus X) for every noninjective X.