Homogeneous corners of a projective-generator algebra

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.generatorCornerEquiv {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)] (i j : ι) (d : ℤ) : ↥(Graded.cornerComponent (generatorAlgebraGrading P G) (generatorIdempotent P i) (generatorIdempotent P j) d) ≃ₗ[k] ↥(G.component (P i) (P j) d)

A corner of the opposite generator algebra is the corresponding Hom space between summands, with the same homogeneous degree.