Pure peak strings as one-arm representables

A pure-positive string which starts and ends on peaks is the complete surviving path arm from its source. Evaluation at the source therefore identifies its literal finite right-string module with the finite representable there. Reversal gives the pure-negative case.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmPeakWedge {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {C : Word R} (arm : (vertex R hR C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) : C.PeakWedge

A pure-positive word with both endpoints on peaks is a peak wedge whose left arm is trivial.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.IsPurePositive.exists_oneArmPeakWedge {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) : ∃ (W : C.PeakWedge), W.leftArm.length = 0 ∧ W.rightArm.length = length R C

The one nontrivial arm of a pure-positive peak wedge has the full word length.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.ordinaryPath_factor_of_vertex_of_peaks {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} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) {y : Q} (p : Quiver.Path C.source y) (hp : pathMap P.relations p ≠ 0) : ∃ (r : Quiver.Path y C.target), arm.ordinaryPath = p.comp r

Every surviving path from the source of a pure peak arm is a prefix of that arm, including when the arm is the trivial path.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.exists_pathReach_oneArm_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} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) {y : Q} (p : Quiver.Path C.source y) (hp : pathMap P.relations p ≠ 0) : ∃ (j : C.PositionAt y), C.PathReach p (oneArmPeakWedge ⋯ arm ⋯ ⋯).peakPosition j

Every surviving path from the one-arm peak reaches a word position.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmSurvivingPathTargetPosition {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} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) (y : Q) (p : SurvivingPath P.relations C.source y) : C.PositionAt y

The position reached by a surviving path from a one-arm peak.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.pathReach_oneArmSurvivingPathTargetPosition {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} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) (y : Q) (p : SurvivingPath P.relations C.source y) : C.PathReach (↑p) (oneArmPeakWedge ⋯ arm ⋯ ⋯).peakPosition (oneArmSurvivingPathTargetPosition P arm ⋯ ⋯ y p)

The selected one-arm target position is reached by its path.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmSurvivingPathEquivPositionAt {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} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) (y : Q) : SurvivingPath P.relations C.source y ≃ C.PositionAt y

Surviving paths from a one-arm peak are equivalent to word positions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmPeakRepresentableHom_app_basis {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 : StringPresentation k A Q) {C : Word P.relations} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) (y : Q) (p : SurvivingPath P.relations C.source y) : (ModuleCat.Hom.hom ((PeakWedge.peakRepresentableHom P (MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmWedge✝ P arm ⋯ ⋯)).hom.hom.app (Opposite.op (obj P.relations y)))) ((PeakWedge.peakRepresentableBasis P (MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmWedge✝ P arm ⋯ ⋯) y) p) = Finsupp.single (oneArmSurvivingPathTargetPosition P.toSpecialBiserialPresentation arm ⋯ ⋯ y p) 1

Source evaluation sends a surviving-path basis vector to the reached word-position basis vector.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmPeakRepresentableComponentLinearEquiv {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 : StringPresentation k A Q) {C : Word P.relations} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) (y : Q) : ↑((PeakWedge.peakRepresentable P (MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmWedge✝ P arm ⋯ ⋯)).obj.obj.obj (Opposite.op (obj P.relations y))) ≃ₗ[k] C.Space y

The componentwise basis equivalence for a one-arm peak.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmPeakRepresentableHom_app_eq {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 : StringPresentation k A Q) {C : Word P.relations} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) (y : Q) : ModuleCat.Hom.hom ((PeakWedge.peakRepresentableHom P (MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmWedge✝ P arm ⋯ ⋯)).hom.hom.app (Opposite.op (obj P.relations y))) = ↑(oneArmPeakRepresentableComponentLinearEquiv P arm ⋯ ⋯ y)

Source evaluation agrees with the componentwise basis equivalence.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmPeakRepresentableHom_isIso {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 : StringPresentation k A Q) {C : Word P.relations} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) : CategoryTheory.IsIso (PeakWedge.peakRepresentableHom P (MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmWedge✝ P arm ⋯ ⋯))

Source evaluation is an isomorphism for a one-arm peak, including the trivial-arm vertex case.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmPeakRepresentableIso {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 : StringPresentation k A Q) {C : Word P.relations} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) : PeakWedge.peakRepresentable P (MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.oneArmWedge✝ P arm ⋯ ⋯) ≅ C.finiteRightModule ⋯

A one-arm peak string is the finite representable at its source.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.finiteRightModule_projective_of_oneArmPeaks {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 : StringPresentation k A Q) {C : Word P.relations} (arm : (vertex P.relations ⋯ C.source).PositiveExtension C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) : CategoryTheory.Projective (C.finiteRightModule ⋯)

The literal module of a one-arm peak is projective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModule_projective_of_isPurePositive_of_peaks {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 : StringPresentation k A Q) {C : Word P.relations} (hpure : IsPurePositive ⋯ C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) : CategoryTheory.Projective (C.finiteRightModule ⋯)

A pure-positive word on peaks at both endpoints is projective, including the length-zero vertex case.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModule_projective_of_isPureNegative_of_peaks {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 : StringPresentation k A Q) {C : Word P.relations} (hpure : IsPureNegative ⋯ C) (hstart : C.StartsOnPeak) (hend : C.EndsOnPeak) : CategoryTheory.Projective (C.finiteRightModule ⋯)

The reversed pure-negative version of one-arm peak projectivity.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_leftHook_of_isPurePositive_of_startsOnPeak_of_not_projective {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 : StringPresentation k A Q) {C : Word P.relations} (hpure : IsPurePositive ⋯ C) (hstart : C.StartsOnPeak) (hnonprojective : ¬CategoryTheory.Projective (C.finiteRightModule ⋯)) : Nonempty C.LeftHookExtension

A nonprojective pure-positive word which is maximal at its right endpoint must admit a maximal left hook.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_hook_of_isPureNegative_of_endsOnPeak_of_not_projective {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 : StringPresentation k A Q) {C : Word P.relations} (hpure : IsPureNegative ⋯ C) (hend : C.EndsOnPeak) (hnonprojective : ¬CategoryTheory.Projective (C.finiteRightModule ⋯)) : ∃ (D : Word P.relations), Nonempty (C.HookExtension D)

A nonprojective pure-negative word which is maximal at its left endpoint must admit a maximal right hook.