The radical map of a string-arrow cokernel

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowRadicalMapAlgebraFiniteDimensional {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.arrowRadicalMapAlgebraOppositeIsNoetherian {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.arrowCokernelRadicalLinearMap {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) : ↥(Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.representedVertexModule y)) →ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↥(Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.arrowCokernelFGObj a))

The projective radical maps linearly onto the radical of the arrow cokernel.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelRadicalMap {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) : P.representedVertexRadicalFGObj y ⟶ FGModuleCat.of P.quotientCategoryAlgebraᵐᵒᵖ ↥(Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.arrowCokernelFGObj a))

The projective radical map, bundled in the finite module category.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelRadicalMap_surjective {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) : Function.Surjective ⇑(P.arrowCokernelRadicalLinearMap a)

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelRadicalMap_ker {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) : (P.arrowCokernelRadicalLinearMap a).ker = (P.arrowBranchRadicalInclusionLinearMap ⟨x, a⟩).range