Path transfer along full-support string graph components #
A full-source-support coefficient component matches every displayed arrow step of its source word. Once the endpoint slope is fixed, the selected target positions therefore contain either the source word itself or its reverse as a literal contiguous signed subpath.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.outputPosition_arrowStep
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullInputSupport)
{x y : Q}
(a : x ⟶ y)
(i : C.PositionAt x)
(j : C.PositionAt y)
(hstep : C.ArrowStep a i j)
:
D.ArrowStep a (component.outputPosition ⋯ i) (component.outputPosition ⋯ j)
The positions selected by a full-input-support component preserve every displayed-arrow step of the source word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.outputPosition_index_eq_source_add_of_forward
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullInputSupport)
(hforward :
(component.outputPosition ⋯ C.targetPosition).index = (component.outputPosition ⋯ C.sourcePosition).index + length R C)
{x : Q}
(i : C.PositionAt x)
:
(component.outputPosition ⋯ i).index = (component.outputPosition ⋯ C.sourcePosition).index + i.index
In the forward endpoint orientation, every selected target index is the selected source index plus the corresponding source-word index.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.outputPosition_index_add_eq_source_of_reverse
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullInputSupport)
(hreverse :
(component.outputPosition ⋯ C.sourcePosition).index = (component.outputPosition ⋯ C.targetPosition).index + length R C)
{x : Q}
(i : C.PositionAt x)
:
(component.outputPosition ⋯ i).index + i.index = (component.outputPosition ⋯ C.sourcePosition).index
In the reverse endpoint orientation, every selected target index is the selected source index minus the corresponding source-word index.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.outputPosition_prefix_eq_of_forward_decomposition
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullInputSupport)
(hforward :
(component.outputPosition ⋯ C.targetPosition).index = (component.outputPosition ⋯ C.sourcePosition).index + length R C)
{x : Quiver.Symmetrify Q}
(p : Quiver.Path C.source x)
(q : Quiver.Path x C.target)
(hpq : C.path = p.comp q)
:
↑(component.outputPosition ⋯ ⟨p, ⋯⟩) = Quiver.Path.comp (↑(component.outputPosition ⋯ C.sourcePosition)) p
In the forward orientation, the prefix of every selected target position is the selected source prefix followed by the corresponding source prefix.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.outputPosition_prefix_eq_of_forward
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullInputSupport)
(hforward :
(component.outputPosition ⋯ C.targetPosition).index = (component.outputPosition ⋯ C.sourcePosition).index + length R C)
{x : Q}
(i : C.PositionAt x)
:
↑(component.outputPosition ⋯ i) = Quiver.Path.comp ↑(component.outputPosition ⋯ C.sourcePosition) ↑i
In the forward orientation, selected prefixes literally contain the corresponding source prefixes.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.outputPosition_source_prefix_eq_comp_reverse_decomposition
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullInputSupport)
(hreverse :
(component.outputPosition ⋯ C.sourcePosition).index = (component.outputPosition ⋯ C.targetPosition).index + length R C)
{x : Quiver.Symmetrify Q}
(p : Quiver.Path C.source x)
(q : Quiver.Path x C.target)
(hpq : C.path = p.comp q)
:
↑(component.outputPosition ⋯ C.sourcePosition) = Quiver.Path.comp (↑(component.outputPosition ⋯ ⟨p, ⋯⟩)) p.reverse
In the reverse orientation, the selected source prefix is the selected
prefix at p followed by the reverse of p.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.outputPosition_source_prefix_eq_comp_reverse
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullInputSupport)
(hreverse :
(component.outputPosition ⋯ C.sourcePosition).index = (component.outputPosition ⋯ C.targetPosition).index + length R C)
{x : Q}
(i : C.PositionAt x)
:
↑(component.outputPosition ⋯ C.sourcePosition) = Quiver.Path.comp (↑(component.outputPosition ⋯ i)) (Quiver.Path.reverse ↑i)
In the reverse orientation, selected prefixes literally contain reversed source prefixes.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.isString_comp_negative_of_forward_of_target_step
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullInputSupport)
(hforward :
(component.outputPosition ⋯ C.targetPosition).index = (component.outputPosition ⋯ C.sourcePosition).index + length R C)
{z : Q}
(a : z ⟶ C.target)
(j : D.PositionAt z)
(hindex : j.index = (component.outputPosition ⋯ C.targetPosition).index + 1)
(hstep : D.ArrowStep a j (component.outputPosition ⋯ C.targetPosition))
:
IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))
In the forward orientation, one further incoming arrow after the selected target endpoint gives a valid negative extension of the source word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.isString_comp_negative_of_reverse_of_target_step
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullInputSupport)
(hreverse :
(component.outputPosition ⋯ C.sourcePosition).index = (component.outputPosition ⋯ C.targetPosition).index + length R C)
{z : Q}
(a : z ⟶ C.target)
(j : D.PositionAt z)
(hindex : j.index + 1 = (component.outputPosition ⋯ C.targetPosition).index)
(hstep : D.ArrowStep a j (component.outputPosition ⋯ C.targetPosition))
:
IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow a)))
In the reverse orientation, one further incoming arrow before the selected target endpoint gives the same valid negative extension after reversing the ambient contiguous subpath.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.inputPosition_arrowStep
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullOutputSupport)
{x y : Q}
(a : x ⟶ y)
(i : D.PositionAt x)
(j : D.PositionAt y)
(hstep : D.ArrowStep a i j)
:
C.ArrowStep a (component.inputPosition ⋯ i) (component.inputPosition ⋯ j)
The positions selected by a full-output-support component preserve every displayed-arrow step of the target word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.inputPosition_index_eq_source_add_of_forward
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullOutputSupport)
(hforward :
(component.inputPosition ⋯ D.targetPosition).index = (component.inputPosition ⋯ D.sourcePosition).index + length R D)
{x : Q}
(i : D.PositionAt x)
:
(component.inputPosition ⋯ i).index = (component.inputPosition ⋯ D.sourcePosition).index + i.index
In the forward endpoint orientation, every selected source index is the selected target-source index plus the corresponding target-word index.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.inputPosition_index_add_eq_source_of_reverse
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullOutputSupport)
(hreverse :
(component.inputPosition ⋯ D.sourcePosition).index = (component.inputPosition ⋯ D.targetPosition).index + length R D)
{x : Q}
(i : D.PositionAt x)
:
(component.inputPosition ⋯ i).index + i.index = (component.inputPosition ⋯ D.sourcePosition).index
In the reverse endpoint orientation, every selected source index plus the corresponding target-word index is the selected target-source index.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.inputPosition_prefix_eq_of_forward_decomposition
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullOutputSupport)
(hforward :
(component.inputPosition ⋯ D.targetPosition).index = (component.inputPosition ⋯ D.sourcePosition).index + length R D)
{x : Quiver.Symmetrify Q}
(p : Quiver.Path D.source x)
(q : Quiver.Path x D.target)
(hpq : D.path = p.comp q)
:
↑(component.inputPosition ⋯ ⟨p, ⋯⟩) = Quiver.Path.comp (↑(component.inputPosition ⋯ D.sourcePosition)) p
In the forward orientation, the prefix of every selected source position is the selected target-source prefix followed by the corresponding target prefix.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.inputPosition_prefix_eq_of_forward
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullOutputSupport)
(hforward :
(component.inputPosition ⋯ D.targetPosition).index = (component.inputPosition ⋯ D.sourcePosition).index + length R D)
{x : Q}
(i : D.PositionAt x)
:
↑(component.inputPosition ⋯ i) = Quiver.Path.comp ↑(component.inputPosition ⋯ D.sourcePosition) ↑i
In the forward orientation, selected source prefixes literally contain the corresponding target prefixes.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.inputPosition_source_prefix_eq_comp_reverse_decomposition
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullOutputSupport)
(hreverse :
(component.inputPosition ⋯ D.sourcePosition).index = (component.inputPosition ⋯ D.targetPosition).index + length R D)
{x : Quiver.Symmetrify Q}
(p : Quiver.Path D.source x)
(q : Quiver.Path x D.target)
(hpq : D.path = p.comp q)
:
↑(component.inputPosition ⋯ D.sourcePosition) = Quiver.Path.comp (↑(component.inputPosition ⋯ ⟨p, ⋯⟩)) p.reverse
In the reverse orientation, the selected target-source prefix is the
selected prefix at p followed by the reverse of p.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.inputPosition_source_prefix_eq_comp_reverse
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullOutputSupport)
(hreverse :
(component.inputPosition ⋯ D.sourcePosition).index = (component.inputPosition ⋯ D.targetPosition).index + length R D)
{x : Q}
(i : D.PositionAt x)
:
↑(component.inputPosition ⋯ D.sourcePosition) = Quiver.Path.comp (↑(component.inputPosition ⋯ i)) (Quiver.Path.reverse ↑i)
In the reverse orientation, selected source prefixes literally contain reversed target prefixes.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.isString_comp_positive_of_forward_of_target_step
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullOutputSupport)
(hforward :
(component.inputPosition ⋯ D.targetPosition).index = (component.inputPosition ⋯ D.sourcePosition).index + length R D)
{z : Q}
(a : D.target ⟶ z)
(j : C.PositionAt z)
(hindex : j.index = (component.inputPosition ⋯ D.targetPosition).index + 1)
(hstep : C.ArrowStep a (component.inputPosition ⋯ D.targetPosition) j)
:
IsString R (Quiver.Path.comp D.path (Quiver.Hom.toPath (positiveArrow a)))
In the forward orientation, one further outgoing arrow after the selected target endpoint gives a valid positive extension of the target word.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.isString_comp_positive_of_reverse_of_target_step
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{C D : Word R}
(component : C.BoundaryFreeMorphismCoefficientComponent D)
(hfull : component.HasFullOutputSupport)
(hreverse :
(component.inputPosition ⋯ D.sourcePosition).index = (component.inputPosition ⋯ D.targetPosition).index + length R D)
{z : Q}
(a : D.target ⟶ z)
(j : C.PositionAt z)
(hindex : j.index + 1 = (component.inputPosition ⋯ D.targetPosition).index)
(hstep : C.ArrowStep a (component.inputPosition ⋯ D.targetPosition) j)
:
IsString R (Quiver.Path.comp D.path (Quiver.Hom.toPath (positiveArrow a)))
In the reverse orientation, one further outgoing arrow before the selected target endpoint gives the same valid positive extension after reversing the ambient contiguous subpath.