Determinism after the first hook or cohook letter

The unsigned trivial word at a branching vertex may admit two extensions, so global endpoint uniqueness is deliberately not asserted. Once a first hook or cohook letter has been chosen, however, reducedness excludes that same displayed arrow from the opposite-sign tail. The special-biserial degree-two bound then makes the first tail arrow unique.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.eq_of_ne_of_ne_of_natCard_le_two {T : Type u_1} [Finite T] (a b c : T) (hba : b ≠ a) (hca : c ≠ a) (hcard : Nat.card T ≤ 2) : b = c

In a finite type of cardinality at most two, two elements different from the same marked element coincide.

@[reducible, inline]

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

Positive displayed arrows which can be appended to a word while retaining the string condition.

@[reducible, inline]

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

Negative displayed arrows which can be appended to a word while retaining the string condition.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positive_negative_not_string {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (a : C.target ⟶ z) (h : IsString R ((Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a))).comp (Quiver.Hom.toPath (negativeArrow a)))) : False

A positive displayed arrow cannot be followed immediately by its formal inverse in a string.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.negative_positive_not_string {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (a : z ⟶ C.target) (h : IsString R ((Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a))).comp (Quiver.Hom.toPath (positiveArrow a)))) : False

A negative displayed arrow cannot be followed immediately by its formal inverse in a string.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.negativeTail_costar_ne_boundary {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z w : Q} (a : C.target ⟶ z) (b : w ⟶ z) (h : IsString R ((Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a))).comp (Quiver.Hom.toPath (negativeArrow b)))) : ⟨w, b⟩ ≠ ⟨C.target, a⟩

After a chosen positive boundary arrow, reducedness excludes that arrow from being the first negative-tail arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positiveTail_star_ne_boundary {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z w : Q} (a : z ⟶ C.target) (b : z ⟶ w) (h : IsString R ((Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a))).comp (Quiver.Hom.toPath (positiveArrow b)))) : ⟨w, b⟩ ≠ ⟨C.target, a⟩

After a chosen negative boundary arrow, reducedness excludes that arrow from being the first positive-tail arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.consecutiveNegative_arrowMap_comp_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {w x : Q} (b : w ⟶ C.target) (hb : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow b)))) (a : x ⟶ w) (ha : IsString R (Quiver.Path.comp (append R C (negativeArrow b) hb).path (Quiver.Hom.toPath (negativeArrow a)))) : CategoryTheory.CategoryStruct.comp (arrowMap R b) (arrowMap R a) ≠ 0

Two consecutive negative letters in a string give a surviving ordinary two-arrow path in the reversed word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.consecutivePositive_arrowMap_comp_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {w x : Q} (b : C.target ⟶ w) (hb : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow b)))) (a : w ⟶ x) (ha : IsString R (Quiver.Path.comp (append R C (positiveArrow b) hb).path (Quiver.Hom.toPath (positiveArrow a)))) : CategoryTheory.CategoryStruct.comp (arrowMap R a) (arrowMap R b) ≠ 0

Two consecutive positive letters in a string give a surviving ordinary two-arrow path in the word itself.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.negativeTail_firstArrow_unique {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) (C : Word P.relations) {z w₁ w₂ : Q} (a : C.target ⟶ z) (b₁ : w₁ ⟶ z) (b₂ : w₂ ⟶ z) (h₁ : IsString P.relations ((Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a))).comp (Quiver.Hom.toPath (negativeArrow b₁)))) (h₂ : IsString P.relations ((Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a))).comp (Quiver.Hom.toPath (negativeArrow b₂)))) : ⟨w₁, b₁⟩ = ⟨w₂, b₂⟩

In a special-biserial presentation, the first negative-tail arrow after a fixed positive hook boundary is unique.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positiveTail_firstArrow_unique {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) (C : Word P.relations) {z w₁ w₂ : Q} (a : z ⟶ C.target) (b₁ : z ⟶ w₁) (b₂ : z ⟶ w₂) (h₁ : IsString P.relations ((Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a))).comp (Quiver.Hom.toPath (positiveArrow b₁)))) (h₂ : IsString P.relations ((Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a))).comp (Quiver.Hom.toPath (positiveArrow b₂)))) : ⟨w₁, b₁⟩ = ⟨w₂, b₂⟩

