Position coefficients of morphisms between string modules

A displayed arrow acts as a partial bijection on the position basis of a string word. This file turns naturality of an arbitrary morphism between two string modules into the local coefficient rules used in graph-map theory: coefficients propagate across two matched arrow steps and vanish at an unmatched source or target boundary.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowStep_source_subsingleton {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) (j : C.PositionAt y) : Subsingleton { i : C.PositionAt x // C.ArrowStep a i j }

A string word has at most one source position mapping to a fixed target position under a displayed arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowOnBasis_apply_eq_zero_of_not_step {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : ¬C.ArrowStep a i j) : (C.arrowOnBasis a i) j = 0

Away from a witnessed arrow step, the corresponding target coefficient of the image basis vector is zero.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowLinearMap_apply_of_step {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) (v : C.Space x) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.ArrowStep a i j) : ((C.arrowLinearMap a) v) j = v i

A displayed-arrow map reads the unique source coefficient at every witnessed target position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowLinearMap_apply_eq_zero_of_not_exists_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) (v : C.Space x) (j : C.PositionAt y) (hj : ¬∃ (i : C.PositionAt x), C.ArrowStep a i j) : ((C.arrowLinearMap a) v) j = 0

If a target position has no source under a displayed arrow, every arrow image has zero coefficient there.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficient {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) {x : Q} (i : C.PositionAt x) (j : D.PositionAt x) : k

The coefficient from a source position basis vector to a target position basis vector for a morphism between two string modules.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficient_eq_of_arrowSteps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (i' : D.PositionAt x) (j' : D.PositionAt y) (hij : C.ArrowStep a i j) (hij' : D.ArrowStep a i' j') : C.morphismCoefficient D hC hD f i i' = C.morphismCoefficient D hC hD f j j'

A morphism coefficient propagates across a pair of matched displayed-arrow steps in the source and target strings.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficient_eq_zero_of_source_step_of_no_target_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (j' : D.PositionAt y) (hij : C.ArrowStep a i j) (hj' : ¬∃ (i' : D.PositionAt x), D.ArrowStep a i' j') : C.morphismCoefficient D hC hD f j j' = 0

A coefficient vanishes at a target-string boundary when the source-string basis vector crosses the displayed arrow but the target position has no incoming matched step.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficient_eq_zero_of_no_source_target_of_target_step {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (i' : D.PositionAt x) (j' : D.PositionAt y) (hi : ¬∃ (j : C.PositionAt y), C.ArrowStep a i j) (hij' : D.ArrowStep a i' j') : C.morphismCoefficient D hC hD f i i' = 0

A coefficient vanishes at a source-string boundary when its source basis vector has no outgoing displayed-arrow step but the target position does.