The diagonal component of the string endomorphism basis

For a self-word, all diagonal coefficient positions lie in one component. This file identifies the corresponding component-indicator map with the identity endomorphism and proves that every other boundary-free component map has zero diagonal.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_id_diagonal {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : C.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.id (C.rightModule hmono)) (C.diagonalMorphismCoefficientPosition i) = 1

Every diagonal coefficient of the identity is one.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_id_eq_zero_of_ne {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {x : Q} (i j : C.PositionAt x) (hij : i ≠ j) : C.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.id (C.rightModule hmono)) ⟨x, (i, j)⟩ = 0

An off-diagonal coefficient of the identity is zero.

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

The equality component containing all diagonal positions of a self-word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponentOf_diagonal {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (i : C.PositionAt x) : C.morphismCoefficientComponentOf C (C.diagonalMorphismCoefficientPosition i) = C.diagonalMorphismCoefficientComponent

Every diagonal coefficient position represents the diagonal component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.diagonalMorphismCoefficientComponent_representative_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Relation.EqvGen (C.MorphismCoefficientStep C) C.diagonalMorphismCoefficientComponent.representative (C.diagonalMorphismCoefficientPosition C.sourcePosition)

The chosen representative of the diagonal component is connected to the source diagonal position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_diagonalComponent_representative_eq_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ C.rightModule hmono) : C.morphismCoefficientAt C hmono hmono f C.diagonalMorphismCoefficientComponent.representative = C.morphismCoefficientAt C hmono hmono f (C.diagonalMorphismCoefficientPosition C.sourcePosition)

Every endomorphism has the same coefficient at the chosen diagonal component representative and at the source diagonal position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_id_diagonalComponent_representative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : C.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.id (C.rightModule hmono)) C.diagonalMorphismCoefficientComponent.representative = 1

The identity has coefficient one at the chosen representative of the diagonal component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.diagonalMorphismCoefficientComponent_isBoundaryFree {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : C.IsBoundaryFreeMorphismCoefficientComponent C C.diagonalMorphismCoefficientComponent.representative

The diagonal component cannot meet an unmatched-step zero boundary.

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

The diagonal component as an index in the graph-component basis.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_representative_eqvGen_diagonal_of_ne {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (component : C.MorphismCoefficientComponent C) (hne : component ≠ C.diagonalMorphismCoefficientComponent) {x : Q} (i : C.PositionAt x) : ¬Relation.EqvGen (C.MorphismCoefficientStep C) component.representative (C.diagonalMorphismCoefficientPosition i)

A component different from the diagonal component contains no diagonal coefficient position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_boundaryFreeComponentMap_diagonal_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (component : C.BoundaryFreeMorphismCoefficientComponent C) (hne : ↑component ≠ C.diagonalMorphismCoefficientComponent) {x : Q} (i : C.PositionAt x) : C.morphismCoefficientAt C hmono hmono (C.boundaryFreeMorphismCoefficientComponentMap C hmono hmono component) (C.diagonalMorphismCoefficientPosition i) = 0

Every non-diagonal graph-component basis vector has zero diagonal coefficient.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientComponentMap_diagonal_eq_id {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : C.boundaryFreeMorphismCoefficientComponentMap C hmono hmono (C.diagonalBoundaryFreeMorphismCoefficientComponent hmono) = CategoryTheory.CategoryStruct.id (C.rightModule hmono)

The graph-component basis vector indexed by the diagonal component is the identity endomorphism.