Branch maps for the represented projective radical

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchMapsAlgebraFiniteDimensional {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) : FiniteDimensional k P.quotientCategoryAlgebra

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchMapsAlgebraOppositeIsNoetherian {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) : IsNoetherianRing P.quotientCategoryAlgebraᵐᵒᵖ

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchRadicalInclusionLinearMap {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 literal linear inclusion of one incoming-arrow range into the represented projective radical.

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

The literal coordinate projection from the represented projective radical onto one incoming-arrow range.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchRadicalInclusion {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.incomingArrowRangeFGObj a ⟶ P.representedVertexRadicalFGObj y

The literal arrow branch included in the represented projective radical.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchRadicalProjection {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.representedVertexRadicalFGObj y ⟶ P.incomingArrowRangeFGObj a

Coordinate projection from the radical onto one arrow branch.