Surplus under finite object deletion #
noncomputable def
MagnitudeConjecture.ObjectDeletion.finiteDeletionSurplus
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X))
(hrep : CoveringHom.IsLocallyRepresentationFinite)
(S : Set C)
:
ℤ
Surplus of the literal finite module category after object deletion.
Instances For
theorem
MagnitudeConjecture.ObjectDeletion.finiteDeletionSurplus_empty
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X))
(hrep : CoveringHom.IsLocallyRepresentationFinite)
:
finiteDeletionSurplus hP hrep ∅ = CoveringHom.finiteCategorySurplus hP hrep
Empty deletion preserves the intrinsic surplus.
theorem
MagnitudeConjecture.ObjectDeletion.finiteDeletionSurplus_iterated
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X))
(hrep : CoveringHom.IsLocallyRepresentationFinite)
(S T : Set C)
:
finiteDeletionSurplus ⋯ ⋯ (AdditionalDeleted C S T) = finiteDeletionSurplus hP hrep (S ∪ T)
Successive deletion has the surplus of deletion by the union.
theorem
MagnitudeConjecture.ObjectDeletion.finiteDeletionSurplus_singleton_le
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X))
(hrep : CoveringHom.IsLocallyRepresentationFinite)
[IsAlgClosed k]
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hskel : CategoryTheory.Skeletal C)
(H : CoveringHom.HasAcyclicFiniteModuleNonzeroNonisomorphisms)
(x : C)
:
finiteDeletionSurplus hP hrep {x} ≤ CoveringHom.finiteCategorySurplus hP hrep
Directed singleton deletion cannot increase intrinsic surplus.
theorem
MagnitudeConjecture.ObjectDeletion.finiteDeletionSurplus_le
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X))
(hrep : CoveringHom.IsLocallyRepresentationFinite)
[IsAlgClosed k]
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hskel : CategoryTheory.Skeletal C)
(H : CoveringHom.HasAcyclicFiniteModuleNonzeroNonisomorphisms)
(S : Set C)
:
finiteDeletionSurplus hP hrep S ≤ CoveringHom.finiteCategorySurplus hP hrep
Deleting any set of objects from a finite directed category cannot increase the module-category surplus.