Magnitude conjecture

MagnitudeConjecture.Algebra.StringDetectorSplitTransport

Transporting contextual string detectors along a word #

One-letter split equivalences compose along a finite walk of displayed cuts. Their naturality therefore composes as well. A walk ending at the target cut identifies its contextual detector with the canonical endpoint detector.

source
theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.ext {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} {c d : E.Split} (hvertex : c.vertex = d.vertex) (hprefix : c.prefixPath ≍ d.prefixPath) (hsuffix : c.suffixPath ≍ d.suffixPath) :
c = d

A split is determined by its displayed vertex and its two dependent path pieces.

source
theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.ext_iff {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} {c d : E.Split} :
c = d ↔ c.vertex = d.vertex ∧ c.prefixPath ≍ d.prefixPath ∧ c.suffixPath ≍ d.suffixPath
source
def MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.positiveStepOfArrowStep {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} {x y : Q} (i : E.PositionAt x) (j : E.PositionAt y) (a : x ⟶ y) (hindex : j.index = i.index + 1) (hstep : E.ArrowStep a i j) :
(ofPosition E ⟨x, i⟩).PositiveStep (ofPosition E ⟨y, j⟩)

Consecutive word positions separated by a positively traversed arrow give a positive split step.

Instances For
    source
    def MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.negativeStepOfArrowStep {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} {x y : Q} (i : E.PositionAt x) (j : E.PositionAt y) (a : y ⟶ x) (hindex : j.index = i.index + 1) (hstep : E.ArrowStep a j i) :
    (ofPosition E ⟨x, i⟩).NegativeStep (ofPosition E ⟨y, j⟩)

    Consecutive word positions separated by an inversely traversed arrow give a negative split step.

    Instances For
      source
      def MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.targetPosition {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} (E : Word P.relations) :
      E.Position

      The total position at the target endpoint.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.targetPosition_index {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} (E : Word P.relations) :
        (targetPosition E).index = length P.relations E
        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.ofPosition_targetPosition {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} (E : Word P.relations) :
        ofPosition E (targetPosition E) = target E

        The split attached to the target position is the target split.

        source
        inductive MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.Walk {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} :
        E.Split → E.Split → Type u

        A finite sequence of consecutive displayed cuts, moving from left to right through the word.

        Instances For
          source
          theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.nonempty_walk_to_target {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} (E : Word P.relations) (i : E.Position) :
          Nonempty ((ofPosition E i).Walk (target E))

          Every displayed word position admits a finite walk through consecutive letters to the target cut.

          source
          noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.walkToTarget {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} (E : Word P.relations) (i : E.Position) :
          (ofPosition E i).Walk (target E)

          A chosen walk from a displayed position to the target cut.

          Instances For
            source
            noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpaceWalkEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) {c d : E.Split} (walk : c.Walk d) :
            SplitDetectorSpace N S E c ≃ₗ[k] SplitDetectorSpace N S E d

            Composite change of split along a finite walk.

            Instances For
              source
              @[simp]
              theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpaceWalkEquiv_nil {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (c : E.Split) :
              splitDetectorSpaceWalkEquiv N S (Word.Split.Walk.nil c) = LinearEquiv.refl k (SplitDetectorSpace N S E c)
              source
              @[simp]
              theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpaceWalkEquiv_positive {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) {c d e : E.Split} (step : c.PositiveStep d) (tail : d.Walk e) :
              splitDetectorSpaceWalkEquiv N S (Word.Split.Walk.positive step tail) = splitDetectorSpacePositiveStepEquiv N S E step ≪≫ₗ splitDetectorSpaceWalkEquiv N S tail
              source
              @[simp]
              theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpaceWalkEquiv_negative {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) {c d e : E.Split} (step : c.NegativeStep d) (tail : d.Walk e) :
              splitDetectorSpaceWalkEquiv N S (Word.Split.Walk.negative step tail) = splitDetectorSpaceNegativeStepEquiv N S E step ≪≫ₗ splitDetectorSpaceWalkEquiv N S tail
              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorLinearMap_walk {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [M.Additive] [N.Additive] (f : M ⟶ N) (S : P.ArrowPolarization) {c d : E.Split} (walk : c.Walk d) (q : SplitDetectorSpace M S E c) :
              (splitDetectorSpaceWalkEquiv N S walk) ((splitDetectorLinearMap f S E c) q) = (splitDetectorLinearMap f S E d) ((splitDetectorSpaceWalkEquiv M S walk) q)

              Composite change of split commutes with every module morphism.

              source
              noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpaceToTargetEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) {c : E.Split} (walk : c.Walk (Word.Split.target E)) :
              SplitDetectorSpace N S E c ≃ₗ[k] DetectorSpace N (detectorEndpoint S E)

              A walk to the target cut identifies a contextual detector with the canonical endpoint detector.

              Instances For
                source
                theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorLinearMap_toTarget {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [M.Additive] [N.Additive] (f : M ⟶ N) (S : P.ArrowPolarization) {c : E.Split} (walk : c.Walk (Word.Split.target E)) (q : SplitDetectorSpace M S E c) :
                (splitDetectorSpaceToTargetEquiv N S walk) ((splitDetectorLinearMap f S E c) q) = (detectorLinearMap f (detectorEndpoint S E)) ((splitDetectorSpaceToTargetEquiv M S walk) q)

                Transport to the target detector is natural in the represented module.

                source
                noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpacePositionEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (i : E.Position) :
                SplitDetectorSpace N S E (Word.Split.ofPosition E i) ≃ₗ[k] DetectorSpace N (detectorEndpoint S E)

                The canonical endpoint detector, transported from the contextual detector at a displayed position.

                Instances For
                  source
                  theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorLinearMap_position {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {E : Word P.relations} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [M.Additive] [N.Additive] (f : M ⟶ N) (S : P.ArrowPolarization) (i : E.Position) (q : SplitDetectorSpace M S E (Word.Split.ofPosition E i)) :
                  (splitDetectorSpacePositionEquiv N S i) ((splitDetectorLinearMap f S E (Word.Split.ofPosition E i)) q) = (detectorLinearMap f (detectorEndpoint S E)) ((splitDetectorSpacePositionEquiv M S i) q)

                  Position-to-endpoint transport commutes with every module morphism.