Module objects underlying string projective radical decompositions

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowLinearRange_nontrivial {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) {x y : Q} (a : x ⟶ y) : Nontrivial ↥(P.representedArrowLinearMap a).range

A represented string-arrow range is nonzero: the trivial path before the arrow is one of its continuation-basis indices.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeFGObj {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} (a : DisplayedIncomingArrow y) : FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ

The finitely generated module carried by one represented incoming-arrow range.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalFGObj {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) : FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ

The module Jacobson radical of a represented canonical projective, retained as a finitely generated module.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeFamilyRadicalLinearEquiv {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) : ((a : DisplayedIncomingArrow y) → ↥(P.representedArrowLinearMap a.snd).range) ≃ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↥(Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.representedVertexModule y))

The incoming-arrow range family is linearly equivalent to the radical of the represented projective.