Indecomposable decomposition of string projective radicals

The radical of a represented canonical projective is the internal direct sum of the represented ranges of the displayed arrows ending at its vertex. Each such range is uniserial and nonzero, hence indecomposable. This file packages that literal path decomposition in the finite categorical format used by almost-split multiplicity arguments.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientFGHasFiniteBiproductsForDecomposition {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ᵐᵒᵖ)

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientFGHasBinaryBiproductsForDecomposition {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ᵐᵒᵖ)

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalDecomposition {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) : CategoryTheory.FiniteIndecomposableDecomposition (P.representedVertexRadicalFGObj y)

The radical of the represented projective at y, decomposed into one indecomposable uniserial summand for every displayed arrow ending at y.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalDecomposition_n {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) : (P.representedVertexRadicalDecomposition y).n = Nat.card (DisplayedIncomingArrow y)

The displayed radical decomposition has exactly as many summands as there are displayed arrows ending at the vertex.