Module maps carried by boundary-free coefficient components

Every boundary-free equality component in the coefficient constraint graph defines a morphism between the corresponding string modules: put coefficient one on the component and zero elsewhere. Naturality is exactly the statement that matched-step edges carry equal coefficients and unmatched boundaries carry coefficient zero.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentIndicator {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root p : C.MorphismCoefficientPosition D) : k

The scalar indicator of one generated coefficient component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentIndicator_eq_one {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root p : C.MorphismCoefficientPosition D) (hp : Relation.EqvGen (C.MorphismCoefficientStep D) root p) : C.coefficientComponentIndicator D root p = 1

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentIndicator_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root p : C.MorphismCoefficientPosition D) (hp : ¬Relation.EqvGen (C.MorphismCoefficientStep D) root p) : C.coefficientComponentIndicator D root p = 0

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentOnBasis {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) {x : Q} (i : C.PositionAt x) : D.Space x

The position-basis vector whose coordinates are the indicator of one coefficient component above a fixed source position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentOnBasis_apply {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) {x : Q} (i : C.PositionAt x) (j : D.PositionAt x) : (C.coefficientComponentOnBasis D root i) j = C.coefficientComponentIndicator D root ⟨x, (i, j)⟩

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentLinearMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (x : Q) : C.Space x →ₗ[k] D.Space x

Extend a component indicator linearly from the source position basis.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentLinearMap_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) {x : Q} (i : C.PositionAt x) (c : k) : (C.coefficientComponentLinearMap D root x) (Finsupp.single i c) = c • C.coefficientComponentOnBasis D root i

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.eqvGen_morphismCoefficientStep_iff {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) {p q : C.MorphismCoefficientPosition D} (hpq : C.MorphismCoefficientStep D p q) : Relation.EqvGen (C.MorphismCoefficientStep D) root p ↔ Relation.EqvGen (C.MorphismCoefficientStep D) root q

Adjoining one equality edge does not change membership in the generated coefficient component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowLinearMap_coefficientComponentOnBasis {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) : (D.arrowLinearMap a) (C.coefficientComponentOnBasis D root i) = (C.coefficientComponentLinearMap D root y) (C.arrowOnBasis a i)

The component indicator commutes with one displayed arrow on a source basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentLinearMap_arrowLinearMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) {x y : Q} (a : x ⟶ y) (v : C.Space x) : (C.coefficientComponentLinearMap D root y) ((C.arrowLinearMap a) v) = (D.arrowLinearMap a) ((C.coefficientComponentLinearMap D root x) v)

The component-indicator linear maps commute with every displayed arrow.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentQuiverRepresentationMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) : C.quiverRepresentation ⟶ D.quiverRepresentation

A boundary-free component indicator is a morphism of the underlying quiver representations.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentFreeRightModuleAuxMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) : D.freeRightModuleAux ⟶ C.freeRightModuleAux

In the opposite-module realization, a component indicator has the reversed natural-transformation direction.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentQuotientRightModuleAuxMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) (hC hD : IsMonomial R) : D.quotientRightModuleAux hD ⟶ C.quotientRightModuleAux hC

Descend a component indicator through the monomial relation quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentRightModuleMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) (hC hD : IsMonomial R) : C.rightModule hC ⟶ D.rightModule hD

The right-module morphism whose matrix is the indicator of a boundary-free coefficient component.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientComponentRightModuleMap_app_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) (hC hD : IsMonomial R) (x : Q) : (C.coefficientComponentRightModuleMap D root hfree hC hD).app (Opposite.op (obj R x)) = ModuleCat.ofHom (C.coefficientComponentLinearMap D root x)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_coefficientComponentRightModuleMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root p : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) (hC hD : IsMonomial R) : C.morphismCoefficientAt D hC hD (C.coefficientComponentRightModuleMap D root hfree hC hD) p = C.coefficientComponentIndicator D root p

The coefficient matrix of the component map is exactly the indicator of the selected component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_coefficientComponentRightModuleMap_root {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) (hC hD : IsMonomial R) : C.morphismCoefficientAt D hC hD (C.coefficientComponentRightModuleMap D root hfree hC hD) root = 1

The selected component map has coefficient one at its root.