Splitting the radical map of a string-arrow cokernel

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

A canonical section of the projective-radical quotient obtained by discarding the selected arrow coordinate.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelRadicalMap_section {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 ∘ₗ P.arrowCokernelRadicalSection a = LinearMap.id