Coherent trajectories along a string word

A trajectory assigns an ambient-module vector to every position of a string word. Membership records a source-subspace condition and compatibility along every displayed word edge. Thus all position maps obtained from one linear section of the trajectory space are coherent by construction, rather than by comparison of separately chosen path lifts.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.incomingAdjacentArrows_ne {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {w x z : Q} (a : w ⟶ x) (b : z ⟶ x) (previous : C.PositionAt w) (i : C.PositionAt x) (next : C.PositionAt z) (hpreviousIndex : previous.index + 1 = i.index) (hnextIndex : next.index = i.index + 1) (ha : C.ArrowStep a previous i) (hb : C.ArrowStep b next i) : ⟨w, a⟩ ≠ ⟨z, b⟩

The two arrows entering an internal peak from its adjacent word positions are distinct.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.outgoingAdjacentArrows_ne {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {w x z : Q} (a : x ⟶ w) (b : x ⟶ z) (previous : C.PositionAt w) (i : C.PositionAt x) (next : C.PositionAt z) (hpreviousIndex : previous.index + 1 = i.index) (hnextIndex : next.index = i.index + 1) (ha : C.ArrowStep a i previous) (hb : C.ArrowStep b i next) : ⟨w, a⟩ ≠ ⟨z, b⟩

The two arrows leaving an internal valley toward its adjacent word positions are distinct.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pathReach_of_prefix_eq_positivePath_reverse {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (p : Quiver.Path x y) (i : C.PositionAt x) (j : C.PositionAt y) : ↑i = Quiver.Path.comp (↑j) (Quiver.Path.reverse (positivePath p)) → C.PathReach p i j

A reversed positive path occurring literally between two word prefixes gives reachability by that ordinary path in the displayed arrow direction.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.Word.PositionFamily {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) : Type u

A vector in the ambient module at every total position of a word.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.Word.totalSourcePosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : C.Position

The source endpoint regarded as a total word position.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.Word.totalTargetPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : C.Position

The target endpoint regarded as a total word position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.totalSourcePosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : C.totalSourcePosition.index = 0

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.totalTargetPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : C.totalTargetPosition.index = length R C

def MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectorySubmodule {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) : Submodule k (PositionFamily N C)

Trajectories which start in U and satisfy the ambient-module arrow equation along every edge displayed by the word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mem_trajectorySubmodule {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (v : PositionFamily N C) : v ∈ trajectorySubmodule N C U ↔ v C.totalSourcePosition ∈ U ∧ ∀ {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y), C.ArrowStep a i j → (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N a)) (v ⟨x, i⟩) = v ⟨y, j⟩

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryPositionMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (i : C.Position) : ↥(trajectorySubmodule N C U) →ₗ[k] ↑(N.obj (Opposite.op (obj R i.fst)))

Evaluation of a coherent trajectory at a total word position.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryPositionAtMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) {x : Q} (i : C.PositionAt x) : ↥(trajectorySubmodule N C U) →ₗ[k] ↑(N.obj (Opposite.op (obj R x)))

Evaluation at a position over a specified displayed vertex.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryPositionAtMap_apply {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) {x : Q} (i : C.PositionAt x) (v : ↥(trajectorySubmodule N C U)) : (trajectoryPositionAtMap N C U i) v = ↑v ⟨x, i⟩

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.moduleArrowMap_trajectoryPositionAtMap_of_arrowStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.ArrowStep a i j) (v : ↥(trajectorySubmodule N C U)) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N a)) ((trajectoryPositionAtMap N C U i) v) = (trajectoryPositionAtMap N C U j) v

Position evaluation respects every displayed arrow step by definition of the trajectory submodule.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.modulePathMap_trajectoryPositionAtMap_of_pathReach {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) {x y : Q} (p : Quiver.Path x y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.PathReach p i j) (v : ↥(trajectorySubmodule N C U)) : (CategoryTheory.ConcreteCategory.hom (modulePathMap N p)) ((trajectoryPositionAtMap N C U i) v) = (trajectoryPositionAtMap N C U j) v

