Matrices attached to a finite tau-category

This file turns the chosen finite skeleton and right tau-sequences in FiniteTauCategoryData into the concrete matrices used by the magnitude argument. The middle term of the right mesh ending at Y is decomposed into chosen indecomposables. Occurrences of X in that decomposition define the arrow multiplicity from X to Y.

For a Hom-finite linear category we also record the integer Hom-dimension matrix. The next layer will prove, from tau-sequence exactness and the one-dimensional residue division algebras, that the mesh and Hom matrices are mutual inverses.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.IsProjective {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 : FiniteRightTauCategoryData C Ind) (X : Ind) : Prop

Projective labels for right-tau data are those whose chosen right mesh has zero first term.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.Nonprojective {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 : FiniteRightTauCategoryData C Ind) : Type w

The finite subtype of nonprojective labels in right-tau data.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightMiddleArity {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.FiniteRightTauCategoryData C Ind) (Y : Ind) : ℕ

Number of indecomposable occurrences in the chosen decomposition of the middle term of the right mesh ending at Y.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightMiddleLabel {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.FiniteRightTauCategoryData C Ind) (Y : Ind) : Fin (rightMiddleArity T Y) → Ind

Labels in the chosen decomposition of the middle term of the right mesh ending at Y.

theorem MagnitudeConjecture.FiniteTauMatrix.rightMiddleIso {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.FiniteRightTauCategoryData C Ind) (Y : Ind) : Nonempty ((T.rightMesh (T.obj Y)).X₂ ≅ ⨁ fun (i : Fin (rightMiddleArity T Y)) => T.obj (rightMiddleLabel T Y i))

The chosen middle-term decomposition really represents the middle term of the right mesh.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.arrowMultiplicity {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.FiniteRightTauCategoryData C Ind) (source target : Ind) : ℕ

Arrow-occurrence multiplicity from source to target, read from the middle term of the right mesh ending at target.

theorem MagnitudeConjecture.FiniteTauMatrix.sum_arrowMultiplicity_source {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.FiniteRightTauCategoryData C Ind) (target : Ind) : ∑ source : Ind, arrowMultiplicity T source target = rightMiddleArity T target

Summing incoming arrow occurrences at a target recovers the number of indecomposable occurrences in its chosen right-mesh middle term.

theorem MagnitudeConjecture.FiniteTauMatrix.sum_arrowMultiplicity_mul {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.FiniteRightTauCategoryData C Ind) (target : Ind) (weight : Ind → ℕ) : ∑ source : Ind, arrowMultiplicity T source target * weight source = ∑ i : Fin (rightMiddleArity T target), weight (rightMiddleLabel T target i)

Regrouping a sum over middle-term occurrences by their indecomposable labels introduces the arrow multiplicities.

def MagnitudeConjecture.FiniteTauMatrix.tau {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] (U : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : U.Nonprojective) : Ind

Auslander--Reiten translation on nonprojective labels.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.meshMatrix {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] (U : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) [DecidableEq Ind] [DecidablePred U.IsProjective] : Matrix Ind Ind ℤ

The paper-oriented mesh matrix of the chosen finite tau-category.

theorem MagnitudeConjecture.FiniteTauMatrix.meshMatrix_apply_of_projective {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] (U : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) [DecidableEq Ind] [DecidablePred U.IsProjective] {source target : Ind} (hTarget : U.IsProjective target) : meshMatrix U source target = (if source = target then 1 else 0) - ↑(arrowMultiplicity U.toFiniteRightTauCategoryData source target)

theorem MagnitudeConjecture.FiniteTauMatrix.meshMatrix_apply_of_nonprojective {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] (U : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) [DecidableEq Ind] [DecidablePred U.IsProjective] {source target : Ind} (hTarget : ¬U.IsProjective target) : meshMatrix U source target = (if source = target then 1 else 0) - ↑(arrowMultiplicity U.toFiniteRightTauCategoryData source target) + if source = tau U ⟨target, hTarget⟩ then 1 else 0

noncomputable def MagnitudeConjecture.FiniteTauMatrix.homDimensionMatrix {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.FiniteRightTauCategoryData C Ind) (k : Type t) [Field k] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] : Matrix Ind Ind ℤ

Integer Hom-dimension matrix of a Hom-finite linear finite tau-category.

theorem MagnitudeConjecture.FiniteTauMatrix.homDimensionMatrix_nonnegative {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.FiniteRightTauCategoryData C Ind) (k : Type t) [Field k] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (X Y : Ind) : 0 ≤ homDimensionMatrix T k X Y

theorem MagnitudeConjecture.FiniteTauMatrix.finrank_hom_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] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) (k : Type t) [Field k] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (X Y : Ind) : Module.finrank k (T.obj X ⟶ (T.rightMesh (T.obj Y)).X₂) = ∑ i : Fin (rightMiddleArity T Y), Module.finrank k (T.obj X ⟶ T.obj (rightMiddleLabel T Y i))

Applying Hom(obj X,-) to the chosen middle-term decomposition gives the sum of the Hom dimensions of all arrow occurrences ending at Y.

theorem MagnitudeConjecture.FiniteTauMatrix.finrank_hom_rightMiddle_eq_arrowSum {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.FiniteRightTauCategoryData C Ind) (k : Type t) [Field k] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (X Y : Ind) : Module.finrank k (T.obj X ⟶ (T.rightMesh (T.obj Y)).X₂) = ∑ source : Ind, arrowMultiplicity T source Y * Module.finrank k (T.obj X ⟶ T.obj source)

The same middle-term formula regrouped by arrow multiplicity.