Linear representatives of finite-string detector classes #
The detector is a quotient of its numerator. Over a field its quotient map
has a linear section, providing a chosen numerator representative of every
detector class. Coherent lifting of that representative along the word is
constructed separately in StringDetectorTrajectory.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorQuotientMap
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype 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)
:
↥(detectorNumerator N C) →ₗ[k] DetectorSpace N C
The quotient map from the detector numerator to the detector space.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorQuotientMap_surjective
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype 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)
:
Function.Surjective ⇑(detectorQuotientMap N C)
The detector quotient map is surjective.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorRepresentative
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype 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)
:
DetectorSpace N C →ₗ[k] ↥(detectorNumerator N C)
A chosen linear representative in the numerator for each detector quotient class.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorQuotientMap_comp_detectorRepresentative
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype 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)
:
detectorQuotientMap N C ∘ₗ detectorRepresentative N C = LinearMap.id
Taking the class of the chosen representative recovers the original detector class.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorUpperRepresentative
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype 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)
:
DetectorSpace N C →ₗ[k] ↥(upperSubspace N C)
The chosen numerator representative, regarded as a member of the upper
word subspace along C.