Position evaluation respects every ordinary path realized monotonically along the word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectory_value_mem_signedPathSubspace {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (v : ↥(trajectorySubmodule N C U)) (i : C.Position) : ↑v i ∈ signedPathSubspace N (↑i.snd) U

The value of a coherent trajectory at each prefix belongs to the subspace obtained by transporting U along that prefix.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTerminalMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) : ↥(trajectorySubmodule N C U) →ₗ[k] ↑(N.obj (Opposite.op (obj R C.target)))

Terminal evaluation from the trajectory submodule.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTerminalMap_range_le_signedPathSubspace {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) : (trajectoryTerminalMap N C U).range ≤ signedPathSubspace N C.path U

Every terminal value of a coherent trajectory lies in the full transported subspace.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTransportMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) : ↥(trajectorySubmodule N C U) →ₗ[k] ↥(signedPathSubspace N C.path U)

Terminal evaluation with its codomain restricted to the full transported subspace.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTransportMap_coe {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (v : ↥(trajectorySubmodule N C U)) : ↑((trajectoryTransportMap N C U) v) = ↑v C.totalTargetPosition

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.extendPositionFamily {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) {z : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (v : PositionFamily N C) (w : ↑(N.obj (Opposite.op (obj R z)))) : PositionFamily N (append R C e h)

Extend a position family across one appended letter by retaining all old values and assigning a specified value to the unique new endpoint.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.extendPositionFamily_appendPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) {z x : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (v : PositionFamily N C) (w : ↑(N.obj (Opposite.op (obj R z)))) (i : C.PositionAt x) : extendPositionFamily N C e h v w ⟨x, C.appendPosition e h i⟩ = v ⟨x, i⟩

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.extendPositionFamily_appendEndPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) {z : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (v : PositionFamily N C) (w : ↑(N.obj (Opposite.op (obj R z)))) : extendPositionFamily N C e h v w ⟨z, C.appendEndPosition e h⟩ = w

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.eq_totalTargetPosition_of_not_exists_old {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {z : Q} (e : SignedArrow C.target z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath e))) (i : (append R C e h).Position) (hi : ¬∃ (j : C.PositionAt i.fst), C.appendPosition e h j = i.snd) : i = (append R C e h).totalTargetPosition

A total position of an appended word which is not inherited from the old word is its unique new target position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.extendPositionFamily_mem_trajectorySubmodule_positive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) {z : Q} (a : C.target ⟶ z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (v : ↥(trajectorySubmodule N C U)) (w : ↑(N.obj (Opposite.op (obj R z)))) (hw : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N a)) (↑v C.totalTargetPosition) = w) : extendPositionFamily N C (positiveArrow a) h (↑v) w ∈ trajectorySubmodule N (append R C (positiveArrow a) h) U

Extending a coherent trajectory across a positive letter preserves coherence when the new endpoint value is the arrow image of the old terminal value.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.extendPositionFamily_mem_trajectorySubmodule_negative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) {z : Q} (a : z ⟶ C.target) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (v : ↥(trajectorySubmodule N C U)) (w : ↑(N.obj (Opposite.op (obj R z)))) (hw : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N a)) w = ↑v C.totalTargetPosition) : extendPositionFamily N C (negativeArrow a) h (↑v) w ∈ trajectorySubmodule N (append R C (negativeArrow a) h) U

Extending a coherent trajectory across a negative letter preserves coherence when the old terminal value is the arrow image of the new endpoint value.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTransportMap_surjective_append_positive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) {z : Q} (a : C.target ⟶ z) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow a)))) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (hsurj : Function.Surjective ⇑(trajectoryTransportMap N C U)) : Function.Surjective ⇑(trajectoryTransportMap N (append R C (positiveArrow a) h) U)

