The canonical representation carried by a string word

The basis vectors of a string representation are the occurrences of vertices along the word. We represent an occurrence by the prefix ending there. This retains repeated visits to the same displayed vertex without choosing numeric coordinates.

A displayed arrow acts between two prefix occurrences when the word traverses that arrow positively between them, or traverses its formal inverse in the opposite direction. Reduction makes the resulting target occurrence unique.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.midpoint_eq_of_comp_eq_of_left_length_eq {V : Type u_1} [Quiver V] {s x y t : V} {p : Quiver.Path s x} {q : Quiver.Path x t} {p' : Quiver.Path s y} {q' : Quiver.Path y t} (hcomp : p.comp q = p'.comp q') (hlength : p.length = p'.length) : x = y

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positiveArrow_ne_negativeArrow {Q : Type u} [Quiver Q] {a b : Q} (e : a ⟶ b) (f : b ⟶ a) : positiveArrow e ≠ negativeArrow f

A positive signed arrow can never equal a negative signed arrow with the same signed endpoints.

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

An occurrence of x along a word, represented by the prefix ending at that occurrence.

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

The length of the prefix representing a position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositionAt.index_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} {x : Q} (i : C.PositionAt x) : i.index ≤ length R C

The prefix length of a position is at most the word length.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositionAt.eq_target_of_index_eq_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} {x : Q} (i : C.PositionAt x) (h : i.index = length R C) : x = C.target

A position at the final word index lies at the target vertex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositionAt.ext_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} {x : Q} {i j : C.PositionAt x} (h : i.index = j.index) : i = j

