Magnitude conjecture

MagnitudeConjecture.CategoryTheory.LinearPathIncoming

Freeness of the incoming-arrow map in a linear path category #

A family of free-path morphisms followed by distinct arrows into a fixed target has a unique expression. This is the path-basis input used to identify the middle kernel in a mesh-simple presentation.

source
@[reducible, inline]
abbrev MagnitudeConjecture.LinearPathCategory.IncomingArrow {Q : Type v} [Quiver Q] (z : Q) :
Type (max v w)

Reversed quiver arrows whose represented categorical maps end at z.

Instances For
    source
    @[reducible, inline]
    abbrev MagnitudeConjecture.LinearPathCategory.IncomingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x z : Q) :
    Type (max (max w v) (max u v) w)

    One free-path coefficient before every arrow into z.

    Instances For
      source
      noncomputable def MagnitudeConjecture.LinearPathCategory.incomingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype (IncomingArrow z)] {x z : Q} (c : IncomingCoefficient x z) :
      obj k Q x ⟶ obj k Q z

      Sum a family of free-path coefficients followed by the corresponding arrows into the target.

      Instances For
        source
        noncomputable def MagnitudeConjecture.LinearPathCategory.singleIncomingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x z : Q} (a₀ : IncomingArrow z) (f : obj k Q x ⟶ obj k Q a₀.fst) :
        IncomingCoefficient x z

        A free-path coefficient family supported at one incoming arrow.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.LinearPathCategory.incomingSum_single {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype (IncomingArrow z)] {x z : Q} (a₀ : IncomingArrow z) (f : obj k Q x ⟶ obj k Q a₀.fst) :
          incomingSum (singleIncomingCoefficient a₀ f) = CategoryTheory.CategoryStruct.comp f (pathHom a₀.snd.toPath)

          Summing a family supported at one incoming arrow recovers the displayed composite.

          source
          noncomputable def MagnitudeConjecture.LinearPathCategory.incomingSumLinearMap {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype (IncomingArrow z)] (x z : Q) :
          IncomingCoefficient x z →ₗ[k] obj k Q x ⟶ obj k Q z

          The incoming-arrow sum as a linear map.

          Instances For
            source
            @[simp]
            theorem MagnitudeConjecture.LinearPathCategory.incomingSumLinearMap_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype (IncomingArrow z)] {x z : Q} (c : IncomingCoefficient x z) :
            (incomingSumLinearMap x z) c = incomingSum c
            source
            def MagnitudeConjecture.LinearPathCategory.prependIncomingPath {Q : Type v} [Quiver Q] {x z : Q} (t : (a : IncomingArrow z) × Quiver.Path a.fst x) :
            Quiver.Path z x

            Prefix a reverse-quiver path by the reverse of one incoming categorical arrow.

            Instances For
              source
              theorem MagnitudeConjecture.LinearPathCategory.prependIncomingPath_injective {Q : Type v} [Quiver Q] (x z : Q) :
              Function.Injective prependIncomingPath

              Distinct incoming arrows followed by arbitrary tails produce distinct paths.

              source
              def MagnitudeConjecture.LinearPathCategory.prependIncomingPathEmbedding {Q : Type v} [Quiver Q] (x z : Q) :
              (a : IncomingArrow z) × Quiver.Path a.fst x ↪ Quiver.Path z x

              The prefix operation as an embedding of path indices.

              Instances For
                source
                noncomputable def MagnitudeConjecture.LinearPathCategory.incomingCoefficientBasis {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype (IncomingArrow z)] (x z : Q) :
                Module.Basis ((a : IncomingArrow z) × Quiver.Path a.fst x) k (IncomingCoefficient x z)

                The product path basis on the domain of the incoming-arrow map.

                Instances For
                  source
                  theorem MagnitudeConjecture.LinearPathCategory.incomingSumLinearMap_basis {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype (IncomingArrow z)] (x z : Q) (t : (a : IncomingArrow z) × Quiver.Path a.fst x) :
                  (incomingSumLinearMap x z) ((incomingCoefficientBasis x z) t) = pathHom (prependIncomingPath t)

                  An incoming product-basis vector maps to the corresponding prefixed path basis vector.

                  source
                  theorem MagnitudeConjecture.LinearPathCategory.incomingSumLinearMap_injective {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype (IncomingArrow z)] (x z : Q) :
                  Function.Injective ⇑(incomingSumLinearMap x z)

                  The free incoming-arrow map is injective.