Mesh-matrix evaluation of additive label weights

The categorical Euler defect of a label weight on a chosen right mesh is the corresponding weighted column sum of the mesh matrix. This identifies the matrix unit equations in the frozen manuscript with Iyama's positive right-additivity hypothesis.

theorem MagnitudeConjecture.FiniteTauMatrix.sum_arrowMultiplicity_mul_int {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) (target : Ind) (weight : Ind → ℤ) : ∑ source : Ind, ↑(arrowMultiplicity T.toFiniteRightTauCategoryData source target) * weight source = ∑ i : Fin (rightMiddleArity T.toFiniteRightTauCategoryData target), weight (rightMiddleLabel T.toFiniteRightTauCategoryData target i)

Regrouping an integral weight over middle-term occurrences by label.

theorem MagnitudeConjecture.FiniteTauMatrix.additiveLabelWeight_rightMiddle {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 → ℤ) (target : Ind) : (T.additiveObjectWeightOfLabelWeight weight).weight (T.rightMesh (T.obj target)).X₂ = ∑ source : Ind, ↑(arrowMultiplicity T.toFiniteRightTauCategoryData source target) * weight source

The additive extension of a label weight evaluates the chosen right middle term by the arrow-occurrence sum.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.meshColumnWeight {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 → ℤ) (target : Ind) : ℤ

Weighted column sum of the paper-oriented mesh matrix.

theorem MagnitudeConjecture.FiniteTauMatrix.rightMeshLabelWeightDefect_eq_meshColumnWeight {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 → ℤ) (target : Ind) : rightMeshLabelWeightDefect T weight target = meshColumnWeight T weight target

The categorical right-mesh Euler defect equals the weighted mesh-matrix column sum.

theorem MagnitudeConjecture.FiniteTauMatrix.isPositiveRightAdditiveLabelWeight_of_meshColumnWeight {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 → ℤ) (weight_pos : ∀ (x : Ind), 0 < weight x) (column_nonnegative : ∀ (x : Ind), 0 ≤ meshColumnWeight T weight x) (column_eq_zero_of_nonprojective : ∀ (x : Ind), ¬T.IsProjective x → meshColumnWeight T weight x = 0) : IsPositiveRightAdditiveLabelWeight T weight

Matrix-column nonnegativity and off-projective vanishing are exactly the Euler clauses of a positive right-additive label weight.

theorem MagnitudeConjecture.FiniteTauMatrix.isPositiveRightAdditiveLabelWeight_of_meshColumnUnit {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] (P : Ind) (hP : T.IsProjective P) (weight : Ind → ℤ) (weight_pos : ∀ (x : Ind), 0 < weight x) (unitEquation : ∀ (x : Ind), meshColumnWeight T weight x = if x = P then 1 else 0) : IsPositiveRightAdditiveLabelWeight T weight

A positive integral solution of the manuscript's unit-column equation is automatically a positive right-additive label weight.

theorem MagnitudeConjecture.FiniteTauMatrix.HomMeshInverseData.ofMeshColumnUnit {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) {k : Type s} [Field k] [IsAlgClosed k] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] [DecidablePred T.IsProjective] (P : Ind) (hP : T.IsProjective P) (weight : Ind → ℤ) (weight_pos : ∀ (x : Ind), 0 < weight x) (unitEquation : ∀ (x : Ind), meshColumnWeight T weight x = if x = P then 1 else 0) : HomMeshInverseData T

Over an algebraically closed field, a positive solution of the unit-column equation supplies the full Hom--mesh inverse package.