Surjectivity of coherent terminal evaluation is preserved by appending a positive letter.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTransportMap_surjective_append_negative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) {z : Q} (a : z ⟶ C.target) (h : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (hsurj : Function.Surjective ⇑(trajectoryTransportMap N C U)) : Function.Surjective ⇑(trajectoryTransportMap N (append R C (negativeArrow a) h) U)

Surjectivity of coherent terminal evaluation is preserved by appending a negative letter.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTransportMap_surjective_of_length_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (hzero : length R C = 0) : Function.Surjective ⇑(trajectoryTransportMap N C U)

For a length-zero word, coherent terminal evaluation is the identity on the chosen source subspace.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTransportMap_surjective_path {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x target : Q} (p : SignedPath x target) (hstring : IsString R p) (U : Submodule k ↑(N.obj (Opposite.op (obj R x)))) : Function.Surjective ⇑(trajectoryTransportMap N { source := x, target := target, path := p, isString := hstring } U)

Path-inductive form of surjectivity of coherent terminal evaluation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTransportMap_surjective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) : Function.Surjective ⇑(trajectoryTransportMap N C U)

Coherent terminal evaluation is onto the transported subspace for every finite string word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectorySection {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) : ↥(signedPathSubspace N C.path U) →ₗ[k] ↥(trajectorySubmodule N C U)

A single chosen linear section of terminal evaluation into coherent trajectories.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.trajectoryTransportMap_comp_trajectorySection {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) : trajectoryTransportMap N C U ∘ₗ trajectorySection N C U = LinearMap.id

The coherent trajectory section has the requested terminal value.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.coherentPositionMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) {x : Q} (i : C.PositionAt x) : ↥(signedPathSubspace N C.path U) →ₗ[k] ↑(N.obj (Opposite.op (obj R x)))

The coherent linear lift from the full transported subspace to one word position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.moduleArrowMap_coherentPositionMap_of_arrowStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.ArrowStep a i j) (q : ↥(signedPathSubspace N C.path U)) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N a)) ((coherentPositionMap N C U i) q) = (coherentPositionMap N C U j) q

Coherent position lifts respect every arrow step displayed by the word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.modulePathMap_coherentPositionMap_of_pathReach {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) {x y : Q} (p : Quiver.Path x y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.PathReach p i j) (q : ↥(signedPathSubspace N C.path U)) : (CategoryTheory.ConcreteCategory.hom (modulePathMap N p)) ((coherentPositionMap N C U i) q) = (coherentPositionMap N C U j) q

Coherent position lifts respect every ordinary path realized monotonically along the word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.coherentPositionMap_targetPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (C : Word R) (U : Submodule k ↑(N.obj (Opposite.op (obj R C.source)))) (q : ↥(signedPathSubspace N C.path U)) : (coherentPositionMap N C U C.targetPosition) q = ↑q

At the terminal position, the coherent lift recovers the given transported vector.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorPositionMap {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) {x : Q} (i : C.word.PositionAt x) : DetectorSpace N C →ₗ[k] ↑(N.obj (Opposite.op (obj P.relations x)))

Coherent detector-class evaluation at one position of the detector word. All position maps factor through the same trajectory section.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorBilinearMap {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) (x : Q) : C.word.Space x →ₗ[k] DetectorSpace N C →ₗ[k] ↑(N.obj (Opposite.op (obj P.relations x)))

Bilinear evaluation of a string-space vector and a detector class by the coherent position lifts.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorTensorMap {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) (x : Q) : TensorProduct k (C.word.Space x) (DetectorSpace N C) →ₗ[k] ↑(N.obj (Opposite.op (obj P.relations x)))

