Intrinsic and finite-skeleton local density

A complete finite indecomposable skeleton implies local representation- finiteness. At each skeleton label, the intrinsic local density defined from an arbitrary minimal sink agrees with the finite right-tau density. Thus the manuscript's sum of intrinsic local densities is the existing finite Auslander--Reiten surplus.

theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.isLocallyRepresentationFinite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) : IsLocallyRepresentationFinite

A complete finite indecomposable skeleton supplies the manuscript's pointwise local representation-finiteness condition.

theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.finiteModuleLocalDensity_eq_rightTauLocalDensity {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (hlocal : IsLocallyRepresentationFinite) (i : Fin S.n) : finiteModuleLocalDensity hlocal (S.obj i) ⋯ = S.rightTauLocalDensity i

Intrinsic local density agrees labelwise with the local density of the complete finite right-tau skeleton.

theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.sum_finiteModuleLocalDensity_eq_surplus {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (hlocal : IsLocallyRepresentationFinite) : ∑ i : Fin S.n, finiteModuleLocalDensity hlocal (S.obj i) ⋯ = ARCount.surplus (FiniteTauMatrix.arrowMultiplicity S.toFiniteRightTauCategoryData) S.toFiniteRightTauCategoryData.IsProjective

Summing intrinsic local density over a complete finite skeleton recovers its Auslander--Reiten surplus.