Grading actual morphisms from the projective sum

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.generatorHomEquiv {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type} [Fintype ι] (P : ι → C) [CategoryTheory.Limits.HasFiniteBiproducts C] (X : C) : (⨁ P ⟶ X) ≃ₗ[k] (i : ι) → P i ⟶ X

The finite biproduct universal property as a linear coordinate equivalence.

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.generatorMatrixEquiv {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type} [Fintype ι] (P : ι → C) [CategoryTheory.Limits.HasFiniteBiproducts C] : (⨁ P ⟶ ⨁ P) ≃ₗ[k] (i j : ι) → P i ⟶ P j

Endomorphisms of the finite sum in matrix coordinates.

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

The internal grading on actual maps from the projective sum.

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

The internal grading on actual endomorphisms of the projective sum.

theorem MagnitudeConjecture.GradedCategory.HomGrading.generatorHom_postcomp_mem {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type} [Fintype ι] (P : ι → C) [CategoryTheory.Limits.HasFiniteBiproducts C] (G : HomGrading k C) [∀ (i : ι) (X : C), FiniteDimensional k (P i ⟶ X)] {X Y : C} {n d : ℤ} {f : ⨁ P ⟶ X} {g : X ⟶ Y} (hf : f ∈ (generatorHomGrading P G X).component n) (hg : g ∈ G.component X Y d) : CategoryTheory.CategoryStruct.comp f g ∈ (generatorHomGrading P G Y).component (n + d)

Postcomposition respects the grading on the actual generator Hom space.

theorem MagnitudeConjecture.GradedCategory.HomGrading.generatorHom_precomp_mem {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type} [Fintype ι] (P : ι → C) [CategoryTheory.Limits.HasFiniteBiproducts C] (G : HomGrading k C) [∀ (i : ι) (X : C), FiniteDimensional k (P i ⟶ X)] {X : C} {d n : ℤ} {a : ⨁ P ⟶ ⨁ P} {f : ⨁ P ⟶ X} (ha : a ∈ (generatorEndGrading P G).component d) (hf : f ∈ (generatorHomGrading P G X).component n) : CategoryTheory.CategoryStruct.comp a f ∈ (generatorHomGrading P G X).component (d + n)

Precomposition respects the grading on actual generator Hom spaces.

theorem MagnitudeConjecture.GradedCategory.HomGrading.generatorEnd_comp_mem {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type} [Fintype ι] (P : ι → C) [CategoryTheory.Limits.HasFiniteBiproducts C] (G : HomGrading k C) [∀ (i : ι) (X : C), FiniteDimensional k (P i ⟶ X)] {d n : ℤ} {a b : ⨁ P ⟶ ⨁ P} (ha : a ∈ (generatorEndGrading P G).component d) (hb : b ∈ (generatorEndGrading P G).component n) : CategoryTheory.CategoryStruct.comp a b ∈ (generatorEndGrading P G).component (d + n)

Composition adds degrees in the actual generator endomorphism space.

theorem MagnitudeConjecture.GradedCategory.HomGrading.generatorEnd_id_mem {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type} [Fintype ι] (P : ι → C) [CategoryTheory.Limits.HasFiniteBiproducts C] (G : HomGrading k C) [∀ (i : ι) (X : C), FiniteDimensional k (P i ⟶ X)] : CategoryTheory.CategoryStruct.id (⨁ P) ∈ (generatorEndGrading P G).component 0

The generator identity is homogeneous of degree zero.