Extending the mesh Hom grading to finite direct sums

The original grading is supplied only on the indecomposable category. Its additive envelope supplies the finite biproducts needed for the generator.

@[instance_reducible]

instance MagnitudeConjecture.GradedCategory.matHomModule {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : CategoryTheory.Mat_ C) : Module k (X ⟶ Y)

@[instance_reducible]

instance MagnitudeConjecture.GradedCategory.matLinear {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Linear k (CategoryTheory.Mat_ C)

instance MagnitudeConjecture.GradedCategory.matFiniteHom {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (X Y : CategoryTheory.Mat_ C) : FiniteDimensional k (X ⟶ Y)

def MagnitudeConjecture.GradedCategory.HomGrading.additiveEnvelope {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] : HomGrading k (CategoryTheory.Mat_ C)

Extend a Hom grading componentwise to the additive envelope.