Butler--Ringel arrow polarizations

Butler and Ringel choose two signs on the arrows of a string quiver. Arrows with a common source have distinct source signs, arrows with a common target have distinct target signs, and a surviving two-arrow path has opposite signs at its middle vertex. The special-biserial degree and continuation bounds are exactly what is needed to make such a choice.

We encode the two signs by Bool; Boolean negation is the source's change of sign. This file proves that every special-biserial presentation admits the choice, so polarization is data derived from the presentation rather than an extra hypothesis on later detector theorems.

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.CompatibleAt {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) {u : Q} (out : Quiver.Star u) (inc : Quiver.Costar u) : Prop

An outgoing and an incoming arrow at u are compatible when their two-arrow path survives the relation quotient.

structure MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.VertexPolarization {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) (u : Q) : Type u

A choice of Butler--Ringel signs at one vertex.

• sourceSign : Quiver.Star u → Bool
• targetSign : Quiver.Costar u → Bool
• sourceSign_injective : Function.Injective self.sourceSign
• targetSign_injective : Function.Injective self.targetSign
• compatible_sign (out : Quiver.Star u) (inc : Quiver.Costar u) : P.CompatibleAt out inc → self.sourceSign out = !self.targetSign inc

structure MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.ArrowPolarization {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) : Type u

A Butler--Ringel arrow polarization, assembled independently at every displayed vertex.

• atVertex (u : Q) : P.VertexPolarization u

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.ArrowPolarization.sourceSign {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} (S : P.ArrowPolarization) {x y : Q} (a : x ⟶ y) : Bool

The source sign sigma(a) of an ordinary arrow.

def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.ArrowPolarization.targetSign {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} (S : P.ArrowPolarization) {x y : Q} (a : x ⟶ y) : Bool

The target sign epsilon(a) of an ordinary arrow.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.ArrowPolarization.sourceSign_ne {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} (S : P.ArrowPolarization) {x y z : Q} {a : x ⟶ y} {b : x ⟶ z} (hab : ⟨y, a⟩ ≠ ⟨z, b⟩) : S.sourceSign a ≠ S.sourceSign b

Distinct arrows with a common source have distinct source signs.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.ArrowPolarization.targetSign_ne {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} (S : P.ArrowPolarization) {x y z : Q} {a : x ⟶ z} {b : y ⟶ z} (hab : ⟨x, a⟩ ≠ ⟨y, b⟩) : S.targetSign a ≠ S.targetSign b

Distinct arrows with a common target have distinct target signs.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.ArrowPolarization.sourceSign_eq_not_targetSign {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} (S : P.ArrowPolarization) {x y z : Q} (a : x ⟶ y) (b : y ⟶ z) (hcomp : CategoryTheory.CategoryStruct.comp (arrowMap P.relations b) (arrowMap P.relations a) ≠ 0) : S.sourceSign b = !S.targetSign a

A surviving composition has opposite signs at its middle vertex.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.exists_vertexPolarization {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) (u : Q) : Nonempty (P.VertexPolarization u)

The degree-two and unique-continuation axioms produce a polarization at each vertex.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.nonempty_arrowPolarization {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) : Nonempty P.ArrowPolarization

Every special-biserial presentation admits Butler--Ringel arrow signs. The choice is noncanonical, as in the source.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.arrowPolarization {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) : P.ArrowPolarization

A fixed noncanonical Butler--Ringel polarization of a special-biserial presentation.

def MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSourceSign {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} (S : P.ArrowPolarization) {x y : Q} (e : SignedArrow x y) : Bool

Butler--Ringel's source sign of a signed arrow. Formal inversion swaps the source and target signs of the underlying ordinary arrow.

def MagnitudeConjecture.BoundQuiver.StringWord.signedArrowTargetSign {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} (S : P.ArrowPolarization) {x y : Q} (e : SignedArrow x y) : Bool

Butler--Ringel's target sign of a signed arrow.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSourceSign_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} (S : P.ArrowPolarization) {x y : Q} (a : x ⟶ y) : signedArrowSourceSign S (positiveArrow a) = S.sourceSign a

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSourceSign_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} (S : P.ArrowPolarization) {x y : Q} (a : x ⟶ y) : signedArrowSourceSign S (negativeArrow a) = S.targetSign a

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowTargetSign_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} (S : P.ArrowPolarization) {x y : Q} (a : x ⟶ y) : signedArrowTargetSign S (positiveArrow a) = S.targetSign a

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowTargetSign_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} (S : P.ArrowPolarization) {x y : Q} (a : x ⟶ y) : signedArrowTargetSign S (negativeArrow a) = S.sourceSign a

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowTargetSign_reverse {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} (S : P.ArrowPolarization) {x y : Q} (e : SignedArrow x y) : signedArrowTargetSign S (Quiver.reverse e) = signedArrowSourceSign S e

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSourceSign_reverse {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} (S : P.ArrowPolarization) {x y : Q} (e : SignedArrow x y) : signedArrowSourceSign S (Quiver.reverse e) = signedArrowTargetSign S e

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSourceSign_eq_not_targetSign_of_isString {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} (S : P.ArrowPolarization) {x y z : Q} (e : SignedArrow x y) (f : SignedArrow y z) (hstring : IsString P.relations ((Quiver.Hom.toPath e).comp (Quiver.Hom.toPath f))) : signedArrowSourceSign S f = !signedArrowTargetSign S e

