Graded Hom coordinates from a finite projective family

The construction applies to any finite family; at the standard-form application the family consists of the indecomposable projectives.

def MagnitudeConjecture.GradedCategory.HomGrading.projectiveHomGrading {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) {ι : Type z} [Fintype ι] (P : ι → C) [∀ (i : ι) (X : C), FiniteDimensional k (P i ⟶ X)] (X : C) : Graded.VectorGrading k ((i : ι) → P i ⟶ X)

The homogeneous coordinates of Hom(⊕ᵢ Pᵢ, X).

def MagnitudeConjecture.GradedCategory.HomGrading.projectiveHomMap {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type z} (P : ι → C) {X Y : C} (f : X ⟶ Y) : ((i : ι) → P i ⟶ X) →ₗ[k] (i : ι) → P i ⟶ Y

Postcomposition on the Hom coordinates.

theorem MagnitudeConjecture.GradedCategory.HomGrading.projectiveHomMap_mem {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) {ι : Type z} [Fintype ι] (P : ι → C) [∀ (i : ι) (X : C), FiniteDimensional k (P i ⟶ X)] {X Y : C} {d n : ℤ} {f : X ⟶ Y} (hf : f ∈ G.component X Y d) {x : (i : ι) → P i ⟶ X} (hx : x ∈ (G.projectiveHomGrading P X).component n) : (projectiveHomMap P f) x ∈ (G.projectiveHomGrading P Y).component (n + d)

Homogeneous postcomposition has the same degree as the original morphism.

def MagnitudeConjecture.GradedCategory.HomGrading.projectiveMatrixGrading {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) {ι : Type z} [Fintype ι] (P : ι → C) [∀ (i : ι) (X : C), FiniteDimensional k (P i ⟶ X)] : Graded.VectorGrading k ((i j : ι) → P i ⟶ P j)

The homogeneous matrix coordinates of the endomorphisms of the projective sum.

theorem MagnitudeConjecture.GradedCategory.HomGrading.projectiveMatrixAction_mem {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) {ι : Type z} [Fintype ι] (P : ι → C) [∀ (i : ι) (X : C), FiniteDimensional k (P i ⟶ X)] {X : C} {d n : ℤ} {a : (i j : ι) → P i ⟶ P j} {x : (i : ι) → P i ⟶ X} (ha : a ∈ (G.projectiveMatrixGrading P).component d) (hx : x ∈ (G.projectiveHomGrading P X).component n) : (fun (i : ι) => ∑ j : ι, CategoryTheory.CategoryStruct.comp (a i j) (x j)) ∈ (G.projectiveHomGrading P X).component (d + n)

Precomposition by a homogeneous matrix shifts the degree of Hom coordinates. This is the right module action used in the manuscript.