In a special-biserial presentation, the first positive-tail arrow after a fixed negative cohook boundary is unique.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.negativeTail_eq_of_steps_eq {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) (C : Word P.relations) {z : Q} (a : C.target ⟶ z) (ha : IsString P.relations (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) {D₁ D₂ : Word P.relations} (tail₁ : (append P.relations C (positiveArrow a) ha).NegativeExtension D₁) (tail₂ : (append P.relations C (positiveArrow a) ha).NegativeExtension D₂) (hsteps : tail₁.steps = tail₂.steps) : ⟨D₁, tail₁⟩ = ⟨D₂, tail₂⟩

Once the positive boundary arrow is fixed, a negative tail is uniquely determined by its number of steps. The endpoint word and the arm witness are both retained in the dependent pair.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positiveTail_eq_of_steps_eq {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) (C : Word P.relations) {z : Q} (a : z ⟶ C.target) (ha : IsString P.relations (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))) {D₁ D₂ : Word P.relations} (tail₁ : (append P.relations C (negativeArrow a) ha).PositiveExtension D₁) (tail₂ : (append P.relations C (negativeArrow a) ha).PositiveExtension D₂) (hsteps : tail₁.steps = tail₂.steps) : ⟨D₁, tail₁⟩ = ⟨D₂, tail₂⟩

Once the negative boundary arrow is fixed, a positive tail is uniquely determined by its number of steps.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.negativeTail_eq_of_maximal {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) (C : Word P.relations) {z : Q} (a : C.target ⟶ z) (ha : IsString P.relations (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) {D₁ D₂ : Word P.relations} (tail₁ : (append P.relations C (positiveArrow a) ha).NegativeExtension D₁) (tail₂ : (append P.relations C (positiveArrow a) ha).NegativeExtension D₂) (hmax₁ : D₁.StartsInDeep) (hmax₂ : D₂.StartsInDeep) : ⟨D₁, tail₁⟩ = ⟨D₂, tail₂⟩

Two maximal negative tails after the same positive boundary are equal, including their endpoint words and arm witnesses.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positiveTail_eq_of_maximal {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) (C : Word P.relations) {z : Q} (a : z ⟶ C.target) (ha : IsString P.relations (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))) {D₁ D₂ : Word P.relations} (tail₁ : (append P.relations C (negativeArrow a) ha).PositiveExtension D₁) (tail₂ : (append P.relations C (negativeArrow a) ha).PositiveExtension D₂) (hmax₁ : D₁.StartsOnPeak) (hmax₂ : D₂.StartsOnPeak) : ⟨D₁, tail₁⟩ = ⟨D₂, tail₂⟩

Two maximal positive tails after the same negative boundary are equal.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.boundary {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} : (D : Word R) × C.HookExtension D → C.PositiveAppendArrow

Forget a maximal hook down to its chosen valid positive boundary arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.eq_of_boundary_eq {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) {C D₁ D₂ : Word P.relations} (hook₁ : C.HookExtension D₁) (hook₂ : C.HookExtension D₂) (hboundary : ⟨hook₁.vertex, hook₁.arrow⟩ = ⟨hook₂.vertex, hook₂.arrow⟩) : ⟨D₁, hook₁⟩ = ⟨D₂, hook₂⟩

In a special-biserial presentation, two maximal hooks with the same chosen positive boundary arrow are the same dependent hook extension.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.boundaryEquiv {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) (C : Word P.relations) : (D : Word P.relations) × C.HookExtension D ≃ C.PositiveAppendArrow

Maximal hooks over a fixed word are in bijection with the valid positive boundary arrows. Multiple boundaries at an unsigned trivial word remain distinct.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.boundary {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} : (D : Word R) × C.CohookExtension D → C.NegativeAppendArrow

Forget a maximal cohook down to its chosen valid negative boundary arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.eq_of_boundary_eq {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) {C D₁ D₂ : Word P.relations} (cohook₁ : C.CohookExtension D₁) (cohook₂ : C.CohookExtension D₂) (hboundary : ⟨cohook₁.vertex, cohook₁.arrow⟩ = ⟨cohook₂.vertex, cohook₂.arrow⟩) : ⟨D₁, cohook₁⟩ = ⟨D₂, cohook₂⟩

In a special-biserial presentation, two maximal cohooks with the same chosen negative boundary arrow are the same dependent cohook extension.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.boundaryEquiv {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) (C : Word P.relations) : (D : Word P.relations) × C.CohookExtension D ≃ C.NegativeAppendArrow

Maximal cohooks over a fixed word are in bijection with the valid negative boundary arrows.