Complete words represented by endpoint-word pairs #
Ringel's finite grid is indexed by pairs of endpoint words with opposite polarizations. This file relates a nonzero pair layer to the complete string obtained by traversing the right word and then the inverse of the left word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_positivePath
{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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
{x y : Q}
(p : Quiver.Path x y)
(U : Submodule k ↑(N.obj (Opposite.op (obj P.relations x))))
:
signedPathSubspace N (positivePath p) U = Submodule.map (ModuleCat.Hom.hom (modulePathMap N p)) U
Transport along an ordinary positive path is direct image under the corresponding module path map.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_positivePath_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
{x y : Q}
(p : Quiver.Path x y)
(U : Submodule k ↑(N.obj (Opposite.op (obj P.relations y))))
:
signedPathSubspace N (Quiver.Path.reverse (positivePath p)) U = Submodule.comap (ModuleCat.Hom.hom (modulePathMap N p)) U
Transport along the inverse of an ordinary positive path is inverse image under the corresponding module path map.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_positivePath_le_reverse_of_pathMap_comp_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
{w x y : Q}
(p : Quiver.Path w x)
(q : Quiver.Path x y)
(U : Submodule k ↑(N.obj (Opposite.op (obj P.relations w))))
(V : Submodule k ↑(N.obj (Opposite.op (obj P.relations y))))
(hzero : pathMap P.relations (p.comp q) = 0)
:
signedPathSubspace N (positivePath p) U ≤ signedPathSubspace N (Quiver.Path.reverse (positivePath q)) V
The image transported along the first half of a zero ordinary path lies in the inverse image of every subspace along the second half.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_positivePath_comp_top_eq_bot_of_pathMap_comp_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
{w x y : Q}
(p : Quiver.Path w x)
(q : Quiver.Path x y)
(hzero : pathMap P.relations (p.comp q) = 0)
:
signedPathSubspace N (positivePath q) (signedPathSubspace N (positivePath p) ⊤) = ⊥
Transporting the whole space through two positive path pieces whose composite is a relation gives the zero subspace.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_positivePath_reverse_comap_bot_eq_top_of_pathMap_comp_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
{w x y : Q}
(p : Quiver.Path w x)
(q : Quiver.Path x y)
(hzero : pathMap P.relations (p.comp q) = 0)
:
signedPathSubspace N (Quiver.Path.reverse (positivePath p))
(Submodule.comap (ModuleCat.Hom.hom (modulePathMap N q)) ⊥) = ⊤
Dually, inverse transport through the first piece of a zero positive composite sends the kernel boundary of the second piece to the whole space.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.exists_positive_relation_crossing_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}
{a x b : Q}
(left : SignedPath a x)
(right : SignedPath x b)
(hleft : AvoidsRelations P.relations left)
(hright : AvoidsRelations P.relations right)
(hnot : ¬AvoidsRelations P.relations (Quiver.Path.comp left right))
:
∃ (c : Q) (d : Q) (p : Quiver.Path c x) (q : Quiver.Path x d) (before : SignedPath a c) (after : SignedPath d b),
left = Quiver.Path.comp before (positivePath p) ∧ right = Quiver.Path.comp (positivePath q) after ∧ 0 < p.length ∧ 0 < q.length ∧ pathMap P.relations (p.comp q) = 0
If relation avoidance fails only after two relation-avoiding signed paths are joined, a killed positive ordinary path crosses the join with a nonempty piece on each side.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathTargetSign_comp_of_right_length_pos
{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)
(q : SignedPath y z)
(hq : 0 < Quiver.Path.length q)
:
signedPathTargetSign S (Quiver.Path.comp p q) = signedPathTargetSign S q
Prefixing a path to a nonempty signed suffix does not change its intrinsic target sign.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathTargetSign_comp_of_right_length_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}
{x y z : Q}
(p : SignedPath x y)
(q : SignedPath y z)
(hq : Quiver.Path.length q = 0)
:
signedPathTargetSign S (Quiver.Path.comp p q) = signedPathTargetSign S p
A zero-length suffix contributes no target sign to a composite.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathSourceSign_comp_of_left_length_pos
{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)
(q : SignedPath y z)
(hp : 0 < Quiver.Path.length p)
:
signedPathSourceSign S (Quiver.Path.comp p q) = signedPathSourceSign S p
Appending a suffix to a nonempty signed path does not change its intrinsic source sign.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathSourceSign_comp_of_left_length_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}
{x y z : Q}
(p : SignedPath x y)
(q : SignedPath y z)
(hp : Quiver.Path.length p = 0)
:
signedPathSourceSign S (Quiver.Path.comp p q) = signedPathSourceSign S q
A zero-length prefix contributes no source sign to a composite.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathSourceSignOr_eq_of_length_pos
{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)
(hp : 0 < Quiver.Path.length p)
(a b : Bool)
:
signedPathSourceSignOr S a p = signedPathSourceSignOr S b p
Once a path is nonempty, the fallback Boolean in its source-sign convention is irrelevant.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathTargetSignOr_eq_of_length_pos
{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)
(hp : 0 < Quiver.Path.length p)
(a b : Bool)
:
signedPathTargetSignOr S a p = signedPathTargetSignOr S b p
Once a path is nonempty, the fallback Boolean in its target-sign convention is irrelevant.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathSourceSignOr_eq_of_length_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}
{x y : Q}
(p : SignedPath x y)
(hp : Quiver.Path.length p = 0)
(a : Bool)
:
signedPathSourceSignOr S a p = a
A zero-length path uses exactly its prescribed source-sign fallback.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathTargetSignOr_eq_of_length_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}
{x y : Q}
(p : SignedPath x y)
(hp : Quiver.Path.length p = 0)
(a : Bool)
:
signedPathTargetSignOr S a p = a
A zero-length path uses exactly its prescribed target-sign fallback.
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.sourceVertex
{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)
:
EndpointWord S C.source !C.sourceSign
The polarized trivial word at the source of an endpoint word whose source sign agrees with that word. Transporting its boundary filtration along the word is the contextual filtration coming from a trivial outer endpoint.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.sourceVertex_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)
:
C.sourceVertex.path = Quiver.Path.nil
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.sourceVertex_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)
:
C.sourceVertex.sourceSign = C.sourceSign
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.isReduced_positiveArrow_comp_of_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)
{v : Q}
(a : v ⟶ C.source)
(hsign : C.sourceSign = !S.targetSign a)
:
IsReduced ((Quiver.Hom.toPath (positiveArrow a)).comp C.path)
A positively oriented arrow with the boundary sign selected at the source
of C cannot cancel the first letter of C.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.isReduced_negativeArrow_comp_of_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)
{v : Q}
(a : C.source ⟶ v)
(hsign : C.sourceSign = !S.sourceSign a)
:
IsReduced ((Quiver.Hom.toPath (negativeArrow a)).comp C.path)
A formally inverse arrow with the inverse-boundary source sign likewise
cannot cancel the first letter of C.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.avoidsRelations_negativeArrow_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}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
{v : Q}
(a : C.source ⟶ v)
:
AvoidsRelations P.relations ((Quiver.Hom.toPath (negativeArrow a)).comp C.path)
A negative source extension has a negative outer boundary, so its forward
orientation inherits relation avoidance from C.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.not_avoidsRelations_reverse_negativeArrow_comp_of_not_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}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
{v : Q}
(a : C.source ⟶ v)
(hsign : C.sourceSign = !S.sourceSign a)
(hnot : ¬IsString P.relations ((Quiver.Hom.toPath (negativeArrow a)).comp C.path))
:
¬AvoidsRelations P.relations ((Quiver.Hom.toPath (negativeArrow a)).comp C.path).reverse
Therefore a sign-compatible inverse source extension which is not a string must fail by a monomial relation in the reversed orientation.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.avoidsRelations_reverse_positiveArrow_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}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
{v : Q}
(a : v ⟶ C.source)
:
AvoidsRelations P.relations ((Quiver.Hom.toPath (positiveArrow a)).comp C.path).reverse
Reversing a positive source extension places a negative arrow at the outer boundary, so no new positive relation can occur there.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.not_avoidsRelations_positiveArrow_comp_of_not_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}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
{v : Q}
(a : v ⟶ C.source)
(hsign : C.sourceSign = !S.targetSign a)
(hnot : ¬IsString P.relations ((Quiver.Hom.toPath (positiveArrow a)).comp C.path))
:
¬AvoidsRelations P.relations ((Quiver.Hom.toPath (positiveArrow a)).comp C.path)
Consequently, a sign-compatible positive source extension which is not a string must fail by a forward monomial relation.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathSubspace_map_top_eq_zeroSubspace_of_not_avoids_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}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(C : EndpointWord S u₀ t)
{v : Q}
(a : v ⟶ C.source)
(hnot : ¬AvoidsRelations P.relations ((Quiver.Hom.toPath (positiveArrow a)).comp C.path))
:
signedPathSubspace N C.path (Submodule.map (ModuleCat.Hom.hom (moduleArrowMap N a)) ⊤) = zeroSubspace N C
If a compatible positive source arrow fails only because a relation
appears after it is attached to C, transporting its image along C gives
exactly the transported zero space.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathSubspace_comap_bot_eq_wholeSubspace_of_not_avoids_reverse_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}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(C : EndpointWord S u₀ t)
{v : Q}
(a : C.source ⟶ v)
(hnot : ¬AvoidsRelations P.relations ((Quiver.Hom.toPath (negativeArrow a)).comp C.path).reverse)
:
signedPathSubspace N C.path (Submodule.comap (ModuleCat.Hom.hom (moduleArrowMap N a)) ⊥) = wholeSubspace N C
If a compatible inverse source arrow fails only because a relation
appears after reversal, transporting its kernel boundary along C gives
exactly the transported whole space.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_eq_sourceVertexBoundaryTransport
{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))
[N.Additive]
(C : EndpointWord S u₀ t)
:
lowerSubspace N C = signedPathSubspace N C.path (lowerBoundarySubspace N C.sourceVertex)
The lower filtration of an endpoint word may equivalently be obtained by starting with the matching polarized trivial word at its source and then transporting that boundary along the word. If the trivial boundary arrow no longer extends the word, the intervening monomial relation makes its transport equal to the transported zero space.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_eq_sourceVertexBoundaryTransport
{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))
[N.Additive]
(C : EndpointWord S u₀ t)
:
upperSubspace N C = signedPathSubspace N C.path (upperBoundarySubspace N C.sourceVertex)
The upper filtration has the same contextual description from the
matching polarized trivial source word. When its inverse boundary arrow no
longer extends C, the reversed monomial relation makes the transported
kernel equal the transported whole space.
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairWord
{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}
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
The complete signed string represented by a valid endpoint-word pair.
Instances For
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairPosition
{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}
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
The original join is a displayed position of the complete pair word.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairPosition_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}
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
(L.pairPosition R hstring).fst = u₀
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairPosition_prefix
{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}
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
↑(L.pairPosition R hstring).snd = R.path
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairPosition_suffix
{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}
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
(L.pairPosition R hstring).snd.suffix = Quiver.Path.reverse L.path
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorEndpoint_pairWord_sourceSign_of_length_pos
{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}
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
(hlength : 0 < Word.length P.relations (L.pairWord R hstring))
:
(ofWord S (L.pairWord R hstring)).sourceSign = R.sourceSign
For a nontrivial complete pair word, the canonical detector endpoint has the same source polarization as the right half.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorEndpoint_pairWord_oppositeVertex_sourceSign_of_length_pos
{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}
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
(hlength : 0 < Word.length P.relations (L.pairWord R hstring))
:
(ofWord S (L.pairWord R hstring)).oppositeVertex.sourceSign = L.sourceSign
For a nontrivial complete pair word, its opposite trivial endpoint has the same source polarization as the left half.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairPath_isReduced
{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}
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
:
Endpoint words of opposite target polarization cannot cancel when their target ends are joined.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_le_lowerSubspace_of_not_avoids_join
{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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
{s₁ s₂ : Bool}
(C : EndpointWord S u₀ s₁)
(D : EndpointWord S u₀ s₂)
(hnot : ¬AvoidsRelations P.relations (Quiver.Path.comp C.path (Quiver.Path.reverse D.path)))
:
upperSubspace N C ≤ lowerSubspace N D
If an ordinary monomial relation first appears across the join of two endpoint words, the upper subspace of the first word is already contained in the lower subspace of the second.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_descendant_le_lowerSubspace_of_not_avoids_join
{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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
{s₁ s₂ : Bool}
(C : EndpointWord S u₀ s₁)
(D : EndpointWord S u₀ s₂)
(E : EndpointWord S u₀ s₁)
(pref : SignedPath E.source C.source)
(hpath : E.path = Quiver.Path.comp pref C.path)
(hnot : ¬AvoidsRelations P.relations (Quiver.Path.comp C.path (Quiver.Path.reverse D.path)))
:
upperSubspace N E ≤ lowerSubspace N D
A forward relation already crossing a join continues to cross after an arbitrary source extension of its left word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.wholeSubspace_le_zeroSubspace_sup_lowerSubspace_of_not_avoids_join
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
{s₁ s₂ : Bool}
(C : EndpointWord S u₀ s₁)
(D : EndpointWord S u₀ s₂)
(hnot : ¬AvoidsRelations P.relations (Quiver.Path.comp C.path (Quiver.Path.reverse D.path)))
:
wholeSubspace N C ≤ zeroSubspace N C ⊔ lowerSubspace N D
If a forward relation crosses the join after C, every vector in the
transported whole space of C is either already in its transported zero
space or lies in the lower subspace of the opposite word. This packages the
collapse of the entire finite source-extension subtree, not just its first
interval.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_le_zeroSubspace_of_not_avoids_join
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
{s₁ s₂ : Bool}
(C : EndpointWord S u₀ s₁)
(D : EndpointWord S u₀ s₂)
(hnot : ¬AvoidsRelations P.relations (Quiver.Path.comp C.path (Quiver.Path.reverse D.path)))
:
upperSubspace N C ≤ zeroSubspace N D
In the finite-word case, a relation crossing the join forces the first word's upper subspace all the way into the transported zero space of the second word. Otherwise descendant coverage of the second word would produce an interval simultaneously above and below the same vector.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_right_le_zeroSubspace_sup_lowerSubspace_left_of_not_avoids
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(inc : R.IncomingExtension)
(hnot : ¬AvoidsRelations P.relations (Quiver.Path.comp (R.prependIncoming inc).path (Quiver.Path.reverse L.path)))
:
lowerSubspace N R ≤ zeroSubspace N R ⊔ lowerSubspace N L
If the positive source extension defining R⁻ ceases to avoid relations
after the left half is attached, its contribution is already accounted for
by the transported zero space of R together with L⁻.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_left_le_zeroSubspace_sup_lowerSubspace_right_of_not_avoids
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(inc : L.IncomingExtension)
(hnot : ¬AvoidsRelations P.relations (Quiver.Path.comp (L.prependIncoming inc).path (Quiver.Path.reverse R.path)))
:
lowerSubspace N L ≤ zeroSubspace N L ⊔ lowerSubspace N R
The symmetric collapse for a positive source extension of the left half. It is the reverse-orientation boundary correction used at the other end of a complete pair word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_left_le_upperSubspace_right_of_not_avoids_outgoing
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(out : R.OutgoingInverseExtension)
(hnot :
¬AvoidsRelations P.relations (Quiver.Path.comp L.path (Quiver.Path.reverse (R.prependOutgoingInverse out).path)))
:
upperSubspace N L ≤ upperSubspace N R
If an inverse source extension of the right half ceases to avoid relations in the reverse orientation after the left half is attached, the left upper subspace is already contained in the old right upper subspace.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_right_le_upperSubspace_left_of_not_avoids_outgoing
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(out : L.OutgoingInverseExtension)
(hnot :
¬AvoidsRelations P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse (L.prependOutgoingInverse out).path)))
:
upperSubspace N R ≤ upperSubspace N L
The symmetric inverse-extension correction at the left half.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_right_le_lowerSubspace_left_of_not_avoids_pairPath
{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))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hnot : ¬AvoidsRelations P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
upperSubspace N R ≤ lowerSubspace N L
A forward relation crossing the pair join kills the right upper word subspace modulo the left lower word subspace.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_left_le_lowerSubspace_right_of_not_avoids_reverse_pairPath
{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))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hnot : ¬AvoidsRelations P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)).reverse)
:
upperSubspace N L ≤ lowerSubspace N R
A relation crossing the reverse of the pair join kills the left upper word subspace modulo the right lower word subspace.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.not_avoids_pairPath_or_reverse_of_not_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}
{u₀ : Q}
{t : Bool}
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hnot : ¬IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
¬AvoidsRelations P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)) ∨ ¬AvoidsRelations P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)).reverse
Since opposite polarization already makes the join reduced, failure of the pair join to be a string is exactly a relation failure in one of its two orientations.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorNumerator_le_pairDetectorDenominator_of_not_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}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hnot : ¬IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
pairDetectorNumerator N L R ≤ pairDetectorDenominator N L R
An invalid endpoint-word pair has zero pair detector: its numerator is already contained in its denominator.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorDenominator_eq_numerator_of_not_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}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hnot : ¬IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
pairDetectorDenominator N L R = pairDetectorNumerator N L R
Equivalently, the numerator and denominator of an invalid pair detector coincide.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridLower_eq_pairGridUpper_of_not_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}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hnot : ¬IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
pairGridLower N L R = pairGridUpper N L R
In Ringel's finite grid, an invalid pair is literally a repeated filtration endpoint.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorSpace_subsingleton_of_not_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}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hnot : ¬IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
Subsingleton (PairDetectorSpace N L R)
The pair-detector quotient of an invalid pair is a zero vector space.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridSpace_subsingleton_of_not_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}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hnot : ¬IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
Subsingleton (PairGridSpace N L R)
The corresponding grid quotient is likewise a zero vector space.