Reversal invariance of finite-string detectors #
The finite detector index identifies a string with its formal reverse. This file constructs the corresponding natural linear equivalence of detector spaces. The proof uses the already formalized change-of-split theorem: at the source end of a nontrivial word, the complete-word detector is the swapped pair presentation of the detector of the reversed word.
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.doubleNotTarget
{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 u₀ !!t
View an endpoint word through the canonical double-negation equality of its target polarization.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.doubleNotTarget_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)
:
C.doubleNotTarget.word = C.word
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.doubleNotTarget_source
{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.doubleNotTarget.source = C.source
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_doubleNotTarget
{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)
:
upperSubspace N C.doubleNotTarget = upperSubspace N C
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_doubleNotTarget
{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)
:
lowerSubspace N C.doubleNotTarget = lowerSubspace N C
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorPairSwapEquiv
{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)
:
PairDetectorSpace N C.doubleNotTarget C.oppositeVertex ≃ₗ[k] DetectorSpace N C
The swapped pair presentation at the far endpoint is the detector of the nontrivial half.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorPairSwapEquiv_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))
(C : EndpointWord S u₀ t)
(x : ↥(pairDetectorNumerator N C.doubleNotTarget C.oppositeVertex))
:
(detectorPairSwapEquiv N C) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨↑x, ⋯⟩
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorPairSwapEquiv_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)
(C : EndpointWord S u₀ t)
(q : PairDetectorSpace M C.doubleNotTarget C.oppositeVertex)
:
(detectorPairSwapEquiv N C) ((pairDetectorLinearMap f C.doubleNotTarget C.oppositeVertex) q) = (detectorLinearMap f C) ((detectorPairSwapEquiv M C) q)
Swapping the far-end pair presentation commutes with every module morphism.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorPairSwapEquiv_symm_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)
(C : EndpointWord S u₀ t)
(q : DetectorSpace M C)
:
(detectorPairSwapEquiv N C).symm ((detectorLinearMap f C) q) = (pairDetectorLinearMap f C.doubleNotTarget C.oppositeVertex) ((detectorPairSwapEquiv M C).symm q)
Naturality in the inverse direction, used to move an ordinary detector to the swapped pair presentation.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.trivialDetectorEquiv
{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))
(S : P.ArrowPolarization)
(u₀ : Q)
:
DetectorSpace N (vertex P S u₀ false) ≃ₗ[k] DetectorSpace N (vertex P S u₀ true)
The two polarized trivial-word detectors at one vertex are naturally equivalent.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.trivialDetectorEquiv_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}
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
(f : M ⟶ N)
(S : P.ArrowPolarization)
(u₀ : Q)
(q : DetectorSpace M (vertex P S u₀ false))
:
(trivialDetectorEquiv N S u₀) ((detectorLinearMap f (vertex P S u₀ false)) q) = (detectorLinearMap f (vertex P S u₀ true)) ((trivialDetectorEquiv M S u₀) q)
The trivial-word equivalence commutes with module morphisms.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.trivialDetectorEquiv_symm_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}
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
(f : M ⟶ N)
(S : P.ArrowPolarization)
(u₀ : Q)
(q : DetectorSpace M (vertex P S u₀ true))
:
(trivialDetectorEquiv N S u₀).symm ((detectorLinearMap f (vertex P S u₀ true)) q) = (detectorLinearMap f (vertex P S u₀ false)) ((trivialDetectorEquiv M S u₀).symm q)
Naturality of the inverse trivial-word equivalence.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorWord_eq_of_underlying_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}
(C D : DetectorWord S)
(hword : C.underlying = D.underlying)
(hlength : 0 < Word.length P.relations C.underlying)
:
C = D
Two nontrivial packaged endpoint words with the same literal word are equal, including their target vertex and polarization indices.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorLinearMap_bijective_of_word_eq
{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)
{v : Q}
{s : Bool}
(C : EndpointWord S u₀ t)
(D : EndpointWord S v s)
(hword : C.word = D.word)
(hbijective : Function.Bijective ⇑(detectorLinearMap f C))
:
Function.Bijective ⇑(detectorLinearMap f D)
Bijectivity of a detector map depends only on the literal oriented word, not on the redundant polarization of the trivial word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.reversePairIsString
{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)
:
IsString P.relations (Quiver.Path.comp C.oppositeVertex.path (Quiver.Path.reverse C.doubleNotTarget.path))
The swapped endpoint pair associated with C is always a valid string:
its complete word is the formal reverse of C.word.
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.reversePairWord
{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)
:
The complete word obtained from the swapped endpoint pair of C.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.reversePairWord_eq
{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.reversePairWord = Word.reverse P.relations C.word
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorReversePairEquiv
{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)
(hlength : 0 < Word.length P.relations C.word)
:
DetectorSpace N C ≃ₗ[k] DetectorSpace N (detectorEndpoint S C.reversePairWord)
A nontrivial detector is naturally equivalent to the canonical detector of its reversed literal word.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorReversePairEquiv_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)
(C : EndpointWord S u₀ t)
(hlength : 0 < Word.length P.relations C.word)
(q : DetectorSpace M C)
:
(detectorReversePairEquiv N C hlength) ((detectorLinearMap f C) q) = (detectorLinearMap f (detectorEndpoint S C.reversePairWord)) ((detectorReversePairEquiv M C hlength) q)
Reversal of a nontrivial detector commutes with every module morphism.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorLinearMap_reversePairWord_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)
(C : EndpointWord S u₀ t)
(hlength : 0 < Word.length P.relations C.word)
(hbijective : Function.Bijective ⇑(detectorLinearMap f C))
:
Function.Bijective ⇑(detectorLinearMap f (detectorEndpoint S C.reversePairWord))
Bijectivity transfers from a nontrivial detector to the canonical detector of its reversed literal word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorLinearMap_bijective_of_detectorIndex
{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}
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(hdetector : ∀ (i : DetectorIndex S), Function.Bijective ⇑(detectorLinearMap f i.endpointWord))
{v : Q}
{s : Bool}
(C : EndpointWord S v s)
:
Function.Bijective ⇑(detectorLinearMap f C)
Bijectivity for the chosen representative of every inversion class implies bijectivity for every literal endpoint word.