Magnitude conjecture

MagnitudeConjecture.Algebra.StringProjectiveIncomingSumBasic

Incoming-arrow sum data in represented string projectives #

Nontrivial surviving paths split according to their final displayed arrow. This file identifies the corresponding internal sum with the radical of the represented canonical projective.

source
@[reducible, inline]
abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.PositiveVertexPath {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) :
Type u

Nontrivial surviving paths ending at a fixed vertex.

Instances For
    source
    def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingContinuationToPositiveVertexPath {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) :
    (a : DisplayedIncomingArrow y) × P.LeftContinuationPath a.snd → P.PositiveVertexPath y

    Concatenating a left continuation with its displayed final arrow gives the corresponding nontrivial surviving path.

    Instances For
      source
      def MagnitudeConjecture.BoundQuiver.StringPresentation.positiveVertexPathToIncomingContinuation {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.PositiveVertexPath y → (a : DisplayedIncomingArrow y) × P.LeftContinuationPath a.snd

      The final arrow of a nontrivial path and its preceding segment recover the unique incoming-arrow continuation index.

      Instances For
        source
        def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingContinuationEquivPositiveVertexPath {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) :
        (a : DisplayedIncomingArrow y) × P.LeftContinuationPath a.snd ≃ P.PositiveVertexPath y

        Partitioning a nontrivial surviving path by its final displayed arrow is a bijection.

        Instances For
          source
          noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeSumLinearMap {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) :
          ((a : DisplayedIncomingArrow y) → ↥(P.representedArrowLinearMap a.snd).range) →ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↑(P.representedVertexModule y)

          Sum the represented arrow ranges ending at y inside the represented canonical projective at y.

          Instances For
            source
            noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeSumKLinearMap {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) :
            ((a : DisplayedIncomingArrow y) → ↥(P.representedArrowLinearMap a.snd).range) →ₗ[k] ↑(P.representedVertexModule y)

            The coefficient-field version of the incoming-arrow range sum.

            Instances For
              source
              noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowModuleBasisFamily {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) (a : DisplayedIncomingArrow y) :
              Module.Basis (P.LeftContinuationPath a.snd) k ↥(P.representedArrowLinearMap a.snd).range

              The continuation basis in each incoming-arrow coordinate, packaged as a named dependent family so coordinatewise basis operations need not unfold its representation-theoretic construction.

              Instances For
                source
                noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeBasis {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.Basis ((a : DisplayedIncomingArrow y) × P.LeftContinuationPath a.snd) k ((a : DisplayedIncomingArrow y) → ↥(P.representedArrowLinearMap a.snd).range)

                The product of the continuation bases is the coefficient-field basis of the family of incoming represented-arrow ranges.

                Instances For