Evaluation from the coefficient-copy string space to the ambient module at one quiver vertex.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorTensorMap_single_tmul {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) {x : Q} (i : C.word.PositionAt x) (c : k) (q : DetectorSpace N C) : (coherentDetectorTensorMap N C x) (Finsupp.single i c ⊗ₜ[k] q) = c • (coherentDetectorPositionMap N C i) q

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.sourceIncomingStep_zeroPath_or_outgoingInverseExtension {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} (C : EndpointWord S u₀ t) {y z : Q} (b : C.source ⟶ y) (a : z ⟶ C.source) (next : C.word.PositionAt z) (hnextIndex : next.index = 1) (ha : C.word.ArrowStep a next C.word.sourcePosition) : (∃ (w : Q) (p : Quiver.Path w C.source) (previous : C.word.PositionAt w), C.word.PathReach p previous C.word.sourcePosition ∧ CategoryTheory.CategoryStruct.comp (arrowMap P.relations b) (pathMap P.relations p) = 0) ∨ IsString P.relations ((Quiver.Hom.toPath (negativeArrow b)).comp C.path) ∧ C.sourceSign = !S.sourceSign b

If a word begins with an inverse arrow, then an additional outgoing inverse either extends the whole string or closes a monomial relation against an incoming path realized by the initial inverse arm.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.sourceOutgoingStep_outgoingInverseExtension {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} (C : EndpointWord S u₀ t) {y z : Q} (b : C.source ⟶ y) (a : C.source ⟶ z) (next : C.word.PositionAt z) (hnextIndex : next.index = 1) (ha : C.word.ArrowStep a C.word.sourcePosition next) (hnot : ¬∃ (j : C.word.PositionAt y), C.word.ArrowStep b C.word.sourcePosition j) : IsString P.relations ((Quiver.Hom.toPath (negativeArrow b)).comp C.path) ∧ C.sourceSign = !S.sourceSign b

If a word begins with an ordinary outgoing arrow, every distinct outgoing arrow gives a compatible inverse extension at the source boundary.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.exists_incomingArrowStep_comp_eq_zero_of_internal_not_arrowStep {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} (C : EndpointWord S u₀ t) {x y : Q} (b : x ⟶ y) (i : C.word.PositionAt x) (hpos : 0 < i.index) (hlt : i.index < Word.length P.relations C.word) (hnot : ¬∃ (j : C.word.PositionAt y), C.word.ArrowStep b i j) : ∃ (w : Q) (a : w ⟶ x) (previous : C.word.PositionAt w), C.word.ArrowStep a previous i ∧ CategoryTheory.CategoryStruct.comp (arrowMap P.relations b) (arrowMap P.relations a) = 0

At an internal word position, every ordinary arrow not displayed out of that position forms a zero two-arrow path with some displayed incoming arrow. Peaks use uniqueness of a left continuation, valleys use the degree-two bound, and the two mixed orientations use uniqueness of a right continuation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorPositionMap_of_arrowStep {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) {x y : Q} (a : x ⟶ y) (i : C.word.PositionAt x) (j : C.word.PositionAt y) (hij : C.word.ArrowStep a i j) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N a)) ((coherentDetectorPositionMap N C i) q) = (coherentDetectorPositionMap N C j) q

Detector position maps respect every arrow step displayed by the word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorPositionMap_eq_zero_of_incomingPath {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)) [N.Additive] (C : EndpointWord S u₀ t) {w x y : Q} (p : Quiver.Path w x) (b : x ⟶ y) (previous : C.word.PositionAt w) (i : C.word.PositionAt x) (hp : C.word.PathReach p previous i) (hzero : CategoryTheory.CategoryStruct.comp (arrowMap P.relations b) (pathMap P.relations p) = 0) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N b)) ((coherentDetectorPositionMap N C i) q) = 0

An incoming displayed path annihilates every outgoing arrow whose concatenation with that path is a relation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorPositionMap_eq_zero_of_internal_not_arrowStep {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)) [N.Additive] (C : EndpointWord S u₀ t) {x y : Q} (b : x ⟶ y) (i : C.word.PositionAt x) (hpos : 0 < i.index) (hlt : i.index < Word.length P.relations C.word) (hnot : ¬∃ (j : C.word.PositionAt y), C.word.ArrowStep b i j) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N b)) ((coherentDetectorPositionMap N C i) q) = 0

Every non-displayed outgoing arrow kills the coherent detector value at an internal word position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_eq_zero_of_mem_upperBoundarySubspace {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) (out : C.OutgoingInverseExtension) (v : ↑(N.obj (Opposite.op (obj P.relations C.source)))) (hv : v ∈ upperBoundarySubspace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N (↑out).snd)) v = 0