Consecutive letters of a string have opposite Butler--Ringel signs at their common vertex. For equally oriented letters this is the polarization condition on a surviving ordinary two-arrow path. For oppositely oriented letters, reducedness and injectivity of the relevant endpoint signs give the same conclusion.

def MagnitudeConjecture.BoundQuiver.StringWord.signedPathTargetSign {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} (S : P.ArrowPolarization) {x y : Q} : SignedPath x y → Option Bool

Target sign of a nonempty signed path. The empty path has no intrinsic sign; its two Butler--Ringel polarizations are supplied separately below.

def MagnitudeConjecture.BoundQuiver.StringWord.signedPathSourceSign {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} (S : P.ArrowPolarization) {x y : Q} (p : SignedPath x y) : Option Bool

Source sign of a nonempty signed path, defined as the target sign of its formal inverse.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathTargetSign_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} (S : P.ArrowPolarization) (x : Q) : signedPathTargetSign S Quiver.Path.nil = none

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathTargetSign_cons {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} (S : P.ArrowPolarization) {x y z : Q} (p : SignedPath x y) (e : SignedArrow y z) : signedPathTargetSign S (Quiver.Path.cons p e) = some (signedArrowTargetSign S e)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSourceSign_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} (S : P.ArrowPolarization) (x : Q) : signedPathSourceSign S Quiver.Path.nil = none

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathTargetSign_reverse {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} (S : P.ArrowPolarization) {x y : Q} (p : SignedPath x y) : signedPathTargetSign S (Quiver.Path.reverse p) = signedPathSourceSign S p

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSourceSign_reverse {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} (S : P.ArrowPolarization) {x y : Q} (p : SignedPath x y) : signedPathSourceSign S (Quiver.Path.reverse p) = signedPathTargetSign S p

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSourceSign_toPath_comp {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} (S : P.ArrowPolarization) {x y z : Q} (e : SignedArrow x y) (p : SignedPath y z) : signedPathSourceSign S ((Quiver.Hom.toPath e).comp p) = some (signedArrowSourceSign S e)

The source sign of a path displayed as its first letter followed by a tail is the source sign of that first letter.

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSourceSign_eq_not_targetSign_of_isString_prepend {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} (S : P.ArrowPolarization) {x y z : Q} (e : SignedArrow x y) (p : SignedPath y z) (hp : 0 < Quiver.Path.length p) (hstring : IsString P.relations ((Quiver.Hom.toPath e).comp p)) : signedPathSourceSign S p = some !signedArrowTargetSign S e

If a letter is prefixed to a nonempty string, its target sign is opposite to the intrinsic source sign of that string.

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathTargetSign_eq_not_sourceSign_of_isString_append {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} (S : P.ArrowPolarization) {x y z : Q} (p : SignedPath x y) (e : SignedArrow y z) (hp : 0 < Quiver.Path.length p) (hstring : IsString P.relations (Quiver.Path.comp p (Quiver.Hom.toPath e))) : signedPathTargetSign S p = some !signedArrowSourceSign S e

Dually, if a letter is appended to a nonempty string, its source sign is opposite to the intrinsic target sign of that string.

def MagnitudeConjecture.BoundQuiver.StringWord.signedPathTargetSignOr {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} (S : P.ArrowPolarization) (t : Bool) {x y : Q} (p : SignedPath x y) : Bool

The target sign of a path, using t for the empty path.

def MagnitudeConjecture.BoundQuiver.StringWord.signedPathSourceSignOr {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} (S : P.ArrowPolarization) (t : Bool) {x y : Q} (p : SignedPath x y) : Bool

The source sign of a path, using t for the empty path.

structure MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord {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} (S : P.ArrowPolarization) (u : Q) (t : Bool) : Type u

Butler--Ringel's W(u,t): a string ending at u with target sign t. For a length-zero word, t chooses one of the two formal trivial strings; for a nonempty word, its last signed arrow determines t.

• source : Q
• path : SignedPath self.source u
• isString : IsString P.relations self.path
• targetSign_eq : signedPathTargetSignOr S t self.path = t

def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.word {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} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C : EndpointWord S u t) : Word P.relations

Forget the endpoint polarization and recover the underlying string word.

def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.sourceSign {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} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C : EndpointWord S u t) : Bool

Butler--Ringel's source sign. For the trivial word 1_(u,t) it is not t; otherwise it is the sign of the first signed arrow.

def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.vertex {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) (S : P.ArrowPolarization) (u : Q) (t : Bool) : EndpointWord S u t

The two formal length-zero strings at a vertex.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.vertex_sourceSign {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) (S : P.ArrowPolarization) (u : Q) (t : Bool) : (vertex P S u t).sourceSign = !t