Diagonal coefficients of products of string graph-component maps

This file reduces a possible nonzero diagonal coefficient of a component-map product to a full-support oriented self-interval. The midpoint argument excluding a proper full-support interval is developed below.

@[instance_reducible]

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

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

A nonzero diagonal coefficient of a product of two component maps has an intermediate position supported by both components.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.firstComponent_full_inputSupport_of_comp_diagonal_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (first second : C.BoundaryFreeMorphismCoefficientComponent C) {x : Q} (i : C.PositionAt x) (hne : C.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap C hmono hmono first) (C.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (C.diagonalMorphismCoefficientPosition i) ≠ 0) {y : Q} (l : C.PositionAt y) : ∃ (j : C.PositionAt y), Relation.EqvGen (C.MorphismCoefficientStep C) (↑first).representative ⟨y, (l, j)⟩

If one diagonal coefficient of a component-map product is nonzero, the first component has a supported coefficient above every word position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.firstComponent_endpointIndices_of_comp_diagonal_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (first second : C.BoundaryFreeMorphismCoefficientComponent C) {x : Q} (i : C.PositionAt x) (hne : C.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap C hmono hmono first) (C.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (C.diagonalMorphismCoefficientPosition i) ≠ 0) : ∃ (j₀ : C.PositionAt C.source) (jₙ : C.PositionAt C.target), Relation.EqvGen (C.MorphismCoefficientStep C) (↑first).representative ⟨C.source, (C.sourcePosition, j₀)⟩ ∧ Relation.EqvGen (C.MorphismCoefficientStep C) (↑first).representative ⟨C.target, (C.targetPosition, jₙ)⟩ ∧ (j₀.index = 0 ∧ jₙ.index = length R C ∨ j₀.index = length R C ∧ jₙ.index = 0)

Full input support at the two word endpoints forces a full increasing or full decreasing interval correspondence.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_full_reversing_boundaryFreeComponent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (component : C.BoundaryFreeMorphismCoefficientComponent C) (hproper : ↑component ≠ C.diagonalMorphismCoefficientComponent) (j₀ : C.PositionAt C.source) (jₙ : C.PositionAt C.target) (hj₀ : Relation.EqvGen (C.MorphismCoefficientStep C) (↑component).representative ⟨C.source, (C.sourcePosition, j₀)⟩) (hjₙ : Relation.EqvGen (C.MorphismCoefficientStep C) (↑component).representative ⟨C.target, (C.targetPosition, jₙ)⟩) (hj₀Index : j₀.index = length R C) : False

A proper self-component cannot be a full reversal of the word-position interval. At an even midpoint it would meet the diagonal; at an odd midpoint it would match one word edge with the same edge traversed in the opposite direction.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_properComponentMap_comp_diagonal_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (first second : C.ProperBoundaryFreeMorphismCoefficientComponent) {x : Q} (i : C.PositionAt x) : C.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (C.properBoundaryFreeMorphismCoefficientComponentMap hmono first) (C.properBoundaryFreeMorphismCoefficientComponentMap hmono second)) (C.diagonalMorphismCoefficientPosition i) = 0

The product of two proper self-component basis maps has zero diagonal coordinate.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.diagonalMorphismCoefficientLinearMap_comp_eq_zero_of_mem_proper {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {f g : C.rightModule hmono ⟶ C.rightModule hmono} (hf : f ∈ C.properMorphismCoefficientComponentSubspace hmono) (hg : g ∈ C.properMorphismCoefficientComponentSubspace hmono) : (C.diagonalMorphismCoefficientLinearMap hmono) (CategoryTheory.CategoryStruct.comp f g) = 0

The diagonal coordinate vanishes on the composite of any two elements of the proper-component span.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.diagonalMorphismCoefficientLinearMap_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f g : C.rightModule hmono ⟶ C.rightModule hmono) : (C.diagonalMorphismCoefficientLinearMap hmono) (CategoryTheory.CategoryStruct.comp f g) = (C.diagonalMorphismCoefficientLinearMap hmono) f * (C.diagonalMorphismCoefficientLinearMap hmono) g

The diagonal graph coordinate is multiplicative on the full string endomorphism ring.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.properMorphismCoefficientComponentSubspace_comp_mem {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {f g : C.rightModule hmono ⟶ C.rightModule hmono} (hf : f ∈ C.properMorphismCoefficientComponentSubspace hmono) (hg : g ∈ C.properMorphismCoefficientComponentSubspace hmono) : CategoryTheory.CategoryStruct.comp f g ∈ C.properMorphismCoefficientComponentSubspace hmono

The proper-component subspace is closed under composition.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.properMorphismCoefficientComponentSubspace_comp_mem_of_mem_left {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {r f : C.rightModule hmono ⟶ C.rightModule hmono} (hr : r ∈ C.properMorphismCoefficientComponentSubspace hmono) : CategoryTheory.CategoryStruct.comp r f ∈ C.properMorphismCoefficientComponentSubspace hmono

The proper-component subspace is stable under postcomposition by an arbitrary endomorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.properMorphismCoefficientComponentSubspace_comp_mem_of_mem_right {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {f r : C.rightModule hmono ⟶ C.rightModule hmono} (hr : r ∈ C.properMorphismCoefficientComponentSubspace hmono) : CategoryTheory.CategoryStruct.comp f r ∈ C.properMorphismCoefficientComponentSubspace hmono

The proper-component subspace is stable under precomposition by an arbitrary endomorphism.