Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteTauOccurrences

Arrow occurrences of a finite tau-category #

The displayed summands of all chosen right-mesh middle terms form a literal finite type of arrow occurrences. Its target fibre at a label is the finite index type of that middle-term decomposition, so occurrence counting gives exactly the finite-tau multiplicity matrix and local density.

source
@[reducible, inline]
abbrev MagnitudeConjecture.FiniteTauMatrix.RightArrowOccurrence {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) :
Type w

A right-arrow occurrence is a displayed indecomposable summand of the chosen right-mesh middle term at its target label.

Instances For
    source
    noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightArrowSource {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) (a : RightArrowOccurrence T) :
    Ind

    Source label of a displayed right-arrow occurrence.

    Instances For
      source
      def MagnitudeConjecture.FiniteTauMatrix.rightArrowTarget {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) (a : RightArrowOccurrence T) :
      Ind

      Target label of a displayed right-arrow occurrence.

      Instances For
        source
        noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightArrowTargetFiberEquiv {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) :
        { a : RightArrowOccurrence T // rightArrowTarget T a = Y } ≃ Fin (rightMiddleArity T Y)

        The occurrences ending at Y are exactly the displayed summands of its right-mesh middle term.

        Instances For
          source
          def MagnitudeConjecture.FiniteTauMatrix.rightArrowSourceTargetFiberEquiv {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) (X Y : Ind) :
          { a : RightArrowOccurrence T // rightArrowSource T a = X ∧ rightArrowTarget T a = Y } ≃ { i : Fin (rightMiddleArity T Y) // rightMiddleLabel T Y i = X }

          Fixing both source and target leaves precisely the displayed middle indices carrying that source label.

          Instances For
            source
            theorem MagnitudeConjecture.FiniteTauMatrix.arrowMultiplicityOfOccurrences_eq {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) (X Y : Ind) :
            CoveringAction.arrowMultiplicityOfOccurrences (rightArrowSource T) (rightArrowTarget T) X Y = arrowMultiplicity T X Y

            Counting canonical occurrences with fixed endpoints recovers the finite-tau arrow multiplicity entry.

            source
            theorem MagnitudeConjecture.FiniteTauMatrix.occurrenceIndegree_rightArrowTarget_eq {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) :
            CoveringAction.occurrenceIndegree (rightArrowTarget T) Y = ↑(rightMiddleArity T Y)

            The occurrence indegree is the literal right-middle arity.

            source
            theorem MagnitudeConjecture.FiniteTauMatrix.occurrenceLocalDensity_rightArrowTarget_eq {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) [DecidablePred T.IsProjective] (Y : Ind) :
            CoveringAction.occurrenceLocalDensity (rightArrowTarget T) T.IsProjective Y = ARCount.localDensityOfIncomingArity (rightMiddleArity T Y) (T.IsProjective Y)

            The occurrence form of local density for the canonical right-arrow type is the incoming-arity form.

            source
            theorem MagnitudeConjecture.FiniteTauMatrix.localDensity_eq_occurrenceLocalDensity {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) [DecidablePred T.IsProjective] (Y : Ind) :
            ARCount.localDensity (arrowMultiplicity T) T.IsProjective Y = CoveringAction.occurrenceLocalDensity (rightArrowTarget T) T.IsProjective Y

            The finite-tau multiplicity-matrix local density is exactly the local density of its canonical right-arrow occurrence type.