The graded right modules represented by the projective generator

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

Coordinates for the opposite endomorphism ring acting by precomposition.

instance MagnitudeConjecture.GradedCategory.HomGrading.generatorScalarTower {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι : Type} [Fintype ι] (P : ι → C) (X : C) : IsScalarTower k (CategoryTheory.End (⨁ P))ᵐᵒᵖ (⨁ P ⟶ X)

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

The internal grading on the opposite generator algebra.

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

The actual Hom module, graded compatibly with the right algebra action.

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

Multiplication in the opposite algebra adds degrees.

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

The algebra unit has degree zero.

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

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.generatorModuleMap {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι : Type} [Fintype ι] (P : ι → C) {X Y : C} (f : X ⟶ Y) : (⨁ P ⟶ X) →ₗ[(CategoryTheory.End (⨁ P))ᵐᵒᵖ] ⨁ P ⟶ Y

Postcomposition is a map of the actual right modules.

theorem MagnitudeConjecture.GradedCategory.HomGrading.generatorModuleMap_homogeneous {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι : Type} [Fintype ι] (P : ι → C) (G : HomGrading k C) [∀ (i : ι) (X : C), FiniteDimensional k (P i ⟶ X)] {X Y : C} {d : ℤ} {f : X ⟶ Y} (hf : f ∈ G.component X Y d) : (generatorModuleGrading P G X).Homogeneous (generatorModuleGrading P G Y) d (generatorModuleMap P f)

The represented module map has the degree of its original morphism.