Two prefix positions at the same vertex with the same index coincide.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositionAt.indexEmbedding {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (x : Q) : C.PositionAt x ↪ Fin (length R C + 1)

Prefix length embeds the positions at a fixed displayed vertex into the finite interval of word indices.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.PositionAt.finite {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (x : Q) : Finite (C.PositionAt x)

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

A position anywhere along a word, retaining the displayed vertex over which it lies.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.Position.index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (i : C.Position) : ℕ

The prefix index of a total word position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Position.ext_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} {i j : C.Position} (h : i.index = j.index) : i = j

The prefix index determines a total position, including its displayed vertex.

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

Prefix index embeds all positions of a word into its finite index interval.

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

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

The position at the source endpoint of a string word.

@[simp]

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

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

The position at the target endpoint of a string word.

@[simp]

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_position_index_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (n : ℕ) (hn : n ≤ length R C) : ∃ (i : C.Position), i.index = n

Every index between zero and the word length is represented by a total word position.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.Position.indexEquiv {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : C.Position ≃ Fin (length R C + 1)

Total word positions are canonically indexed by the finite interval from zero through the word length.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Position.card_eq_length_add_one {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Nat.card C.Position = length R C + 1

@[reducible, inline]

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

The vertex space of the canonical string representation.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.ArrowStep {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) : Prop

A positive occurrence of a moves a basis position one step forward; an inverse occurrence moves it one step backward.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.ArrowStep.index {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) : j.index = i.index + 1 ∨ i.index = j.index + 1

An arrow step changes the prefix index by one, forward or backward.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_arrowStep_of_position_index_succ {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (i j : C.Position) (hindex : j.index = i.index + 1) : (∃ (a : i.fst ⟶ j.fst), C.ArrowStep a i.snd j.snd) ∨ ∃ (a : j.fst ⟶ i.fst), C.ArrowStep a j.snd i.snd

Two total positions at consecutive indices are joined by the displayed ordinary arrow, oriented according to the intervening signed letter.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_arrowStep_of_index_lt_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (i : C.Position) (hindex : i.index < length R C) : (∃ (y : Q) (j : C.PositionAt y) (a : i.fst ⟶ y), j.index = i.index + 1 ∧ C.ArrowStep a i.snd j) ∨ ∃ (y : Q) (j : C.PositionAt y) (a : y ⟶ i.fst), j.index = i.index + 1 ∧ C.ArrowStep a j i.snd

A position before the final index has an adjacent next position and a displayed arrow in one of the two ordinary orientations.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_arrowStep_of_index_pos {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (i : C.Position) (hindex : 0 < i.index) : (∃ (x : Q) (j : C.PositionAt x) (a : x ⟶ i.fst), j.index + 1 = i.index ∧ C.ArrowStep a j i.snd) ∨ ∃ (x : Q) (j : C.PositionAt x) (a : i.fst ⟶ x), j.index + 1 = i.index ∧ C.ArrowStep a i.snd j

A position after the initial index has an adjacent previous position and a displayed arrow in one of the two ordinary orientations.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrow_eq_of_arrowSteps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} {a b : x ⟶ y} {i : C.PositionAt x} {j : C.PositionAt y} (ha : C.ArrowStep a i j) (hb : C.ArrowStep b i j) : a = b

A fixed pair of adjacent word positions determines the displayed arrow between them.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_arrowSteps_reverse_of_index_add_one {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} {a : x ⟶ y} {b : y ⟶ x} {i : C.PositionAt x} {j : C.PositionAt y} (ha : C.ArrowStep a i j) (hb : C.ArrowStep b j i) (hindex : j.index = i.index + 1) : False

Two displayed-arrow steps cannot traverse the same word edge in opposite displayed directions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowStep_subsingleton {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) : Subsingleton { j : C.PositionAt y // C.ArrowStep a i j }

A string word has at most one target position for a displayed arrow from a fixed source position.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowOnBasis {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) : C.Space y

The image of one position-basis vector under a displayed arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowOnBasis_eq_single_of_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 = Finsupp.single j 1

At a witnessed arrow step, the corresponding basis vector is sent to the basis vector at that target position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowOnBasis_eq_zero_of_not_exists {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) (h : ¬∃ (j : C.PositionAt y), C.ArrowStep a i j) : C.arrowOnBasis a i = 0

If an arrow has no target occurrence from a basis position, that basis vector is killed.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowLinearMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) : C.Space x →ₗ[k] C.Space y

The linear map assigned to a displayed arrow by the canonical string representation.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowLinearMap_single {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) (c : k) : (C.arrowLinearMap a) (Finsupp.single i c) = c • C.arrowOnBasis a i

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowLinearMap_single_one_of_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.arrowLinearMap a) (Finsupp.single i 1) = Finsupp.single j 1

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteDimensional_space {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (x : Q) : FiniteDimensional k (C.Space x)

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PathReach {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} : Quiver.Path x y → C.PositionAt x → C.PositionAt y → Prop

Reachability of one word-position basis vector under an ordinary quiver path. Each arrow is allowed to use either its positive occurrence or the matching inverse occurrence in the word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_forward_cons_then_negative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {w x y z : Q} (p : Quiver.Path w x) (b : x ⟶ y) (a : y ⟶ z) (i : C.PositionAt w) (j : C.PositionAt y) (l : C.PositionAt z) (hforward : ↑j = Quiver.Path.comp (↑i) (positivePath (p.cons b))) (hnegative : ↑j = Quiver.Path.comp (↑l) (Quiver.Hom.toPath (negativeArrow a))) : False

A nonempty positive traversal cannot be followed by a backward arrow step: their final signed arrows would have opposite signs.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_backward_cons_then_positive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {w x y z : Q} (p : Quiver.Path w x) (b : x ⟶ y) (a : y ⟶ z) (i : C.PositionAt w) (j : C.PositionAt y) (l : C.PositionAt z) (hbackward : ↑i = Quiver.Path.comp (↑j) (Quiver.Path.reverse (positivePath (p.cons b)))) (hpositive : ↑l = Quiver.Path.comp (↑j) (Quiver.Hom.toPath (positiveArrow a))) : False

A nonempty backward traversal cannot be followed by a forward arrow step. Reversing the two competing suffixes reduces this to the preceding positive-versus-negative final-arrow contradiction.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pathReach_forward_or_backward {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) : C.PathReach p i j → ↑j = Quiver.Path.comp (↑i) (positivePath p) ∨ ↑i = Quiver.Path.comp (↑j) (Quiver.Path.reverse (positivePath p))

A reachable ordinary path moves monotonically along the word: it is realized either by the positive copy of the whole path or by the reversed positive copy in the opposite direction.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pathReach_contiguous_forward_or_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) (hij : C.PathReach p i j) : IsContiguousSubpath (positivePath p) C.path ∨ IsContiguousSubpath (positivePath p) (Quiver.Path.reverse C.path)

A reachable path occurs as one contiguous positive segment of the word or of its reverse.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pathMap_ne_zero_of_pathReach {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) (hij : C.PathReach p i j) : pathMap R p ≠ 0

Every ordinary path which acts nontrivially on a position basis survives the string-algebra relation quotient.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pathReach_subsingleton {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) : Subsingleton { j : C.PositionAt y // C.PathReach p i j }

Reduction makes the endpoint of a reachable path unique.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.pathOnBasis {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) : C.Space y

The image of a position-basis vector under a quiver path, expressed as the unique reachable basis vector when it exists.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pathOnBasis_eq_single_of_reach {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) (hij : C.PathReach p i j) : C.pathOnBasis p i = Finsupp.single j 1

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pathOnBasis_eq_zero_of_not_exists {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) (h : ¬∃ (j : C.PositionAt y), C.PathReach p i j) : C.pathOnBasis p i = 0

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.quiverRepresentation {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : LinearPathCategory.QuiverRep k Q

The canonical quiver representation of a string word before descending through the relation quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.quiverMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (p : Quiver.Path x y) : ModuleCat.of k (C.Space x) ⟶ ModuleCat.of k (C.Space y)

Evaluation of the canonical representation with the original displayed vertices pinned explicitly.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.quiverMap_nil {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (x : Q) : C.quiverMap Quiver.Path.nil = CategoryTheory.CategoryStruct.id (ModuleCat.of k (C.Space x))

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.quiverMap_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y z : Q} (p : Quiver.Path x y) (q : Quiver.Path y z) : C.quiverMap (p.comp q) = CategoryTheory.CategoryStruct.comp (C.quiverMap p) (C.quiverMap q)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.quiverRepresentation_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (x : Q) : C.quiverRepresentation.obj x = ModuleCat.of k (C.Space x)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.quiverRepresentation_map_toPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) : C.quiverRepresentation.map a.toPath = ModuleCat.ofHom (C.arrowLinearMap a)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.quiverMap_toPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (a : x ⟶ y) : C.quiverMap a.toPath = ModuleCat.ofHom (C.arrowLinearMap a)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowLinearMap_pathOnBasis {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y z : Q} (p : Quiver.Path x y) (a : y ⟶ z) (i : C.PositionAt x) : (C.arrowLinearMap a) (C.pathOnBasis p i) = C.pathOnBasis (p.cons a) i

Applying one more displayed arrow to the path image of a basis position agrees with extending position reachability by that arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.quiverRepresentation_map_single {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) (c : k) : (CategoryTheory.ConcreteCategory.hom (C.quiverRepresentation.map p)) (Finsupp.single i c) = c • C.pathOnBasis p i

Evaluation of an ordinary quiver path on a position-basis vector is the unique reachable basis vector, or zero when no such position exists.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.quiverRepresentation_map_eq_zero_of_pathMap_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (p : Quiver.Path x y) (hp : pathMap R p = 0) : C.quiverRepresentation.map p = 0

Every ordinary path killed by the relation quotient acts as zero on the canonical string representation.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.freeRightModuleAux {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : CategoryTheory.Functor (LinearPathCategory.Category k Q) (ModuleCat k)ᵒᵖ

The reversed linear realization of the canonical quiver representation as a right module over the free linear path category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.freeRightModuleAux_pathMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : Q} (p : Quiver.Path x y) : LinearPathCategory.pathMap (fun (x : Q) => Opposite.op (ModuleCat.of k (C.Space x))) (fun {i j : Q} (a : i ⟶ j) => (ModuleCat.ofHom (C.arrowLinearMap a)).op) p = (C.quiverMap p).op

Reversed path evaluation agrees with the opposite of evaluation in the canonical quiver representation.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.freeRightModuleAux_map_pathHom {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x y : LinearPathCategory.Category k Q} (p : Quiver.Path (LinearPathCategory.vertex y) (LinearPathCategory.vertex x)) : C.freeRightModuleAux.map (LinearPathCategory.pathHom p) = (C.quiverMap p).op

On a path-basis morphism, the free right-module realization is the opposite of the corresponding quiver-representation map.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.freeRightModuleAux_additive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : C.freeRightModuleAux.Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.freeRightModuleAux_linear {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : CategoryTheory.Functor.Linear k C.freeRightModuleAux

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.relationIdeal_isKilledBy {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : (LinearPathCategory.HomogeneousQuotient.relationIdeal R).IsKilledBy C.freeRightModuleAux

For a monomial presentation, the free realization of a string word kills the complete generated relation ideal.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.quotientRightModuleAux {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : CategoryTheory.Functor (Category R) (ModuleCat k)ᵒᵖ

The string-word realization descended through a monomial relation quotient, still written covariantly with values in the opposite module category.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.quotientRightModuleAux_additive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : (C.quotientRightModuleAux hmono).Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.quotientRightModuleAux_linear {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : CategoryTheory.Functor.Linear k (C.quotientRightModuleAux hmono)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightModule {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)

The canonical finite-dimensional right module represented by a string word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightModule_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (x : Q) : (C.rightModule hmono).obj (Opposite.op (obj R x)) = ModuleCat.of k (C.Space x)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightModule_map_pathMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {x y : Q} (p : Quiver.Path x y) : (C.rightModule hmono).map (pathMap R p).op = C.quiverMap p

The descended right module evaluates a quotient path by the canonical position-basis path map.