Pointwise-thin finite-dimensional modules

For modules on a basic finite or locally bounded linear category, multiplicity-freeness is expressed by having coefficient-field dimension at most one at every object. This is the form supplied by the universal-cover equality calculation.

def MagnitudeConjecture.CoveringHom.IsPointwiseThin {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Functor C (ModuleCat k)) : Prop

A linear module is pointwise thin when every value has dimension at most one over the coefficient field.

theorem MagnitudeConjecture.CoveringHom.isPointwiseThin_iff_finrank_eq_one_of_not_isZero {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : CategoryTheory.Functor C (ModuleCat k)) (hM : ∀ (X : C), FiniteDimensional k ↑(M.obj X)) : IsPointwiseThin M ↔ ∀ (X : C), ¬CategoryTheory.Limits.IsZero (M.obj X) → Module.finrank k ↑(M.obj X) = 1

For a pointwise finite module, pointwise thinness is equivalently the statement that every nonzero value has dimension one.

theorem MagnitudeConjecture.ObjectDeletion.isPointwiseThin_of_extensionByZero {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.LinearModuleCategory k) (hM : CoveringHom.IsPointwiseThin ((linearModuleExtensionByZero C S).obj M).obj) : CoveringHom.IsPointwiseThin M.obj

Pointwise thinness descends from an extension-by-zero module to the original module on the surviving category.