Complete homogeneous idempotents of the graded projective generator

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

The opposite endomorphism projecting onto one summand of the generator.

theorem MagnitudeConjecture.GradedCategory.HomGrading.generatorIdempotent_idempotent {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι : Type} [Fintype ι] (P : ι → C) (p : ι) : generatorIdempotent P p * generatorIdempotent P p = generatorIdempotent P p

theorem MagnitudeConjecture.GradedCategory.HomGrading.generatorIdempotent_orthogonal {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι : Type} [Fintype ι] (P : ι → C) : Pairwise fun (p q : ι) => generatorIdempotent P p * generatorIdempotent P q = 0

theorem MagnitudeConjecture.GradedCategory.HomGrading.sum_generatorIdempotent {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) : ∑ p : ι, generatorIdempotent P p = 1

theorem MagnitudeConjecture.GradedCategory.HomGrading.generatorIdempotent_mem_zero {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)] (p : ι) : generatorIdempotent P p ∈ (generatorAlgebraGrading P G).component 0

Each summand projection is homogeneous of degree zero.

theorem MagnitudeConjecture.GradedCategory.HomGrading.generatorAlgebra_component_eq_bot {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 : ℤ) (hd : ∀ (i j : ι), G.component (P i) (P j) d = ⊥) : (generatorAlgebraGrading P G).component d = ⊥

A degree absent in every projective Hom space is absent in the generator algebra.