Intrinsic surplus of finite linear module categories #
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategorySurplus
{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), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
:
ℤ
The finite module-category surplus, with a complete skeleton constructed from local representation finiteness.
Instances For
theorem
MagnitudeConjecture.CoveringHom.finiteCategorySurplus_eq_skeleton
{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), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
(T : FiniteDimensionalModuleIndecomposableSkeleton)
:
Any complete indecomposable skeleton computes the intrinsic surplus.
theorem
MagnitudeConjecture.CoveringHom.finiteCategorySurplus_eq_of_equivalence
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
{D : Type u'}
[CategoryTheory.Category.{v, u'} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k D]
[Fintype D]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hQ : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
(hrepD : IsLocallyRepresentationFinite)
(E : C ≌ D)
[E.functor.Additive]
[CategoryTheory.Functor.Linear k E.functor]
:
finiteCategorySurplus hP hrep = finiteCategorySurplus hQ hrepD
A finite linear category equivalence preserves module-category surplus.