Aligned positions in string graph-component factorizations

When a graph-component product is nonzero on an output component, a full support hypothesis identifies the outside position before the intermediate position is extracted. This strengthens mere support transfer to a pointwise alignment of the two selected factor components along the entire output interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.exists_intermediate_of_comp_of_fullOutputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (output : C.BoundaryFreeMorphismCoefficientComponent E) (houtput : output.HasFullOutputSupport) (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E) (hne : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second)) (↑output).representative ≠ 0) {x : Q} (l : E.PositionAt x) : ∃ (j : D.PositionAt x), Relation.EqvGen (C.MorphismCoefficientStep D) (↑first).representative ⟨x, (output.inputPosition ⋯ l, j)⟩ ∧ Relation.EqvGen (D.MorphismCoefficientStep E) (↑second).representative ⟨x, (j, l)⟩

Full target support of the output component aligns both selected factor components above every target position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.exists_intermediate_of_comp_of_fullInputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (output : C.BoundaryFreeMorphismCoefficientComponent E) (hinput : output.HasFullInputSupport) (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E) (hne : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second)) (↑output).representative ≠ 0) {x : Q} (i : C.PositionAt x) : ∃ (j : D.PositionAt x), Relation.EqvGen (C.MorphismCoefficientStep D) (↑first).representative ⟨x, (i, j)⟩ ∧ Relation.EqvGen (D.MorphismCoefficientStep E) (↑second).representative ⟨x, (j, output.outputPosition ⋯ i)⟩

Full source support of the output component aligns both selected factor components below every source position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rightModuleProjectionComponent_inputPosition_eq_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : (extension.rightModuleProjectionComponent hmono).inputPosition ⋯ i = extension.toRightExtension.position i

The input selected by the right-boundary projection component is the inherited position in the extended word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rightModuleInclusionComponent_outputPosition_eq_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : (extension.rightModuleInclusionComponent hmono).outputPosition ⋯ i = extension.toRightExtension.position i

The output selected by the right-boundary inclusion component is the inherited position in the extended word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.moduleMapComponent_inputPosition_eq_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : (extension.moduleMapComponent hmono).inputPosition ⋯ i = extension.position i

The input selected by the positive left-boundary projection component is the inherited position in the extended word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.moduleMapComponent_outputPosition_eq_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : (extension.moduleMapComponent hmono).outputPosition ⋯ i = extension.position i

The output selected by the negative left-boundary inclusion component is the inherited position in the extended word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.exists_intermediate_of_component_pair {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (first : D.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent C) (hne : D.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (D.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (↑(hook.moduleMapComponent hmono)).representative ≠ 0) {x : Q} (i : C.PositionAt x) : ∃ (j : M.PositionAt x), Relation.EqvGen (D.MorphismCoefficientStep M) (↑first).representative ⟨x, (hook.toPositiveBoundaryExtension.toRightExtension.position i, j)⟩ ∧ Relation.EqvGen (M.MorphismCoefficientStep C) (↑second).representative ⟨x, (j, i)⟩

A nonzero component product over a right hook aligns both factor components at every inherited position of the old word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.exists_intermediate_of_component_pair {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (first : C.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent D) (hne : C.morphismCoefficientAt D hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap D hmono hmono second)) (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) {x : Q} (i : C.PositionAt x) : ∃ (j : M.PositionAt x), Relation.EqvGen (C.MorphismCoefficientStep M) (↑first).representative ⟨x, (i, j)⟩ ∧ Relation.EqvGen (M.MorphismCoefficientStep D) (↑second).representative ⟨x, (j, cohook.toNegativeBoundaryExtension.toRightExtension.position i)⟩

A nonzero component product over a right cohook aligns both factor components at every inherited position of the old word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.exists_intermediate_of_component_pair {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C M : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) (first : hook.result.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent C) (hne : hook.result.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (hook.result.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (↑(hook.moduleMapComponent hmono)).representative ≠ 0) {x : Q} (i : C.PositionAt x) : ∃ (j : M.PositionAt x), Relation.EqvGen (hook.result.MorphismCoefficientStep M) (↑first).representative ⟨x, (hook.toLeftPositiveBoundaryExtension.position i, j)⟩ ∧ Relation.EqvGen (M.MorphismCoefficientStep C) (↑second).representative ⟨x, (j, i)⟩

A nonzero component product over a left hook aligns both factor components at every inherited position of the old word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.exists_intermediate_of_component_pair {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C M : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) (first : C.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent cohook.result) (hne : C.morphismCoefficientAt cohook.result hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap cohook.result hmono hmono second)) (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) {x : Q} (i : C.PositionAt x) : ∃ (j : M.PositionAt x), Relation.EqvGen (C.MorphismCoefficientStep M) (↑first).representative ⟨x, (i, j)⟩ ∧ Relation.EqvGen (M.MorphismCoefficientStep cohook.result) (↑second).representative ⟨x, (j, cohook.toLeftNegativeBoundaryExtension.position i)⟩

A nonzero component product over a left cohook aligns both factor components at every inherited position of the old word.