Hom-dimension weights and the two unit equations

Once the Hom-dimension matrix and the mesh matrix are inverse, a row represented by a label P satisfies the paper's column equation Phi^T d = e_P, while a column represented by I satisfies Phi d = e_I. Nonzero maps from P, or to I, make the corresponding integral weights strictly positive.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.homFromWeight {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] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (P : Ind) : Ind → ℤ

The integer Hom-dimension row represented by P.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.homToWeight {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] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (I : Ind) : Ind → ℤ

The integer Hom-dimension column represented by I.

theorem MagnitudeConjecture.FiniteTauMatrix.additiveObjectWeight_homFromWeight {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] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (P : Ind) (X : C) : (T.additiveObjectWeightOfLabelWeight (homFromWeight T P)).weight X = ↑(Module.finrank k (T.obj P ⟶ X))

The additive extension of a represented Hom row evaluates every object by the dimension of its Hom space from the representing object.

theorem MagnitudeConjecture.FiniteTauMatrix.additiveObjectWeight_homToWeight {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] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (I : Ind) (X : C) : (T.additiveObjectWeightOfLabelWeight (homToWeight T I)).weight X = ↑(Module.finrank k (X ⟶ T.obj I))

The additive extension of a represented Hom column evaluates every object by the dimension of its Hom space to the representing object.

theorem MagnitudeConjecture.FiniteTauMatrix.additiveObjectWeight_eq_zero_iff_isZero {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] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (weight : Ind → ℤ) (hpos : ∀ (i : Ind), 0 < weight i) (X : C) : (T.additiveObjectWeightOfLabelWeight weight).weight X = 0 ↔ CategoryTheory.Limits.IsZero X

A strictly positive label weight has zero additive extension exactly on zero objects.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.leftMeshLabelWeightDefect {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] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (weight : Ind → ℤ) (source : Ind) : ℤ

The Euler defect of a label weight on the chosen left mesh.

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

Weighted row sum of the paper-oriented mesh matrix.

theorem MagnitudeConjecture.FiniteTauMatrix.meshColumnWeight_homFromWeight {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) (P target : Ind) : meshColumnWeight T (homFromWeight T P) target = if target = P then 1 else 0

The row of Hom dimensions represented by P satisfies the manuscript's unit-column equation Phi^T d = e_P.

theorem MagnitudeConjecture.FiniteTauMatrix.meshRowWeight_homToWeight {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) (I source : Ind) : meshRowWeight T (homToWeight T I) source = if source = I then 1 else 0

The column of Hom dimensions represented by I satisfies the manuscript's unit-row equation Phi d = e_I.

theorem MagnitudeConjecture.FiniteTauMatrix.leftMeshLabelWeightDefect_homToWeight {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) (D : HomMeshInverseData T) (leftEpi : ∀ (A : Ind), CategoryTheory.Epi (T.leftMesh (T.obj A)).g) (I A : Ind) : leftMeshLabelWeightDefect T (homToWeight T I) A = if A = I then 1 else 0

The categorical left-mesh defect of a represented Hom column is the Kronecker delta at its representing label. This is the literal opposite unit equation used at Iyama's injective boundary.

theorem MagnitudeConjecture.FiniteTauMatrix.meshUnitEquations_of_homDimensionIdentities {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) (P I : Ind) (weight : Ind → ℤ) (weight_eq_from : ∀ (X : Ind), weight X = homFromWeight T P X) (weight_eq_to : ∀ (X : Ind), weight X = homToWeight T I X) : (∀ (target : Ind), meshColumnWeight T weight target = if target = P then 1 else 0) ∧ ∀ (source : Ind), meshRowWeight T weight source = if source = I then 1 else 0

A single weight identified with both the source Hom row and the sink Hom column satisfies the two unit equations in Proposition factor-structure of the frozen manuscript.

theorem MagnitudeConjecture.FiniteTauMatrix.homFromWeight_pos {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] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (P : Ind) (reachable : ∀ (X : Ind), ∃ (f : T.obj P ⟶ T.obj X), f ≠ 0) (X : Ind) : 0 < homFromWeight T P X

Nonzero maps from P to every chosen indecomposable make its Hom row a strictly positive integral weight.

theorem MagnitudeConjecture.FiniteTauMatrix.homToWeight_pos {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] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (I : Ind) (coreachable : ∀ (X : Ind), ∃ (f : T.obj X ⟶ T.obj I), f ≠ 0) (X : Ind) : 0 < homToWeight T I X

Nonzero maps from every chosen indecomposable to I make its Hom column a strictly positive integral weight.