Biproduct decompositions with homogeneous degree-zero structure maps

def MagnitudeConjecture.GradedCategory.HomGrading.shiftedBicone {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} {V : ι → C} (b : CategoryTheory.Limits.Bicone V) (hπ : ∀ (i : ι), b.π i ∈ G.component b.pt (V i) 0) (hι : ∀ (i : ι), b.ι i ∈ G.component (V i) b.pt 0) (t : ℤ) : CategoryTheory.Limits.Bicone fun (i : ι) => { obj := V i, degree := t }

A degree-zero direct-sum diagram lifts with any common external shift.

def MagnitudeConjecture.GradedCategory.HomGrading.shiftedBiconeIsBilimit {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 ι] {V : ι → C} (b : CategoryTheory.Limits.Bicone V) (hπ : ∀ (i : ι), b.π i ∈ G.component b.pt (V i) 0) (hι : ∀ (i : ι), b.ι i ∈ G.component (V i) b.pt 0) (t : ℤ) (htotal : ∑ i : ι, CategoryTheory.CategoryStruct.comp (b.π i) (b.ι i) = CategoryTheory.CategoryStruct.id b.pt) : (G.shiftedBicone b hπ hι t).IsBilimit

The lifted diagram is still a biproduct: its total identity is unchanged.