Magnitude conjecture

MagnitudeConjecture.CategoryTheory.Magnitude

Rational magnitude of a finite Hom-finite category #

For a finite chosen skeleton, the Leinster magnitude is the total sum of the inverse of the rational Hom-dimension matrix. The Hom--mesh inverse theorem identifies that inverse with the integral mesh matrix, proving the frozen manuscript's magnitude formula rather than merely its combinatorial analogue.

source
noncomputable def MagnitudeConjecture.FiniteTauMatrix.rationalHomDimensionMatrix {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) :
Matrix Ind Ind ℚ

Rational Hom-dimension matrix of the chosen finite skeleton.

Instances For
    source
    noncomputable def MagnitudeConjecture.FiniteTauMatrix.rationalMeshMatrix {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] :
    Matrix Ind Ind ℚ

    The integral mesh matrix, regarded over the rationals.

    Instances For
      source
      noncomputable def MagnitudeConjecture.FiniteTauMatrix.categoryMagnitude {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) :
      ℚ

      Leinster magnitude of the chosen finite Hom-dimension matrix.

      Instances For
        source
        theorem MagnitudeConjecture.FiniteTauMatrix.rationalHomDimensionMatrix_mul_rationalMeshMatrix {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) :
        rationalHomDimensionMatrix T * rationalMeshMatrix T = 1

        The integer inverse equation remains valid after passing to rational coefficients.

        source
        theorem MagnitudeConjecture.FiniteTauMatrix.rationalHomDimensionMatrix_inv_eq_rationalMeshMatrix {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) :
        (rationalHomDimensionMatrix T)⁻¹ = rationalMeshMatrix T

        Hence the nonsingular inverse of the rational Hom matrix is precisely the rationalized mesh matrix.

        source
        theorem MagnitudeConjecture.FiniteTauMatrix.categoryMagnitude_eq_eulerMagnitude {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) :
        categoryMagnitude T = ↑(ARCount.eulerMagnitude (arrowMultiplicity T.toFiniteRightTauCategoryData) T.IsProjective)

        Frozen manuscript, equations (2.1) and (2.3): categorical magnitude is the Auslander--Reiten Euler expression vertices - arrows + meshes.