Reindexing the incoming-arrow biproduct by a finite ordinal

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientFGHasFiniteBiproductsForReindex {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : CategoryTheory.Limits.HasFiniteBiproducts (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowBiproductReindexIso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (y : Q) : (⨁ fun (a : DisplayedIncomingArrow y) => P.incomingArrowRangeFGObj a) ≅ ⨁ P.representedVertexRadicalSummand y

Reindex the incoming-arrow categorical biproduct by its cardinality.