Magnitude conjecture

MagnitudeConjecture.Algebra.StringArrowCokernelBranchIdentification

Identifying the surviving branch family with the cokernel radical #

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.otherIncomingFamilyCokernelRadicalLinearEquiv {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) :
((b : OtherIncomingArrow ⟨x, a⟩) → ↥(P.representedArrowLinearMap (↑b).snd).range) ≃ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↥(Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.arrowCokernelFGObj a))

The radical of V(a) is linearly equivalent to the family of all incoming-arrow ranges other than the range generated by a.

Instances For