The distinguished coordinate on a matching string detector #
Target-coordinate evaluation annihilates the matching detector denominator, so it descends to a linear map from the detector quotient to the coefficient field. The endpoint basis class gives an explicit linear section. Proving that this descended coordinate is injective is exactly the remaining one-dimensionality problem for diagonal detector evaluation.
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.numeratorTargetCoordinate
{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)
:
↥(detectorNumerator (C.word.rightModule ⋯) C) →ₗ[k] k
Target-coordinate evaluation restricted to the matching detector numerator.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.numeratorTargetCoordinate_apply
{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)
(x : ↥(detectorNumerator (C.word.rightModule ⋯) C))
:
C.numeratorTargetCoordinate x = (have this := ↑x;
this)
C.word.targetPosition
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.denominatorInNumerator_le_ker_numeratorTargetCoordinate
{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)
:
detectorDenominatorInNumerator (C.word.rightModule ⋯) C ≤ C.numeratorTargetCoordinate.ker
The numerator coordinate kills the denominator submodule.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetCoordinate
{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)
:
DetectorSpace (C.word.rightModule ⋯) C →ₗ[k] k
Target-coordinate evaluation descended to the matching detector quotient.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetCoordinate_mk
{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)
(x : ↥(detectorNumerator (C.word.rightModule ⋯) C))
:
C.detectorTargetCoordinate (Submodule.Quotient.mk x) = C.numeratorTargetCoordinate x
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetCoordinate_targetDetectorClass
{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)
:
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetSection
{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)
:
k →ₗ[k] DetectorSpace (C.word.rightModule ⋯) C
Scalar multiples of the distinguished endpoint class give a linear section of the descended target coordinate.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetSection_apply
{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)
(c : k)
:
C.detectorTargetSection c = c • C.targetDetectorClass
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetCoordinate_comp_detectorTargetSection
{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)
:
C.detectorTargetCoordinate ∘ₗ C.detectorTargetSection = LinearMap.id
The descended target coordinate is a split epimorphism.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetCoordinate_surjective
{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)
:
Function.Surjective ⇑C.detectorTargetCoordinate
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetCoordinate_injective_iff
{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)
:
Function.Injective ⇑C.detectorTargetCoordinate ↔ C.numeratorTargetCoordinate.ker ≤ detectorDenominatorInNumerator (C.word.rightModule ⋯) C
Exact residual form of diagonal one-dimensionality: the descended coordinate is injective precisely when every numerator vector with zero target coordinate already lies in the detector denominator.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.ker_numeratorTargetCoordinate_le_denominator_iff_single
{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)
:
C.numeratorTargetCoordinate.ker ≤ detectorDenominatorInNumerator (C.word.rightModule ⋯) C ↔ ∀ (i : C.word.PositionAt u₀),
i ≠ C.word.targetPosition →
Finsupp.single i 1 ∈ detectorNumerator (C.word.rightModule ⋯) C →
Finsupp.single i 1 ∈ detectorDenominator (C.word.rightModule ⋯) C
The reverse kernel inclusion is equivalent to a basis-position statement: every non-target position basis vector which lies in the numerator already lies in the denominator.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetCoordinate_injective_iff_single
{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)
:
Function.Injective ⇑C.detectorTargetCoordinate ↔ ∀ (i : C.word.PositionAt u₀),
i ≠ C.word.targetPosition →
Finsupp.single i 1 ∈ detectorNumerator (C.word.rightModule ⋯) C →
Finsupp.single i 1 ∈ detectorDenominator (C.word.rightModule ⋯) C
Diagonal one-dimensionality is therefore exactly the absence of any surviving non-target position basis vector in the matching detector.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetCoordinate_injective
{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)
:
Function.Injective ⇑C.detectorTargetCoordinate
Target-coordinate evaluation is injective on the matching detector. Every hypothetical surviving non-target coordinate traces a complete copy of the word through itself, whose endpoint rigidity forces that coordinate to be the target after all.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorTargetEquiv
{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)
:
DetectorSpace (C.word.rightModule ⋯) C ≃ₗ[k] k
The matching finite-string detector is canonically one-dimensional by target-coordinate evaluation.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.finrank_detectorSpace_rightModule_self
{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)
:
Module.finrank k (DetectorSpace (C.word.rightModule ⋯) C) = 1
Literal dimension statement for matching detector evaluation.