Coefficient-support components of string morphisms

Naturality presents the matrix coefficients of a morphism between two string modules by equality constraints along matched word steps and zero constraints at unmatched boundaries. This file packages that presentation as a graph on pairs of word positions. Its connected components are the ambient objects from which graph-map overlaps will be extracted.

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

A possible matrix-coefficient position for a morphism from C to D: two word positions lying over the same displayed vertex.

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

The source-word index of a coefficient position.

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

The target-word index of a coefficient position.

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

The source-word position underlying a coefficient position.

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

The target-word position underlying a coefficient position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.MorphismCoefficientPosition.inputPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (p : C.MorphismCoefficientPosition D) : p.inputPosition.index = p.inputIndex

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.MorphismCoefficientPosition.outputPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (p : C.MorphismCoefficientPosition D) : p.outputPosition.index = p.outputIndex

def MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientPositionIndexEmbedding {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : C.MorphismCoefficientPosition D ↪ Fin (length R C + 1) × Fin (length R D + 1)

The two word indices determine a coefficient position.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientPosition_finite {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Finite (C.MorphismCoefficientPosition D)

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

A coefficient position on the diagonal of an endomorphism matrix.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt {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) (p : C.MorphismCoefficientPosition D) : k

The value of a string-module morphism at one coefficient position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (p : C.MorphismCoefficientPosition D) : C.morphismCoefficientAt D hC hD 0 p = 0

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_add {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f g : C.rightModule hC ⟶ D.rightModule hD) (p : C.MorphismCoefficientPosition D) : C.morphismCoefficientAt D hC hD (f + g) p = C.morphismCoefficientAt D hC hD f p + C.morphismCoefficientAt D hC hD g p

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_neg {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) (p : C.MorphismCoefficientPosition D) : C.morphismCoefficientAt D hC hD (-f) p = -C.morphismCoefficientAt D hC hD f p

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_sub {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f g : C.rightModule hC ⟶ D.rightModule hD) (p : C.MorphismCoefficientPosition D) : C.morphismCoefficientAt D hC hD (f - g) p = C.morphismCoefficientAt D hC hD f p - C.morphismCoefficientAt D hC hD g p

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_smul {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (c : k) (f : C.rightModule hC ⟶ D.rightModule hD) (p : C.MorphismCoefficientPosition D) : C.morphismCoefficientAt D hC hD (c • f) p = c * C.morphismCoefficientAt D hC hD f p

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_sum {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) {ι : Type u_1} (s : Finset ι) (f : ι → (C.rightModule hC ⟶ D.rightModule hD)) (p : C.MorphismCoefficientPosition D) : C.morphismCoefficientAt D hC hD (∑ i ∈ s, f i) p = ∑ i ∈ s, C.morphismCoefficientAt D hC hD (f i) p

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightModuleHom_ext_morphismCoefficientAt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) {f g : C.rightModule hC ⟶ D.rightModule hD} (hcoeff : ∀ (p : C.MorphismCoefficientPosition D), C.morphismCoefficientAt D hC hD f p = C.morphismCoefficientAt D hC hD g p) : f = g

A morphism between position-basis string modules is determined by all of its position coefficients.

inductive MagnitudeConjecture.BoundQuiver.StringWord.Word.MorphismCoefficientStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : C.MorphismCoefficientPosition D → C.MorphismCoefficientPosition D → Prop

An equality edge between coefficient positions. Both words cross the same displayed arrow, so naturality identifies the two coefficients.

• ofArrow {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} {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.MorphismCoefficientStep D ⟨x, (i, i')⟩ ⟨y, (j, j')⟩

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.MorphismCoefficientStep.index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : C.MorphismCoefficientStep D p q) : (q.inputIndex = p.inputIndex + 1 ∨ p.inputIndex = q.inputIndex + 1) ∧ (q.outputIndex = p.outputIndex + 1 ∨ p.outputIndex = q.outputIndex + 1)

A matched-step edge moves one index in each of the two words.

inductive MagnitudeConjecture.BoundQuiver.StringWord.Word.IsMorphismCoefficientBoundary {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : C.MorphismCoefficientPosition D → Prop

A zero boundary in the coefficient constraint graph. The first constructor records a source-word step with no matching incoming target-word step; the second records a target-word step with no matching outgoing source-word step.

• source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} {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.IsMorphismCoefficientBoundary D ⟨y, (j, j')⟩
• target {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} {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.IsMorphismCoefficientBoundary D ⟨x, (i, i')⟩

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

A generated coefficient component contains no naturality boundary marked as zero.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.diagonalMorphismCoefficientPosition_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (C.MorphismCoefficientStep C) (C.diagonalMorphismCoefficientPosition i) (C.diagonalMorphismCoefficientPosition C.sourcePosition)

All diagonal coefficient positions of one word lie in the component of the source position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_eq_of_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) {p q : C.MorphismCoefficientPosition D} (hpq : C.MorphismCoefficientStep D p q) : C.morphismCoefficientAt D hC hD f p = C.morphismCoefficientAt D hC hD f q

Coefficients agree across one matched-step edge.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_eq_zero_of_boundary {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) {p : C.MorphismCoefficientPosition D} (hp : C.IsMorphismCoefficientBoundary D p) : C.morphismCoefficientAt D hC hD f p = 0

Every coefficient marked by an unmatched boundary is zero.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_eq_of_eqvGen {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) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.EqvGen (C.MorphismCoefficientStep D) p q) : C.morphismCoefficientAt D hC hD f p = C.morphismCoefficientAt D hC hD f q

Coefficients are constant on every equivalence component generated by matched-step edges.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_eq_zero_of_eqvGen_boundary {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) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.EqvGen (C.MorphismCoefficientStep D) p q) (hq : C.IsMorphismCoefficientBoundary D q) : C.morphismCoefficientAt D hC hD f p = 0

If a coefficient component reaches an unmatched boundary, every coefficient in that component vanishes.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_ne_zero_iff_of_eqvGen {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) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.EqvGen (C.MorphismCoefficientStep D) p q) : C.morphismCoefficientAt D hC hD f p ≠ 0 ↔ C.morphismCoefficientAt D hC hD f q ≠ 0

Nonvanishing is constant on a coefficient component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_boundary_of_morphismCoefficientAt_ne_zero_of_eqvGen {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) {p q : C.MorphismCoefficientPosition D} (hp : C.morphismCoefficientAt D hC hD f p ≠ 0) (hpq : Relation.EqvGen (C.MorphismCoefficientStep D) p q) : ¬C.IsMorphismCoefficientBoundary D q

A nonzero coefficient component contains no unmatched boundary.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isBoundaryFreeMorphismCoefficientComponent_of_ne_zero {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) (root : C.MorphismCoefficientPosition D) (hroot : C.morphismCoefficientAt D hC hD f root ≠ 0) : C.IsBoundaryFreeMorphismCoefficientComponent D root

The component of every nonzero coefficient of an actual morphism is boundary-free.