Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteTauAlmostSplitMultiplicity

Incoming multiplicity in a finite tau-category #

The terminal map of a chosen right tau-sequence is a minimal right almost-split map after identifying its endpoint with the chosen indecomposable representative. Hence the number of occurrences in the chosen right-mesh middle term is the size of every finite indecomposable decomposition of every minimal right almost-split source at that endpoint.

source
noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightMiddleFiniteIndecomposableDecomposition {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) :
CategoryTheory.FiniteIndecomposableDecomposition (T.rightMesh (T.obj Y)).X₂

The chosen right-mesh middle term as a displayed finite indecomposable decomposition.

Instances For
    source
    theorem MagnitudeConjecture.FiniteTauMatrix.rightMesh_terminal_isRightAlmostSplit {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) :
    QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.CategoryStruct.comp (T.rightMesh (T.obj Y)).g (T.rightTermIso (T.obj Y)).hom)

    After the chosen endpoint identification, the terminal map of a right tau-sequence is right almost split.

    source
    theorem MagnitudeConjecture.FiniteTauMatrix.rightMesh_terminal_isRightMinimal {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) :
    QuotientSubmoduleEquidistribution.IsRightMinimal (CategoryTheory.CategoryStruct.comp (T.rightMesh (T.obj Y)).g (T.rightTermIso (T.obj Y)).hom)

    The chosen right-mesh terminal map is right minimal after the endpoint identification.

    source
    theorem MagnitudeConjecture.FiniteTauMatrix.rightMiddleArity_eq_of_minimalRightAlmostSplitDecomposition {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) {E : C} {f : E ⟶ T.obj Y} (d : CategoryTheory.FiniteIndecomposableDecomposition E) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) :
    rightMiddleArity T Y = d.n

    The total incoming-arrow multiplicity at Y, represented by rightMiddleArity, is the number of indecomposable occurrences in every minimal right almost-split source ending at T.obj Y.