Magnitude conjecture

MagnitudeConjecture.Algebra.StringArrowRightIdealBasis

The global continuation basis of a string-arrow right ideal #

The product decomposition of the represented arrow range supplies a basis indexed by all surviving paths before the arrow, with their starting vertices retained.

source
def MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationSigmaEquiv {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 : Q) × P.LeftContinuationAt a z ≃ P.LeftContinuationPath a

Collecting the fixed-startpoint continuation types over all displayed vertices gives the manuscript's complete left-continuation type.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationSigmaEquiv_symm_apply {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 : P.LeftContinuationPath a) :
    (P.leftContinuationSigmaEquiv a).symm p = ⟨(↑p).fst, ⟨(↑p).snd, ⋯⟩⟩
    source
    noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationObjectSigmaEquiv {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) :
    (X : Category P.relations) × P.LeftContinuationAt a (P.quotientObjectEquiv X) ≃ P.LeftContinuationPath a

    Reindexing the small family of pointwise continuation indices from quotient-category objects to displayed vertices, and then collecting them into complete left continuations.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftContinuationObjectSigmaEquiv_symm_apply {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 : P.LeftContinuationPath a) :
      (P.leftContinuationObjectSigmaEquiv a).symm p = ⟨obj P.relations (↑p).fst, ⟨(↑p).snd, ⋯⟩⟩
      source
      noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowRangeBasis {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.Basis (P.LeftContinuationPath a) k ↥(P.representedArrowKLinearMap a).range

      The global range of the represented arrow has a basis indexed by all surviving paths before that arrow, with the starting vertex retained.

      Instances For
        source
        theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowRangeBasis_coordinate_self {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 : P.LeftContinuationPath a) :
        (P.representedArrowRangeCoordinateLinearEquiv a) ((P.representedArrowRangeBasis a) p) (obj P.relations (↑p).fst) = (P.leftArrowCoordinateBasis a (↑p).fst) ⟨(↑p).snd, ⋯⟩

        At its starting vertex, a global basis vector is the corresponding pointwise continuation-path vector.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowRangeBasis_coordinate_ne {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 : P.LeftContinuationPath a) (z : Q) (hz : z ≠ (↑p).fst) :
        (P.representedArrowRangeCoordinateLinearEquiv a) ((P.representedArrowRangeBasis a) p) (obj P.relations z) = 0

        Away from its starting vertex, a global continuation basis vector has zero coordinate.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringPresentation.finrank_representedArrowKLinearMap_range_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) {x y : Q} (a : x ⟶ y) :
        Module.finrank k ↥(P.representedArrowKLinearMap a).range = Nat.card (P.LeftContinuationPath a)

        The coefficient-field dimension of the assembled represented arrow image is the number of its surviving left continuations.