Magnitude conjecture

MagnitudeConjecture.Algebra.StringProjectiveRadicalDecompositionBasic

Basic objects for decomposing string projective radicals #

source
noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.displayedIncomingArrowEquivFin {Q : Type u} [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (y : Q) :
Fin (Nat.card (DisplayedIncomingArrow y)) ≃ DisplayedIncomingArrow y
Instances For
    source
    noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalSummand {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) (i : Fin (Nat.card (DisplayedIncomingArrow y))) :
    FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ
    Instances For