The magnitude theorem through graded intervals

The inequality follows from nonnegative directed interval surplus and its uniform comparison with ambient surplus. At equality, separated interval packing and thinness make the control interval special biserial. The actual graded incoming maps transfer its beta bound to the original algebra. The converse uses the proved socle reduction to a string algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_eq_zero_iff_isSpecialBiserial {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (P : S.PrimitiveProjectivePresentation) : S.ambientARSurplus = 0 ↔ BoundQuiver.IsSpecialBiserial k A

Zero surplus is equivalent to special biseriality for a displayed primitive-projective presentation.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_eq_zero_iff_isSpecialBiserial_withoutPresentation {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.ambientARSurplus = 0 ↔ BoundQuiver.IsSpecialBiserial k A

The equality characterization for an arbitrary finite-dimensional algebra, using its basic Morita representative for the converse.

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.categoryMagnitude_eq_projectiveCount_iff_isSpecialBiserial_withoutPresentation {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)) ↔ BoundQuiver.IsSpecialBiserial k A

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.magnitudeConjecture_of_finiteIndecomposableSkeleton {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 ∧ (FiniteTauMatrix.categoryMagnitude S.finiteTauCategoryData = ↑(ARCount.projectiveCount fun (x : Fin S.n) => CategoryTheory.Projective (S.fgObj x)) ↔ BoundQuiver.IsSpecialBiserial k A)

noncomputable def MagnitudeConjecture.RightModule.representationFiniteSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] (hA : IsRepresentationFinite k A) : FiniteIndecomposableSkeleton k A

noncomputable def MagnitudeConjecture.RightModule.moduleCategoryMagnitude {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : ℚ

noncomputable def MagnitudeConjecture.RightModule.numberOfSimpleModules {k A : Type u} [Field k] [Ring A] [Algebra k A] (hA : IsRepresentationFinite k A) : ℤ

theorem MagnitudeConjecture.RightModule.magnitudeConjecture {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : ↑(numberOfSimpleModules hA) ≤ moduleCategoryMagnitude hA ∧ (moduleCategoryMagnitude hA = ↑(numberOfSimpleModules hA) ↔ BoundQuiver.IsSpecialBiserial k A)