Magnitude conjecture

MagnitudeConjecture.Algebra.StringProjectiveRadical

Projective radicals of a string category algebra #

Dimension and maximal-submodule arguments identify the incoming-arrow sum inside a represented canonical projective with its Jacobson radical.

source
instance MagnitudeConjecture.BoundQuiver.StringPresentation.incomingContinuationFinite {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) :
Finite ((a : DisplayedIncomingArrow y) × P.LeftContinuationPath a.snd)

The total continuation-basis index over all arrows ending at a vertex is finite.

source
def MagnitudeConjecture.BoundQuiver.StringPresentation.nilVertexPath {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) :
P.VertexPath y

The zero-length surviving path ending at y is the trivial path at y.

Instances For
    source
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.zeroLengthVertexPath_unique {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) (p : { p : P.VertexPath y // (↑p.snd).length = 0 }) :
    ↑p = P.nilVertexPath y

    There is exactly one zero-length surviving path ending at a fixed vertex.

    source
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.natCard_zeroLengthVertexPath_eq_one {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) :
    Nat.card { p : P.VertexPath y // (↑p.snd).length = 0 } = 1

    The zero-length part of the global represented-projective path basis has cardinality one.

    source
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.natCard_vertexPath_eq_positive_add_one {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) :
    Nat.card (P.VertexPath y) = Nat.card (P.PositiveVertexPath y) + 1

    The complete path basis is the disjoint union of the nontrivial path basis and the unique trivial path.

    source
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.finrank_representedVertexModule_eq_natCard {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) :
    Module.finrank k ↑(P.representedVertexModule y) = Nat.card (P.VertexPath y)

    The represented canonical projective has dimension equal to the number of its surviving-path basis vectors.

    source
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.finrank_incomingArrowRangeFamily_eq_natCard {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) :
    Module.finrank k ((a : DisplayedIncomingArrow y) → ↥(P.representedArrowLinearMap a.snd).range) = Nat.card ((a : DisplayedIncomingArrow y) × P.LeftContinuationPath a.snd)

    The product of incoming arrow ranges has dimension equal to its literal continuation-basis cardinality.

    source
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.finrank_incomingArrowRangeSum_quotient_eq_one {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) :
    Module.finrank k (↑(P.representedVertexModule y) ⧸ (P.incomingArrowRangeSumLinearMap y).range) = 1

    The sum of all represented arrow ranges ending at a vertex has codimension one in the corresponding canonical projective.

    source
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeSum_isCoatom {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) :
    IsCoatom (P.incomingArrowRangeSumLinearMap y).range

    The internal sum of all represented arrow ranges ending at a vertex is a maximal submodule of the corresponding canonical projective.

    source
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeSum_eq_jacobson {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) :
    (P.incomingArrowRangeSumLinearMap y).range = Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.representedVertexModule y)

    The internal sum of the represented incoming-arrow ranges is exactly the module Jacobson radical of the represented canonical projective.