Magnitude conjecture

QuotientSubmoduleEquidistribution.CategoryTheory.LinearMat

Linear structure on finite matrix categories #

source
@[instance_reducible]
instance QuotientSubmoduleEquidistribution.CategoryTheory.matLinear {K : Type w} [Semiring K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear K C] :
CategoryTheory.Linear K (CategoryTheory.Mat_ C)

The pointwise linear structure on the finite matrix category.

source
instance QuotientSubmoduleEquidistribution.CategoryTheory.matHomModuleFinite {K : Type w} [DivisionRing K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear K C] [∀ (X Y : C), Module.Finite K (X ⟶ Y)] (M N : CategoryTheory.Mat_ C) :
Module.Finite K (M ⟶ N)

Finite matrices of finite-dimensional Hom spaces remain finite-dimensional.