Magnitude and the ambient Auslander--Reiten surplus

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.categoryMagnitude_eq_projectiveCount_iff_ambientARSurplus_eq_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FiniteTauMatrix.categoryMagnitude S.finiteTauCategoryData = ↑(ARCount.projectiveCount fun (x : Fin S.n) => CategoryTheory.Projective (S.fgObj x)) ↔ S.ambientARSurplus = 0

Equality between categorical magnitude and the projective count is equivalent to vanishing of the ambient Auslander--Reiten surplus.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.categoryMagnitude_ge_projectiveCount {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ↑(ARCount.projectiveCount fun (x : Fin S.n) => CategoryTheory.Projective (S.fgObj x)) ≤ FiniteTauMatrix.categoryMagnitude S.finiteTauCategoryData

The magnitude lower bound follows from nonnegative interval surplus. The projective count equals the number of simple modules.