Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteDimensionalModuleHomFinite

Hom-finiteness of finite-support module categories #

A natural transformation out of a finite-support pointwise finite-dimensional linear module is determined by its components on that finite support. Evaluation therefore embeds every Hom space between finite modules into a finite product of finite-dimensional linear-map spaces.

source
def MagnitudeConjecture.CoveringHom.finiteDimensionalModuleHomEvaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M N : FiniteDimensionalModuleCategory k) :
(M ⟶ N) →ₗ[k] (X : ↑(moduleSupport k M.obj.obj)) → ↑(M.obj.obj.obj ↑X) →ₗ[k] ↑(N.obj.obj.obj ↑X)

Evaluate a morphism on the finite support of its source.

Instances For
    source
    theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModuleHomEvaluation_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M N : FiniteDimensionalModuleCategory k) :
    Function.Injective ⇑(finiteDimensionalModuleHomEvaluation k M N)

    Evaluation on source support detects a natural transformation.

    source
    instance MagnitudeConjecture.CoveringHom.finiteDimensionalModuleHom_finiteDimensional {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M N : FiniteDimensionalModuleCategory k) :
    FiniteDimensional k (M ⟶ N)

    Hom spaces between finite-support pointwise finite-dimensional modules are finite-dimensional.