Extending endpoint-polarized detector words #
The ordered-word filtration grows a word at its source endpoint. This file packages its two legal one-letter extensions: a compatible incoming arrow is prefixed positively, while a compatible outgoing arrow is prefixed with its formal inverse. Both operations preserve the target polarization and increase word length strictly.
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeSigns
{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)
:
List Bool
The signs of a word read from its fixed target back toward its source. Source extension appends one Boolean to this list.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeSigns_length
{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)
:
C.routeSigns.length = Word.length P.relations C.word
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.prependIncoming
{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)
(inc : C.IncomingExtension)
:
EndpointWord S u t
Prefix the compatible incoming ordinary arrow to an endpoint word.
Instances For
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.prependOutgoingInverse
{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)
(out : C.OutgoingInverseExtension)
:
EndpointWord S u t
Prefix the formal inverse of the compatible outgoing ordinary arrow to an endpoint word.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.prependIncoming_path
{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)
(inc : C.IncomingExtension)
:
(C.prependIncoming inc).path = (Quiver.Hom.toPath (positiveArrow (↑inc).snd)).comp C.path
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.prependOutgoingInverse_path
{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)
(out : C.OutgoingInverseExtension)
:
(C.prependOutgoingInverse out).path = (Quiver.Hom.toPath (negativeArrow (↑out).snd)).comp C.path
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.prependIncoming_length
{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)
(inc : C.IncomingExtension)
:
Word.length P.relations (C.prependIncoming inc).word = Word.length P.relations C.word + 1
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.prependOutgoingInverse_length
{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)
(out : C.OutgoingInverseExtension)
:
Word.length P.relations (C.prependOutgoingInverse out).word = Word.length P.relations C.word + 1
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeSigns_prependIncoming
{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)
(inc : C.IncomingExtension)
:
(C.prependIncoming inc).routeSigns = C.routeSigns ++ [false]
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeSigns_prependOutgoingInverse
{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)
(out : C.OutgoingInverseExtension)
:
(C.prependOutgoingInverse out).routeSigns = C.routeSigns ++ [true]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.prependIncoming_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}
{u : Q}
{t : Bool}
(C : EndpointWord S u t)
(inc : C.IncomingExtension)
:
C.prependIncoming inc ≠ C
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.prependOutgoingInverse_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}
{u : Q}
{t : Bool}
(C : EndpointWord S u t)
(out : C.OutgoingInverseExtension)
:
C.prependOutgoingInverse out ≠ C
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.prependIncoming_upperSubspace_le_lowerSubspace
{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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C : EndpointWord S u t)
(inc : C.IncomingExtension)
:
upperSubspace N (C.prependIncoming inc) ≤ lowerSubspace N C
The interval of a positive source extension lies entirely below the lower endpoint of its parent interval.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_le_prependOutgoingInverse_lowerSubspace
{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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C : EndpointWord S u t)
(out : C.OutgoingInverseExtension)
:
upperSubspace N C ≤ lowerSubspace N (C.prependOutgoingInverse out)
The interval of a negative source extension lies entirely above the upper endpoint of its parent interval.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_le_lowerSubspace_of_sourcePrefix_prependIncoming
{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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C E : EndpointWord S u t)
(inc : C.IncomingExtension)
(pref : SignedPath E.source (↑inc).fst)
(hpath : E.path = Quiver.Path.comp pref ((Quiver.Hom.toPath (positiveArrow (↑inc).snd)).comp C.path))
:
upperSubspace N E ≤ lowerSubspace N C
Every word whose path reaches the positive source extension of C after
an arbitrary source prefix has its whole interval below C⁻.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_le_lowerSubspace_of_sourcePrefix_prependOutgoingInverse
{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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C E : EndpointWord S u t)
(out : C.OutgoingInverseExtension)
(pref : SignedPath E.source (↑out).fst)
(hpath : E.path = Quiver.Path.comp pref ((Quiver.Hom.toPath (negativeArrow (↑out).snd)).comp C.path))
:
upperSubspace N C ≤ lowerSubspace N E
Every word whose path reaches the inverse source extension of C after
an arbitrary source prefix has its whole interval above C⁺.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.exists_parent_extension
{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)
(hC : 0 < Word.length P.relations C.word)
:
(∃ (D : EndpointWord S u t) (inc : D.IncomingExtension), C = D.prependIncoming inc) ∨ ∃ (D : EndpointWord S u t) (out : D.OutgoingInverseExtension), C = D.prependOutgoingInverse out
Every nontrivial endpoint word is obtained, according to its first-letter sign, from a shorter endpoint word by one of the two source extensions.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.eq_vertex_of_word_length_eq_zero
{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)
(hC : Word.length P.relations C.word = 0)
:
C = vertex P S u t
An endpoint word of length zero is the fixed polarized vertex word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeSigns_injective
{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}
:
Function.Injective routeSigns
For fixed target and polarization, the signs read from target to source determine the whole endpoint word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.exists_sourcePrefix_of_routeSigns_eq_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}
{u : Q}
{t : Bool}
(C D : EndpointWord S u t)
(suffix : List Bool)
(hsigns : D.routeSigns = C.routeSigns ++ suffix)
:
∃ (pref : SignedPath D.source C.source), D.path = Quiver.Path.comp pref C.path ∧ signedPathSigns pref = suffix
If the route-sign word of C is an initial segment of that of D, then
the literal path of C is a target-side suffix of the literal path of D.
The extra source-side path is returned explicitly.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.exists_endpointWord_of_routeSigns_eq_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}
{u : Q}
{t : Bool}
(E : EndpointWord S u t)
(base suffix : List Bool)
(hsigns : E.routeSigns = base ++ suffix)
:
∃ (C : EndpointWord S u t) (pref : SignedPath E.source C.source),
C.routeSigns = base ∧ E.path = Quiver.Path.comp pref C.path ∧ signedPathSigns pref = suffix
Every initial segment of an endpoint word's route signs is itself realized by a target-side endpoint word, and the remaining signs come from the explicit source prefix.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_le_lowerSubspace_of_routeSigns_eq_append_false
{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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C E : EndpointWord S u t)
(tail : List Bool)
(hsigns : E.routeSigns = C.routeSigns ++ false :: tail)
:
upperSubspace N E ≤ lowerSubspace N C
Every endpoint word in the positive branch below C has its interval
below the lower endpoint of C.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_le_lowerSubspace_of_routeSigns_eq_append_true
{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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C E : EndpointWord S u t)
(tail : List Bool)
(hsigns : E.routeSigns = C.routeSigns ++ true :: tail)
:
upperSubspace N C ≤ lowerSubspace N E
Every endpoint word in the inverse branch above C has its interval
above the upper endpoint of C.