Official module-category surplus and numerical count estimates #

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_eq_counts {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :

The official ambient surplus uses the literal indecomposable and simple counts and the official arrow multiplicities.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_error_of_counts {k A B : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (T : FiniteIndecomposableSkeleton k B) (m : ℕ) (W C : ℤ) (hN : ↑T.n = ↑S.n * (↑m + 1) - W) (ha : |ARCount.arrowCount (FiniteTauMatrix.arrowMultiplicity T.finiteTauCategoryData.toFiniteRightTauCategoryData) - (↑m + 1) * ARCount.arrowCount (FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData)| ≤ C) (hp : T.simpleCount = S.simpleCount * (m + 1)) :

|T.ambientARSurplus - (↑m + 1) * S.ambientARSurplus| ≤ 2 * |W| + C

Exact indecomposable and simple counts and an arrow bound control the official surplus of a second finite module skeleton.

Magnitude conjecture