Full-support string graph components

The constant-slope interval normal form gives exact endpoint displacement for a component which covers a whole source or target word. In particular, full source support forces the source word no longer than the target word, full target support gives the opposite inequality, and two-sided full support forces equal word lengths.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.exists_endpointPositions {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) : ∃ (j₀ : D.PositionAt C.source) (jₙ : D.PositionAt C.target), Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨C.source, (C.sourcePosition, j₀)⟩ ∧ Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨C.target, (C.targetPosition, jₙ)⟩ ∧ (jₙ.index = j₀.index + length R C ∨ j₀.index = jₙ.index + length R C)

A component covering its complete source word embeds the source position line as one increasing or decreasing interval in the target word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.source_length_le_target_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) : length R C ≤ length R D

Full source support forces the source word no longer than the target word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.exists_endpointPositions {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) : ∃ (i₀ : C.PositionAt D.source) (iₙ : C.PositionAt D.target), Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨D.source, (i₀, D.sourcePosition)⟩ ∧ Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨D.target, (iₙ, D.targetPosition)⟩ ∧ (iₙ.index = i₀.index + length R D ∨ i₀.index = iₙ.index + length R D)

A component covering its complete target word embeds the target position line as one increasing or decreasing interval in the source word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.target_length_le_source_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) : length R D ≤ length R C

Full target support forces the target word no longer than the source word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.length_eq_of_fullSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) (houtput : component.HasFullOutputSupport) : length R C = length R D

A component with full support on both words connects words of equal length.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.hasFullInputSupport_of_length_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) (hlength : length R C = length R D) : component.HasFullInputSupport

At equal word length, full target support already covers the complete source word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.hasFullOutputSupport_of_length_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) (hlength : length R C = length R D) : component.HasFullOutputSupport

At equal word length, full source support already covers the complete target word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.inputPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (houtput : component.HasFullOutputSupport) {x : Q} (j : D.PositionAt x) : C.PositionAt x

The unique source position supported below a given target position of a full-output-support component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.inputPosition_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (houtput : component.HasFullOutputSupport) {x : Q} (j : D.PositionAt x) : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨x, (component.inputPosition ⋯ j, j)⟩

The selected input position belongs to the component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.inputPosition_eq_of_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (houtput : component.HasFullOutputSupport) {x : Q} (j : D.PositionAt x) (i : C.PositionAt x) (hi : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨x, (i, j)⟩) : component.inputPosition ⋯ j = i

The selected input is the only input supported below the given target position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.inputPosition_injective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (houtput : component.HasFullOutputSupport) {x : Q} : Function.Injective (component.inputPosition ⋯)

A component's selected input-position map is injective.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.outputPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) {x : Q} (i : C.PositionAt x) : D.PositionAt x

The unique target position supported above a given source position of a full-input-support component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.outputPosition_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨x, (i, component.outputPosition ⋯ i)⟩

The selected output position belongs to the component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.outputPosition_eq_of_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) {x : Q} (i : C.PositionAt x) (j : D.PositionAt x) (hj : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨x, (i, j)⟩) : component.outputPosition ⋯ i = j

The selected output is the only output supported above the given source position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.outputPosition_injective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) {x : Q} : Function.Injective (component.outputPosition ⋯)

A component's selected output-position map is injective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.outputPosition_surjective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) (houtput : component.HasFullOutputSupport) {x : Q} : Function.Surjective (component.outputPosition ⋯)

Full output support makes the selected output-position map surjective.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.outputPositionEquiv {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) (houtput : component.HasFullOutputSupport) (x : Q) : C.PositionAt x ≃ D.PositionAt x

Two-sided full support gives a position equivalence on every displayed vertex.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.outputPositionEquiv_apply {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) (houtput : component.HasFullOutputSupport) {x : Q} (i : C.PositionAt x) : (component.outputPositionEquiv ⋯ ⋯ x) i = component.outputPosition ⋯ i

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.coefficientComponentOnBasis_eq_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) {x : Q} (i : C.PositionAt x) : C.coefficientComponentOnBasis D (↑component).representative i = Finsupp.single (component.outputPosition ⋯ i) 1

On a source basis position, a full-input component indicator is the single target basis vector selected above it.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.coefficientComponentLinearMap_eq_domLCongr {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hinput : component.HasFullInputSupport) (houtput : component.HasFullOutputSupport) (x : Q) : C.coefficientComponentLinearMap D (↑component).representative x = ↑(Finsupp.domLCongr (component.outputPositionEquiv ⋯ ⋯ x))

With two-sided full support, the component indicator linear map is the coordinate permutation induced by the position equivalence.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.isIso_componentMap_of_fullSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hC hD : IsMonomial R) (hinput : component.HasFullInputSupport) (houtput : component.HasFullOutputSupport) : CategoryTheory.IsIso (C.boundaryFreeMorphismCoefficientComponentMap D hC hD component)

A graph-component basis map with full support on both words is an isomorphism of right modules.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.inv_componentMap_app_eq_domLCongr_symm {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hC hD : IsMonomial R) (hinput : component.HasFullInputSupport) (houtput : component.HasFullOutputSupport) (x : Q) : let map := C.boundaryFreeMorphismCoefficientComponentMap D hC hD component; (CategoryTheory.inv map).app (Opposite.op (obj R x)) = ModuleCat.ofHom ↑(Finsupp.domLCongr (component.outputPositionEquiv ⋯ ⋯ x)).symm

The inverse of a two-sided full-support component map is the inverse coordinate permutation at every displayed vertex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.morphismCoefficientAt_comp_inv_componentMap_diagonal {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hC hD : IsMonomial R) (hinput : component.HasFullInputSupport) (houtput : component.HasFullOutputSupport) (f : C.rightModule hC ⟶ D.rightModule hD) {x : Q} (i : C.PositionAt x) : let map := C.boundaryFreeMorphismCoefficientComponentMap D hC hD component; C.morphismCoefficientAt C hC hC (CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv map)) (C.diagonalMorphismCoefficientPosition i) = C.morphismCoefficientAt D hC hD f ⟨x, (i, component.outputPosition ⋯ i)⟩

Postcomposing with the inverse full-support component map turns its selected coefficient into the corresponding diagonal coefficient.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.isIso_of_morphismCoefficientAt_ne_zero_of_fullSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hC hD : IsMonomial R) (hinput : component.HasFullInputSupport) (houtput : component.HasFullOutputSupport) (f : C.rightModule hC ⟶ D.rightModule hD) (hcoefficient : C.morphismCoefficientAt D hC hD f (↑component).representative ≠ 0) : CategoryTheory.IsIso f

Any string-module morphism with a nonzero coefficient on a two-sided full-support component is an isomorphism.