Membership in an upper boundary subspace is exactly the vanishing needed for any witnessed compatible outgoing inverse extension.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorPositionMap_source_eq_zero {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) (out : C.OutgoingInverseExtension) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N (↑out).snd)) ((coherentDetectorPositionMap N C C.word.sourcePosition) q) = 0

A witnessed compatible outgoing inverse extension kills the coherent detector value at the source endpoint.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorPositionMap_target_eq_zero {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) (out : C.oppositeVertex.OutgoingInverseExtension) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N (↑out).snd)) ((coherentDetectorPositionMap N C C.word.targetPosition) q) = 0

A witnessed compatible outgoing inverse extension of the opposite trivial word kills the coherent detector value at the target endpoint.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorPositionMap_source_eq_zero_of_not_arrowStep {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)) [N.Additive] (C : EndpointWord S u₀ t) {y : Q} (b : C.source ⟶ y) (hnot : ¬∃ (j : C.word.PositionAt y), C.word.ArrowStep b C.word.sourcePosition j) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N b)) ((coherentDetectorPositionMap N C C.word.sourcePosition) q) = 0

Every non-displayed outgoing arrow kills the coherent detector value at the source endpoint. A failed inverse extension contributes its exact initial monomial relation; a successful extension is killed by the source upper boundary. For a trivial word the two endpoint polarizations partition all outgoing arrows.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorPositionMap_target_eq_zero_of_not_arrowStep {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)) [N.Additive] (C : EndpointWord S u₀ t) {y : Q} (b : u₀ ⟶ y) (hnot : ¬∃ (j : C.word.PositionAt y), C.word.ArrowStep b C.word.targetPosition j) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N b)) ((coherentDetectorPositionMap N C C.word.targetPosition) q) = 0

Every non-displayed outgoing arrow kills the coherent detector value at the target endpoint. The opposite trivial upper boundary handles every surviving or distinct outgoing continuation; a zero continuation is killed by the incoming-path relation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorPositionMap_eq_zero_of_not_arrowStep {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)) [N.Additive] (C : EndpointWord S u₀ t) {x y : Q} (b : x ⟶ y) (i : C.word.PositionAt x) (hnot : ¬∃ (j : C.word.PositionAt y), C.word.ArrowStep b i j) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N b)) ((coherentDetectorPositionMap N C i) q) = 0

The coherent detector position maps satisfy the zero equation for every ordinary arrow not displayed out of the given word position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorTensorMap_single_tmul {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)) [N.Additive] (C : EndpointWord S u₀ t) {x y : Q} (a : x ⟶ y) (i : C.word.PositionAt x) (c : k) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N a)) ((coherentDetectorTensorMap N C x) (Finsupp.single i c ⊗ₜ[k] q)) = (coherentDetectorTensorMap N C y) ((C.word.arrowLinearMap a) (Finsupp.single i c) ⊗ₜ[k] q)

Tensor evaluation intertwines one ordinary arrow on every position-basis pure tensor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.moduleArrowMap_coherentDetectorTensorMap_tmul {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)) [N.Additive] (C : EndpointWord S u₀ t) {x y : Q} (a : x ⟶ y) (v : C.word.Space x) (q : DetectorSpace N C) : (CategoryTheory.ConcreteCategory.hom (moduleArrowMap N a)) ((coherentDetectorTensorMap N C x) (v ⊗ₜ[k] q)) = (coherentDetectorTensorMap N C y) ((C.word.arrowLinearMap a) v ⊗ₜ[k] q)

Tensor evaluation intertwines one ordinary arrow on an arbitrary pure tensor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorTensorMap_arrow_naturality {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)) [N.Additive] (C : EndpointWord S u₀ t) {x y : Q} (a : x ⟶ y) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (coherentDetectorTensorMap N C x)) (moduleArrowMap N a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ModuleCat.ofHom (C.word.arrowLinearMap a)) (ModuleCat.of k (DetectorSpace N C))) (ModuleCat.ofHom (coherentDetectorTensorMap N C y))

