Indecomposability of string projective radical summands

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientFGHasBinaryBiproducts {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.HasBinaryBiproducts (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalSummand_indec {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) (i : Fin (Nat.card (DisplayedIncomingArrow y))) : CategoryTheory.Indecomposable (P.representedVertexRadicalSummand y i)