Interval structure of string coefficient components

Orienting every matched coefficient edge by increasing source-word index makes the edge relation a partial bijection. Church--Rosser then shows that each connected coefficient component embeds in both word-position lines. This is the graph-theoretic core of identifying graph-map components with oriented common intervals.

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

The matched coefficient edges, oriented by increasing source-word index.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientForwardStep_rightUnique {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Relator.RightUnique (C.MorphismCoefficientForwardStep D)

An oriented coefficient edge has at most one successor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientForwardStep_leftUnique {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Relator.LeftUnique (C.MorphismCoefficientForwardStep D)

An oriented coefficient edge has at most one predecessor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientForwardStep_or_reverse {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.SymmGen (C.MorphismCoefficientStep D) p q) : C.MorphismCoefficientForwardStep D p q ∨ C.MorphismCoefficientForwardStep D q p

Every unoriented matched edge has a unique orientation by increasing source-word index.

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

Matched-step connectivity is generated by the forward-oriented edge relation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_common_morphismCoefficientForwardStep_of_eqvGen {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.EqvGen (C.MorphismCoefficientStep D) p q) : ∃ (r : C.MorphismCoefficientPosition D), Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p r ∧ Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) q r

Two vertices in one coefficient component have a common descendant for the forward-oriented relation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.inputIndex_le_of_reflTransGen_morphismCoefficientForwardStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p q) : p.inputIndex ≤ q.inputIndex

A forward coefficient walk weakly increases the source-word index.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.eq_of_reflTransGen_morphismCoefficientForwardStep_of_inputIndex_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p q) (hindex : p.inputIndex = q.inputIndex) : p = q

A forward coefficient walk whose endpoints have equal source index is reflexive.

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

A connected coefficient component contains at most one vertex above each source-word position.

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

Transpose a coefficient position by interchanging its two word positions.

@[simp]

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

@[simp]

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

@[simp]

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.MorphismCoefficientStep.transpose {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) : D.MorphismCoefficientStep C ((C.morphismCoefficientPositionTranspose D) p) ((C.morphismCoefficientPositionTranspose D) q)

Transposition preserves one matched coefficient edge.

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

Transposition preserves generated coefficient components.

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

A connected coefficient component contains at most one vertex above each target-word position.

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

The vertices in the generated coefficient component of a chosen root.

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

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

A coefficient component embeds into the source word's finite position line.

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

A coefficient component embeds into the target word's finite position line.