The tensor evaluation maps satisfy the quiver-arrow naturality square.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorTensorMap_path_naturality {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)) [N.Additive] (C : EndpointWord S u₀ t) {x y : Q} (p : Quiver.Path x y) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (coherentDetectorTensorMap N C x)) (modulePathMap N p) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (C.word.quiverMap p) (ModuleCat.of k (DetectorSpace N C))) (ModuleCat.ofHom (coherentDetectorTensorMap N C y))

The tensor evaluation maps satisfy naturality along every ordinary quiver path.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorTensorMap_boundPath_naturality {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)) [N.Additive] (C : EndpointWord S u₀ t) (hmono : IsMonomial P.relations) {x y : Q} (p : Quiver.Path x y) : CategoryTheory.CategoryStruct.comp ((C.word.scalarRightModule hmono (ModuleCat.of k (DetectorSpace N C))).map (pathMap P.relations p).op) (ModuleCat.ofHom (coherentDetectorTensorMap N C y)) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (coherentDetectorTensorMap N C x)) (N.map (pathMap P.relations p).op)

Path naturality written directly for the descended coefficient-copy string module and the ambient bound-quiver module.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorTensorMap_pathHom_naturality {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)) [N.Additive] (C : EndpointWord S u₀ t) (hmono : IsMonomial P.relations) {X Y : LinearPathCategory.Category k Q} (p : Quiver.Path (LinearPathCategory.vertex Y) (LinearPathCategory.vertex X)) : CategoryTheory.CategoryStruct.comp ((C.word.scalarRightModule hmono (ModuleCat.of k (DetectorSpace N C))).map ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map (LinearPathCategory.pathHom p)).op) (ModuleCat.ofHom (coherentDetectorTensorMap N C (LinearPathCategory.vertex X))) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (coherentDetectorTensorMap N C (LinearPathCategory.vertex Y))) (N.map ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map (LinearPathCategory.pathHom p)).op)

The same path square with source and target retained as arbitrary objects of the free linear path category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorTensorMap_free_naturality {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)) [N.Additive] [CategoryTheory.Functor.Linear k N] (C : EndpointWord S u₀ t) (hmono : IsMonomial P.relations) {X Y : LinearPathCategory.Category k Q} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((C.word.scalarRightModule hmono (ModuleCat.of k (DetectorSpace N C))).map ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f).op) (ModuleCat.ofHom (coherentDetectorTensorMap N C (LinearPathCategory.vertex X))) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (coherentDetectorTensorMap N C (LinearPathCategory.vertex Y))) (N.map ((LinearPathCategory.HomogeneousQuotient.quotientFunctor P.relations).map f).op)

Tensor evaluation is natural for every morphism before passage from the free linear path category to the bound-path quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorModuleMap {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)) [N.Additive] [CategoryTheory.Functor.Linear k N] (C : EndpointWord S u₀ t) (hmono : IsMonomial P.relations) : C.word.scalarRightModule hmono (ModuleCat.of k (DetectorSpace N C)) ⟶ N

The coherent trajectory evaluation is an actual morphism from the coefficient-copy string module to the ambient bound-quiver module.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorModuleMap_app_obj {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)) [N.Additive] [CategoryTheory.Functor.Linear k N] (C : EndpointWord S u₀ t) (hmono : IsMonomial P.relations) (x : Q) : (coherentDetectorModuleMap N C hmono).app (Opposite.op (obj P.relations x)) = ModuleCat.ofHom (coherentDetectorTensorMap N C x)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorEvaluation {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 : CoveringHom.LinearModuleCategory k) (C : EndpointWord S u₀ t) (hmono : IsMonomial P.relations) : (C.word.stringEmbeddingFunctor hmono).obj (C.detectorFunctor.obj N) ⟶ N

Objectwise Butler--Ringel evaluation S_C(F_C(N)) → N, bundled in the category of linear modules.