Primitive quotient surplus of literal object deletion

The singleton object-deletion category is equivalent to modules over the canonical primitive quotient of the finite category algebra. Pulling back the label-aligned quotient skeleton through this equivalence identifies its finite-tau surplus with the intrinsic quotient surplus used by directed deletion.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.primitiveQuotientSurplusAlgebraFiniteDimensional {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : FiniteDimensional k (algebra hP)

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.primitiveQuotientSurplusAlgebraOppositeIsNoetherian {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : IsNoetherianRing (algebra hP)ᵐᵒᵖ

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.deletionCategorySkeleton_surplus_eq_primitiveQuotientFinite_ambientARSurplus {k : Type u} [Field k] [IsAlgClosed k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hP)) (X : C) (T : FiniteDimensionalModuleIndecomposableSkeleton) : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective = (S.primitiveQuotientFiniteIndecomposableSkeleton ⋯).ambientARSurplus

The surplus of any complete skeleton of the literal singleton-deletion module category is the actual finite-tau surplus of the corresponding primitive quotient algebra. Unlike the intrinsic directed-deletion formula below, this comparison does not require the ambient module category to be directed.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.deletionCategorySkeleton_surplus_eq_primitiveQuotientARSurplus {k : Type u} [Field k] [IsAlgClosed k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hP)) (H : S.HasAcyclicNonzeroNonisomorphisms) (X : C) (T : FiniteDimensionalModuleIndecomposableSkeleton) : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective = S.primitiveQuotientARSurplus ⋯

The surplus of any complete skeleton of the literal singleton-deletion module category is the intrinsic primitive-quotient surplus of the matching canonical category-algebra projector.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.singletonDeletion_surplus_le {k : Type u} [Field k] [IsAlgClosed k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hskel : CategoryTheory.Skeletal C) (hrep : IsLocallyRepresentationFinite) (H : HasAcyclicFiniteModuleNonzeroNonisomorphisms) (X : C) (T : FiniteDimensionalModuleIndecomposableSkeleton) (Tdeleted : FiniteDimensionalModuleIndecomposableSkeleton) : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity Tdeleted.toFiniteRightTauCategoryData) Tdeleted.toFiniteRightTauCategoryData.IsProjective ≤ ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective

Literal singleton object deletion cannot increase finite-tau surplus in a finite representation-directed category. All algebra, skeleton, primitive presentation, coordinate, and boundary data are constructed internally.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finrank_obj_eq_one_of_singletonDeletion_surplus_eq {k : Type u} [Field k] [IsAlgClosed k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hskel : CategoryTheory.Skeletal C) (hrep : IsLocallyRepresentationFinite) (H : HasAcyclicFiniteModuleNonzeroNonisomorphisms) (X : C) (T : FiniteDimensionalModuleIndecomposableSkeleton) (Tdeleted : FiniteDimensionalModuleIndecomposableSkeleton) (hEquality : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity Tdeleted.toFiniteRightTauCategoryData) Tdeleted.toFiniteRightTauCategoryData.IsProjective = ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective) (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (hMX : ¬CategoryTheory.Limits.IsZero (M.obj.obj.obj X)) : Module.finrank k ↑(M.obj.obj.obj X) = 1

If singleton deletion preserves surplus, then every indecomposable module which is nonzero at the deleted object has one-dimensional fiber there. This is the literal category-module form of primitive-deletion equality rigidity.