Pair detectors as contextual complete-word detectors #
For a nontrivial valid pair of oppositely polarized endpoint words, the matching trivial outer boundaries identify the raw pair detector at the join with the contextual detector of the complete pair word. Change of split then identifies it naturally with the canonical detector of that complete word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightLower_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(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))
:
splitRightLower N S (L.pairWord R hstring) (Word.Split.ofPosition (L.pairWord R hstring) (L.pairPosition R hstring)) = lowerSubspace N R
At the join of a nontrivial complete pair word, the contextual right lower space is exactly the raw lower space of the right half.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightUpper_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(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))
:
splitRightUpper N S (L.pairWord R hstring) (Word.Split.ofPosition (L.pairWord R hstring) (L.pairPosition R hstring)) = upperSubspace N R
The analogous right upper-space identification.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftLower_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(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))
:
splitLeftLower N S (L.pairWord R hstring) (Word.Split.ofPosition (L.pairWord R hstring) (L.pairPosition R hstring)) = lowerSubspace N L
At the same join, the contextual left lower space is exactly the raw lower space of the left half.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftUpper_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(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))
:
splitLeftUpper N S (L.pairWord R hstring) (Word.Split.ofPosition (L.pairWord R hstring) (L.pairPosition R hstring)) = upperSubspace N L
The analogous left upper-space identification.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorNumerator_eq_splitDetectorNumerator_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(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))
:
pairDetectorNumerator N L R = splitDetectorNumerator N S (L.pairWord R hstring)
(Word.Split.ofPosition (L.pairWord R hstring) (L.pairPosition R hstring))
The raw pair numerator is the contextual numerator at the displayed join.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorDenominator_eq_splitDetectorDenominator_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(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))
:
pairDetectorDenominator N L R = splitDetectorDenominator N S (L.pairWord R hstring)
(Word.Split.ofPosition (L.pairWord R hstring) (L.pairPosition R hstring))
The raw pair denominator is likewise the contextual denominator at the join.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorSplitEquiv
{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)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
(hlength : 0 < Word.length P.relations (L.pairWord R hstring))
:
PairDetectorSpace N L R ≃ₗ[k] SplitDetectorSpace N S (L.pairWord R hstring)
(Word.Split.ofPosition (L.pairWord R hstring) (L.pairPosition R hstring))
Canonical identification of a nontrivial raw pair detector with the contextual detector at its join.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorSplitEquiv_mk
{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)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
(hlength : 0 < Word.length P.relations (L.pairWord R hstring))
(x : ↥(pairDetectorNumerator N L R))
:
(pairDetectorSplitEquiv N L R hstring hlength) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨↑x, ⋯⟩
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorCompleteWordEquiv
{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)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
(hlength : 0 < Word.length P.relations (L.pairWord R hstring))
:
PairDetectorSpace N L R ≃ₗ[k] DetectorSpace N (detectorEndpoint S (L.pairWord R hstring))
A nontrivial valid pair detector is naturally the canonical detector of its complete pair word.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorSplitEquiv_naturality
{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}
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(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))
(q : PairDetectorSpace M L R)
:
(pairDetectorSplitEquiv N L R hstring hlength) ((pairDetectorLinearMap f L R) q) = (splitDetectorLinearMap f S (L.pairWord R hstring)
(Word.Split.ofPosition (L.pairWord R hstring) (L.pairPosition R hstring)))
((pairDetectorSplitEquiv M L R hstring hlength) q)
The join identification commutes with every module morphism.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorCompleteWordEquiv_naturality
{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}
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(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))
(q : PairDetectorSpace M L R)
:
(pairDetectorCompleteWordEquiv N L R hstring hlength) ((pairDetectorLinearMap f L R) q) = (detectorLinearMap f (detectorEndpoint S (L.pairWord R hstring)))
((pairDetectorCompleteWordEquiv M L R hstring hlength) q)
The complete-word equivalence is natural in the represented module.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorRightEquiv_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}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(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 : Word.length P.relations (L.pairWord R hstring) = 0)
:
PairDetectorSpace N L R ≃ₗ[k] DetectorSpace N R
If a valid pair has total length zero, its left half is the opposite polarized trivial word of its right half. Thus its pair detector is already the ordinary detector of the right endpoint word.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorRightEquiv_of_length_zero_naturality
{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}
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
(f : M ⟶ N)
(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 : Word.length P.relations (L.pairWord R hstring) = 0)
(q : PairDetectorSpace M L R)
:
(pairDetectorRightEquiv_of_length_zero N L R hstring hlength) ((pairDetectorLinearMap f L R) q) = (detectorLinearMap f R) ((pairDetectorRightEquiv_of_length_zero M L R hstring hlength) q)
The direct identification of a zero-length pair with its right detector is natural in the represented module.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorLinearMap_bijective_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}
{u₀ : Q}
{t : Bool}
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(hdetector : ∀ {v : Q} {s : Bool} (C : EndpointWord S v s), Function.Bijective ⇑(detectorLinearMap f C))
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(hstring : IsString P.relations (Quiver.Path.comp R.path (Quiver.Path.reverse L.path)))
:
Function.Bijective ⇑(pairDetectorLinearMap f L R)
A valid pair-detector map is bijective whenever every ordinary endpoint detector map is bijective. Nontrivial pairs use the complete pair word; the sole length-zero case uses the right endpoint word directly.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorLinearMap_bijective
{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}
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(hdetector : ∀ {v : Q} {s : Bool} (C : EndpointWord S v s), Function.Bijective ⇑(detectorLinearMap f C))
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
:
Function.Bijective ⇑(pairDetectorLinearMap f L R)
Every pair-detector map is bijective under endpoint-detector bijectivity: valid joins reduce to an ordinary detector, while invalid joins have zero source and target quotients.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridLinearMap_bijective
{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}
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(hdetector : ∀ {v : Q} {s : Bool} (C : EndpointWord S v s), Function.Bijective ⇑(detectorLinearMap f C))
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
:
Function.Bijective ⇑(pairGridLinearMap f L R)
Every map on a lexicographic grid layer is bijective under ordinary endpoint-detector bijectivity.
@[reducible, inline]
abbrev
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.OrderedGridLayerSpace
{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]
(i : Fin (Nat.card (GridWordIndex S u₀ t)))
:
Type u
One successive quotient of the ordered grid filtration, before its identification with the corresponding pair-grid quotient.
Instances For
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridLayerEquiv
{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]
(i : Fin (Nat.card (GridWordIndex S u₀ t)))
:
OrderedGridLayerSpace N i ≃ₗ[k] PairGridSpace N (orderedGridWord i).1 (orderedGridWord i).2
The ith ordered-filtration quotient is canonically its literal
pair-grid quotient.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridLayerEquiv_mk
{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]
(i : Fin (Nat.card (GridWordIndex S u₀ t)))
(x : ↥((orderedGridFiltration N).subspace i.succ))
:
(orderedGridLayerEquiv N i) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨↑x, ⋯⟩
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridLayerEquiv_naturality
{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)]
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(i : Fin (Nat.card (GridWordIndex S u₀ t)))
(q : OrderedGridLayerSpace M i)
:
(orderedGridLayerEquiv N i)
((LinearAlgebra.FiniteFiltration.Filtration.gradedMap (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations u₀))))
(orderedGridFiltration M) (orderedGridFiltration N) ⋯ i)
q) = (pairGridLinearMap f (orderedGridWord i).1 (orderedGridWord i).2) ((orderedGridLayerEquiv M i) q)
The ordered-layer identification commutes with every module morphism.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridFiltration_gradedMap_bijective
{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)]
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(hdetector : ∀ {v : Q} {s : Bool} (C : EndpointWord S v s), Function.Bijective ⇑(detectorLinearMap f C))
(i : Fin (Nat.card (GridWordIndex S u₀ t)))
:
Function.Bijective
⇑(LinearAlgebra.FiniteFiltration.Filtration.gradedMap (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations u₀))))
(orderedGridFiltration M) (orderedGridFiltration N) ⋯ i)
Every successive map in the ordered grid filtration is bijective under ordinary endpoint-detector bijectivity.