The mesh matrix is the inverse Hom matrix

This file proves Iyama's finite radical-layer recurrence in matrix form. Its inputs are a finite tau-category, strictness of every chosen right tau- sequence, Hom-finiteness, and the residue-dimension formula

dim rad(X,Y) + delta(X,Y) = dim Hom(X,Y).

The first two categorical inputs turn each right tau-sequence into a short exact sequence on Hom spaces. The chosen middle-term decomposition supplies the arrow multiplicities. Column by column, the resulting recurrence is exactly H * K = 1; finite square matrices over ℤ are Dedekind finite, so also K * H = 1.

structure MagnitudeConjecture.FiniteTauMatrix.HomMeshInverseData {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] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) : Prop

The two additional properties needed to pass from finite tau-category data to the integer Hom/mesh inverse relation.

For module categories over an algebraically closed field, rightMono comes from strictness of almost-split sequences and radicalFinrank_add_delta from the fact that every indecomposable has residue division algebra k.

• rightMono (Y : Ind) : CategoryTheory.Mono (T.rightMesh (T.obj Y)).f
• radicalFinrank_add_delta (X Y : Ind) : (Module.finrank k ↥(CategoryTheory.radicalSubmodule k (T.obj X) (T.obj Y)) + if X = Y then 1 else 0) = Module.finrank k (T.obj X ⟶ T.obj Y)

theorem MagnitudeConjecture.FiniteTauMatrix.finrank_hom_rightMesh_left_of_projective {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) (X Y : Ind) (hY : T.IsProjective Y) : Module.finrank k (T.obj X ⟶ (T.rightMesh (T.obj Y)).X₁) = 0

theorem MagnitudeConjecture.FiniteTauMatrix.finrank_hom_rightMesh_left_of_nonprojective {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] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (X Y : Ind) (hY : ¬T.IsProjective Y) : Module.finrank k (T.obj X ⟶ (T.rightMesh (T.obj Y)).X₁) = Module.finrank k (T.obj X ⟶ T.obj (tau T ⟨Y, hY⟩))

theorem MagnitudeConjecture.FiniteTauMatrix.projective_column_recurrence {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) (X Y : Ind) (hY : T.IsProjective Y) : homDimensionMatrix T.toFiniteRightTauCategoryData k X Y - ∑ source : Ind, ↑(arrowMultiplicity T.toFiniteRightTauCategoryData source Y) * homDimensionMatrix T.toFiniteRightTauCategoryData k X source = if X = Y then 1 else 0

theorem MagnitudeConjecture.FiniteTauMatrix.nonprojective_column_recurrence {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) (X Y : Ind) (hY : ¬T.IsProjective Y) : homDimensionMatrix T.toFiniteRightTauCategoryData k X Y - ∑ source : Ind, ↑(arrowMultiplicity T.toFiniteRightTauCategoryData source Y) * homDimensionMatrix T.toFiniteRightTauCategoryData k X source + homDimensionMatrix T.toFiniteRightTauCategoryData k X (tau T ⟨Y, hY⟩) = if X = Y then 1 else 0

theorem MagnitudeConjecture.FiniteTauMatrix.homDimensionMatrix_mul_meshMatrix {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) [DecidablePred T.IsProjective] : homDimensionMatrix T.toFiniteRightTauCategoryData k * meshMatrix T = 1

The radical-layer recurrence is the right-inverse equation H * K = 1.

theorem MagnitudeConjecture.FiniteTauMatrix.meshMatrix_mul_homDimensionMatrix {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) [DecidablePred T.IsProjective] : meshMatrix T * homDimensionMatrix T.toFiniteRightTauCategoryData k = 1

Hence the mesh matrix is also a left inverse of the Hom-dimension matrix.

theorem MagnitudeConjecture.FiniteTauMatrix.homMesh_inverse_and_total {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) [DecidablePred T.IsProjective] : homDimensionMatrix T.toFiniteRightTauCategoryData k * meshMatrix T = 1 ∧ meshMatrix T * homDimensionMatrix T.toFiniteRightTauCategoryData k = 1 ∧ ARCount.matrixTotal (meshMatrix T) = ARCount.eulerMagnitude (arrowMultiplicity T.toFiniteRightTauCategoryData) T.IsProjective

Complete matrix form of the magnitude formula for a finite strict tau- category satisfying the residue-dimension condition.