Off-diagonal evaluation of finite-string detectors #
A basis coordinate which survives a finite-string detector traces a complete occurrence of the detector word in the evaluated literal string. The two boundary filters make that occurrence maximal at both ends. It is therefore the whole evaluated word, in the forward or reverse direction, and detectors attached to distinct inversion classes vanish.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.isString_prepend_of_prefix_eq
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
(D : Word P.relations)
{x y z : Q}
(e : SignedArrow x y)
(p : SignedPath y z)
(previous : D.PositionAt x)
(first : D.PositionAt y)
(last : D.PositionAt z)
(hprevious : ↑first = Quiver.Path.comp (↑previous) (Quiver.Hom.toPath e))
(hsegment : ↑last = Quiver.Path.comp (↑first) p)
:
A displayed predecessor followed by a realized path segment is itself a contiguous string segment of the ambient literal word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.isString_append_of_prefix_eq
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
(D : Word P.relations)
{x y z : Q}
(p : SignedPath x y)
(e : SignedArrow y z)
(first : D.PositionAt x)
(last : D.PositionAt y)
(next : D.PositionAt z)
(hsegment : ↑last = Quiver.Path.comp (↑first) p)
(hnext : ↑next = Quiver.Path.comp (↑last) (Quiver.Hom.toPath e))
:
A realized path segment followed by a displayed successor is itself a contiguous string segment of the ambient literal word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.eq_of_full_forward_segment
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
(C D : Word P.relations)
(first : D.PositionAt C.source)
(last : D.PositionAt C.target)
(hsegment : ↑last = Quiver.Path.comp (↑first) C.path)
(hfirst : first.index = 0)
(hlast : last.index = length P.relations D)
:
D = C
A forward segment beginning and ending at the two ambient boundary indices is the whole ambient word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.eq_reverse_of_full_reverse_segment
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
(C D : Word P.relations)
(first : D.PositionAt C.target)
(last : D.PositionAt C.source)
(hsegment : ↑last = Quiver.Path.comp (↑first) (Quiver.Path.reverse C.path))
(hfirst : first.index = 0)
(hlast : last.index = length P.relations D)
:
A reverse segment beginning and ending at the two ambient boundary indices is the whole ambient word in the reverse orientation.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.eq_vertex_of_path_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 : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
(hC : Quiver.Path.length C.path = 0)
:
C = vertex P.toSpecialBiserialPresentation S u₀ t
An endpoint word of length zero is the corresponding formal polarized vertex word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.single_mem_lowerBoundarySubspace_of_incomingExtension_step
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(D : Word P.relations)
(C : EndpointWord S u₀ t)
(inc : C.IncomingExtension)
(i : D.PositionAt (↑inc).fst)
(j : D.PositionAt C.source)
(hstep : D.ArrowStep (↑inc).snd i j)
:
Finsupp.single j 1 ∈ lowerBoundarySubspace (D.rightModule ⋯) C
An actual incoming step selected by the lower boundary puts its target basis vector in that boundary image.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.single_not_mem_upperBoundarySubspace_of_outgoingInverseExtension_step
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(D : Word P.relations)
(C : EndpointWord S u₀ t)
(out : C.OutgoingInverseExtension)
(i : D.PositionAt C.source)
(j : D.PositionAt (↑out).fst)
(hstep : D.ArrowStep (↑out).snd i j)
:
Finsupp.single i 1 ∉ upperBoundarySubspace (D.rightModule ⋯) C
An actual outgoing step selected by the upper boundary prevents its source basis vector from lying in that boundary kernel.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.forwardOccurrence_sourceIndex_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 : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(D : Word P.relations)
(C : EndpointWord S u₀ t)
(hC : 0 < Quiver.Path.length C.path)
(first : D.PositionAt C.source)
(last : D.PositionAt u₀)
(hsegment : ↑last = Quiver.Path.comp (↑first) C.path)
(hupper : Finsupp.single first 1 ∈ upperBoundarySubspace (D.rightModule ⋯) C)
(hnotLower : Finsupp.single first 1 ∉ lowerBoundarySubspace (D.rightModule ⋯) C)
:
first.index = 0
At the forward start of a nonempty occurrence, surviving the lower and upper source-boundary filters forces the occurrence to begin at index zero of the ambient literal string.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.forwardOccurrence_targetIndex_eq_length
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(D : Word P.relations)
(C : EndpointWord S u₀ t)
(hC : 0 < Quiver.Path.length C.path)
(first : D.PositionAt C.source)
(last : D.PositionAt u₀)
(hsegment : ↑last = Quiver.Path.comp (↑first) C.path)
(hupper : Finsupp.single last 1 ∈ upperBoundarySubspace (D.rightModule ⋯) C.oppositeVertex)
(hnotLower : Finsupp.single last 1 ∉ lowerBoundarySubspace (D.rightModule ⋯) C.oppositeVertex)
:
last.index = Word.length P.relations D
At the forward end of a nonempty occurrence, the opposite trivial boundary filters force the occurrence to end at the final ambient index.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.reverseOccurrence_targetIndex_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 : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(D : Word P.relations)
(C : EndpointWord S u₀ t)
(hC : 0 < Quiver.Path.length C.path)
(first : D.PositionAt u₀)
(last : D.PositionAt C.source)
(hsegment : ↑last = Quiver.Path.comp (↑first) (Quiver.Path.reverse C.path))
(hupper : Finsupp.single first 1 ∈ upperBoundarySubspace (D.rightModule ⋯) C.oppositeVertex)
(hnotLower : Finsupp.single first 1 ∉ lowerBoundarySubspace (D.rightModule ⋯) C.oppositeVertex)
:
first.index = 0
At the start of a reverse occurrence, the opposite trivial boundary filters force the occurrence to begin at the initial ambient index.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.reverseOccurrence_sourceIndex_eq_length
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(D : Word P.relations)
(C : EndpointWord S u₀ t)
(hC : 0 < Quiver.Path.length C.path)
(first : D.PositionAt u₀)
(last : D.PositionAt C.source)
(hsegment : ↑last = Quiver.Path.comp (↑first) (Quiver.Path.reverse C.path))
(hupper : Finsupp.single last 1 ∈ upperBoundarySubspace (D.rightModule ⋯) C)
(hnotLower : Finsupp.single last 1 ∉ lowerBoundarySubspace (D.rightModule ⋯) C)
:
last.index = Word.length P.relations D
At the end of a reverse occurrence, the source-boundary filters of the original endpoint word force the occurrence to end at the final ambient index.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.trivialPair_index_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 : StringPresentation k A Q}
{S : P.ArrowPolarization}
(D : Word P.relations)
(u : Q)
(s : Bool)
(i : D.PositionAt u)
(hupper : Finsupp.single i 1 ∈ upperBoundarySubspace (D.rightModule ⋯) (vertex P.toSpecialBiserialPresentation S u s))
(hupperOpposite :
Finsupp.single i 1 ∈ upperBoundarySubspace (D.rightModule ⋯) (vertex P.toSpecialBiserialPresentation S u !s))
(hnotLower :
Finsupp.single i 1 ∉ lowerBoundarySubspace (D.rightModule ⋯) (vertex P.toSpecialBiserialPresentation S u s))
(hnotLowerOpposite :
Finsupp.single i 1 ∉ lowerBoundarySubspace (D.rightModule ⋯) (vertex P.toSpecialBiserialPresentation S u !s))
:
i.index = 0
For a formal vertex word and its opposite polarization, surviving both upper filters and neither lower filter forces the selected position to be the initial position of the ambient word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.trivialPair_index_eq_length
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
(D : Word P.relations)
(u : Q)
(s : Bool)
(i : D.PositionAt u)
(hupper : Finsupp.single i 1 ∈ upperBoundarySubspace (D.rightModule ⋯) (vertex P.toSpecialBiserialPresentation S u s))
(hupperOpposite :
Finsupp.single i 1 ∈ upperBoundarySubspace (D.rightModule ⋯) (vertex P.toSpecialBiserialPresentation S u !s))
(hnotLower :
Finsupp.single i 1 ∉ lowerBoundarySubspace (D.rightModule ⋯) (vertex P.toSpecialBiserialPresentation S u s))
(hnotLowerOpposite :
Finsupp.single i 1 ∉ lowerBoundarySubspace (D.rightModule ⋯) (vertex P.toSpecialBiserialPresentation S u !s))
:
i.index = Word.length P.relations D
The same two polarized trivial filters force a surviving position to be the final position of the ambient word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.word_eq_or_eq_reverse_of_single_mem_detectorNumerator_not_denominator
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
(D : Word P.relations)
(i : D.PositionAt u₀)
(hnum : Finsupp.single i 1 ∈ detectorNumerator (D.rightModule ⋯) C)
(hnotDen : Finsupp.single i 1 ∉ detectorDenominator (D.rightModule ⋯) C)
:
C.word = D ∨ C.word = Word.reverse P.relations D
If one position basis vector survives the detector indexed by C on a
literal string module M(D), then D is the word of C or its formal
reverse.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.single_mem_detectorDenominator_of_not_inverseEquivalent
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
(D : Word P.relations)
(hnot : ¬(C.word = D ∨ C.word = Word.reverse P.relations D))
(i : D.PositionAt u₀)
(hnum : Finsupp.single i 1 ∈ detectorNumerator (D.rightModule ⋯) C)
:
Finsupp.single i 1 ∈ detectorDenominator (D.rightModule ⋯) C
Away from the inversion class of C, every numerator basis coordinate
already belongs to the detector denominator.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorDenominator_eq_detectorNumerator_of_not_inverseEquivalent
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
(D : Word P.relations)
(hnot : ¬(C.word = D ∨ C.word = Word.reverse P.relations D))
:
detectorDenominator (D.rightModule ⋯) C = detectorNumerator (D.rightModule ⋯) C
On a literal string outside the inversion class of C, the detector
denominator equals its numerator.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorDenominatorInNumerator_eq_top_of_not_inverseEquivalent
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
(D : Word P.relations)
(hnot : ¬(C.word = D ∨ C.word = Word.reverse P.relations D))
:
detectorDenominatorInNumerator (D.rightModule ⋯) C = ⊤
Off the inversion class of C, the denominator inside the numerator is
the whole numerator.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorSpace_subsingleton_of_not_inverseEquivalent
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
(D : Word P.relations)
(hnot : ¬(C.word = D ∨ C.word = Word.reverse P.relations D))
:
Subsingleton (DetectorSpace (D.rightModule ⋯) C)
Every off-diagonal finite-string detector space is subsingleton.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.finrank_detectorSpace_rightModule_eq_zero_of_not_inverseEquivalent
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(C : EndpointWord S u₀ t)
(D : Word P.relations)
(hnot : ¬(C.word = D ∨ C.word = Word.reverse P.relations D))
:
Module.finrank k (DetectorSpace (D.rightModule ⋯) C) = 0
Literal dimension statement for off-diagonal detector evaluation.
@[instance_reducible]
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.instDecidableEq
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
:
DecidableEq (DetectorIndex S)
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finrank_detectorSpace_rightModule_endpointWord
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
(i j : DetectorIndex S)
:
Module.finrank k (EndpointWord.DetectorSpace (j.endpointWord.word.rightModule ⋯) i.endpointWord) = if i = j then 1 else 0
The chosen finite-string detectors evaluate on the chosen literal string modules as a Kronecker delta: dimension one on the matching inversion class and zero on every other class.