Local density from a minimal right almost-split source

The manuscript's local density at an indecomposable is twice its nonprojective indicator minus the total number of incoming arrow occurrences. In a finite tau-category, the second term is the arity of the chosen right-mesh middle object. This file records the exact numerical bridge in a form that can also use any other minimal right almost-split source decomposition.

noncomputable def MagnitudeConjecture.ARCount.localDensityOfIncomingArity (incomingArity : ℕ) (IsProjective : Prop) : ℤ

Local density written using a supplied total incoming arity.

theorem MagnitudeConjecture.FiniteTauMatrix.rightTau_first_isZero_iff_mono_terminal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence S) : CategoryTheory.Limits.IsZero S.X₁ ↔ CategoryTheory.Mono S.g

The first term of a right tau-sequence is zero exactly when its terminal map is monic.

theorem MagnitudeConjecture.FiniteTauMatrix.isProjective_iff_projective_obj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Limits.HasFiniteBiproducts A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.IsIdempotentComplete A] {J : Type w} [Fintype J] (U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData A J) [CategoryTheory.EnoughProjectives A] (Y : J) : U.IsProjective Y ↔ CategoryTheory.Projective (U.obj Y)

In an abelian category with enough projectives, the finite tau predicate defined by a zero left mesh term is exactly categorical projectivity of the chosen indecomposable.

theorem MagnitudeConjecture.FiniteTauMatrix.localDensity_eq_localDensityOfIncomingArity {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) (incomingArity : ℕ) (hArity : rightMiddleArity T Y = incomingArity) (IsProjective : Prop) (hProjective : T.IsProjective Y ↔ IsProjective) : ARCount.localDensity (arrowMultiplicity T) T.IsProjective Y = ARCount.localDensityOfIncomingArity incomingArity IsProjective

The matrix local density is determined by the right-middle arity and the projective predicate at the chosen label.

theorem MagnitudeConjecture.FiniteTauMatrix.localDensity_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) [DecidablePred T.IsProjective] (Y : Ind) {E : C} {f : E ⟶ T.obj Y} (d : CategoryTheory.FiniteIndecomposableDecomposition E) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) (IsProjective : Prop) (hProjective : T.IsProjective Y ↔ IsProjective) : ARCount.localDensity (arrowMultiplicity T) T.IsProjective Y = ARCount.localDensityOfIncomingArity d.n IsProjective

Equivalently, every finite decomposition of a minimal right almost-split source computes the local density at its endpoint.