Directed finite category surplus and zero-surplus thinness #
theorem
MagnitudeConjecture.CoveringHom.finiteCategorySurplus_nonnegative
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type}
[CategoryTheory.Category.{v, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
(H : HasAcyclicFiniteModuleNonzeroNonisomorphisms)
:
0 ≤ finiteCategorySurplus hP hrep
Directed primitive induction gives nonnegative intrinsic surplus.
theorem
MagnitudeConjecture.CoveringHom.finiteDeletionSurplus_nonnegative
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type}
[CategoryTheory.Category.{v, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
(H : HasAcyclicFiniteModuleNonzeroNonisomorphisms)
(S : Set C)
:
0 ≤ ObjectDeletion.finiteDeletionSurplus hP hrep S
Every finite deletion of a directed category has nonnegative surplus.
theorem
MagnitudeConjecture.CoveringHom.finiteDeletionSurplus_eq_zero
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type}
[CategoryTheory.Category.{v, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
(H : HasAcyclicFiniteModuleNonzeroNonisomorphisms)
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hskel : CategoryTheory.Skeletal C)
(hz : finiteCategorySurplus hP hrep = 0)
(S : Set C)
:
ObjectDeletion.finiteDeletionSurplus hP hrep S = 0
At zero surplus, all finite object deletions also have zero surplus.
theorem
MagnitudeConjecture.CoveringHom.finrank_obj_eq_one_of_finiteCategorySurplus_eq_zero
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type}
[CategoryTheory.Category.{v, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
(H : HasAcyclicFiniteModuleNonzeroNonisomorphisms)
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hskel : CategoryTheory.Skeletal C)
(hz : finiteCategorySurplus hP hrep = 0)
(M : FiniteDimensionalModuleCategory k)
(hM : CategoryTheory.Indecomposable M)
(x : C)
(hx : ¬CategoryTheory.Limits.IsZero (M.obj.obj.obj x))
:
Module.finrank k ↑(M.obj.obj.obj x) = 1
Zero surplus forces each nonzero fiber of an indecomposable to be a line.
theorem
MagnitudeConjecture.CoveringHom.finrank_obj_le_one_of_finiteCategorySurplus_eq_zero
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type}
[CategoryTheory.Category.{v, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
(H : HasAcyclicFiniteModuleNonzeroNonisomorphisms)
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hskel : CategoryTheory.Skeletal C)
(hz : finiteCategorySurplus hP hrep = 0)
(M : FiniteDimensionalModuleCategory k)
(hM : CategoryTheory.Indecomposable M)
(x : C)
:
Module.finrank k ↑(M.obj.obj.obj x) ≤ 1
Every indecomposable in a directed zero-surplus category is pointwise thin.