Peak wedges in string modules

A string which runs backwards along one ordinary path into a common vertex and then forwards along another ordinary path is a peak wedge. When both endpoints are maximal peaks, every position of the word is reached from the common vertex by one of the two outgoing arms.

The strict overlap of left and right cohook deletions has exactly this form. This file packages that geometry independently of the deletion bookkeeping; the resulting peak position is the generator used to compare the literal right-string module with a covariant representable on the opposite quotient category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pathReach_of_prefix_eq_positivePath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (p : Quiver.Path x y) (i : C.PositionAt x) (j : C.PositionAt y) : ↑j = Quiver.Path.comp (↑i) (positivePath p) → C.PathReach p i j

A positive path occurring literally after one word prefix gives reachability in the displayed arrow direction.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Type u

A maximal two-arm peak decomposition of a string word.

• peak : Q
• leftArm : Quiver.Path self.peak C.source
• rightArm : Quiver.Path self.peak C.target
• path_eq : C.path = (Quiver.Path.reverse (positivePath self.leftArm)).comp (positivePath self.rightArm)
• startsOnPeak : C.StartsOnPeak
• endsOnPeak : C.EndsOnPeak

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.word_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) : length R C = W.leftArm.length + W.rightArm.length

The word length is the sum of the two arm lengths.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) : C.PositionAt W.peak

The occurrence of the common peak between the two arms.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) : W.peakPosition.index = W.leftArm.length

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.rightPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) {x : Q} (p : Quiver.Path W.peak x) (q : Quiver.Path x C.target) (h : W.rightArm = p.comp q) : C.PositionAt x

The position reached after following an initial segment of the right arm from the peak.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.rightPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) {x : Q} (p : Quiver.Path W.peak x) (q : Quiver.Path x C.target) (h : W.rightArm = p.comp q) : (W.rightPosition p q h).index = W.leftArm.length + p.length

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.pathReach_rightPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) {x : Q} (p : Quiver.Path W.peak x) (q : Quiver.Path x C.target) (h : W.rightArm = p.comp q) : C.PathReach p W.peakPosition (W.rightPosition p q h)

The right-arm position is reached from the peak by its defining initial segment.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.leftPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) {x : Q} (p : Quiver.Path W.peak x) (q : Quiver.Path x C.source) (h : W.leftArm = p.comp q) : C.PositionAt x

The position reached after following an initial segment of the left arm from the peak. In the written word this position occurs on the reversed left arm.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.leftPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) {x : Q} (p : Quiver.Path W.peak x) (q : Quiver.Path x C.source) (h : W.leftArm = p.comp q) : (W.leftPosition p q h).index = q.length

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.pathReach_leftPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) {x : Q} (p : Quiver.Path W.peak x) (q : Quiver.Path x C.source) (h : W.leftArm = p.comp q) : C.PathReach p W.peakPosition (W.leftPosition p q h)

The left-arm position is reached from the peak by its defining initial segment.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.exists_pathReach_peak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) (i : C.Position) : ∃ (p : Quiver.Path W.peak i.fst), C.PathReach p W.peakPosition i.snd

Every occurrence along a peak wedge is reached from the common peak by an ordinary path along one of its two arms.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.path_eq_of_pathReach_peak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) {y : Q} (p q : Quiver.Path W.peak y) (j : C.PositionAt y) (hp : C.PathReach p W.peakPosition j) (hq : C.PathReach q W.peakPosition j) : p = q

An ordinary path from the common peak is determined by the word position which it reaches.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.reverse {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (W : C.PeakWedge) : (Word.reverse R C).PeakWedge

Reversing a peak wedge exchanges its two outgoing arms.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.not_surviving_of_rightArm_strictPrefix {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) {y : Q} (p : Quiver.Path W.peak y) (hp : pathMap P.relations p ≠ 0) (hprefix : ∃ (r : Quiver.Path C.target y), p = W.rightArm.comp r) (hlength : W.rightArm.length < p.length) : False

A surviving path cannot strictly extend the maximal right arm of a two-sided peak wedge.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.not_surviving_of_leftArm_strictPrefix {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) {y : Q} (p : Quiver.Path W.peak y) (hp : pathMap P.relations p ≠ 0) (hprefix : ∃ (r : Quiver.Path C.source y), p = W.leftArm.comp r) (hlength : W.leftArm.length < p.length) : False

A surviving path cannot strictly extend the maximal left arm of a two-sided peak wedge.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.IsArmPrefix {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) {y : Q} (p : Quiver.Path W.peak y) : Prop

A path from the peak is a prefix of one of the two outgoing arms.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.isArmPrefix_of_pathMap_ne_zero {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) {y : Q} (p : Quiver.Path W.peak y) (hp : pathMap P.relations p ≠ 0) : IsArmPrefix P W p

Every surviving ordinary path starting at the common peak is a prefix of one of the two arms.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.exists_pathReach_peak_of_pathMap_ne_zero {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) {y : Q} (p : Quiver.Path W.peak y) (hp : pathMap P.relations p ≠ 0) : ∃ (j : C.PositionAt y), C.PathReach p W.peakPosition j

Every surviving path from the common peak reaches a word position.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.survivingPathTargetPosition {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) (y : Q) (p : SurvivingPath P.relations W.peak y) : C.PositionAt y

The target position reached by a surviving path from the common peak.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.pathReach_survivingPathTargetPosition {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) (y : Q) (p : SurvivingPath P.relations W.peak y) : C.PathReach (↑p) W.peakPosition (survivingPathTargetPosition P W hleft hright y p)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.positionSurvivingPath {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) (y : Q) (j : C.PositionAt y) : SurvivingPath P.relations W.peak y

The surviving ordinary path which reaches a given word position from the common peak.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.pathReach_positionSurvivingPath {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) (y : Q) (j : C.PositionAt y) : C.PathReach (↑(positionSurvivingPath P W y j)) W.peakPosition j

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.survivingPathEquivPositionAt {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) (y : Q) : SurvivingPath P.relations W.peak y ≃ C.PositionAt y

Surviving paths from the common peak are in bijection with the word positions over each displayed vertex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_peakWedge_of_overlappingCohookDeletions {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {C L D : Word P.relations} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hoverlap : length P.relations C < leftDeletion.steps + rightDeletion.steps) : ∃ (W : C.PeakWedge), W.leftArm.length = leftDeletion.cohook.tail.steps ∧ W.rightArm.length = rightDeletion.cohook.tail.steps ∧ 0 < W.leftArm.length ∧ 0 < W.rightArm.length

A strict overlap of left and right cohook deletions produces a maximal peak wedge whose two nonempty arms have exactly the cohook-tail lengths.