The selected coordinate of the arrow-cokernel radical section #
theorem
MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelRadicalSection_selectedCoordinate
{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)
(z : ↥(Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.arrowCokernelFGObj a)))
:
(P.incomingArrowRangeFamilyRadicalLinearEquiv y).symm ((P.arrowCokernelRadicalSection a) z) ⟨x, a⟩ = 0
The canonical radical section has zero selected-arrow coordinate.