Nilpotence of proper string graph components

Proper component maps define directed partial-bijection steps on the finite set of positions above each displayed vertex. The proper ideal has no directed position cycle: a cycle would produce an element of the ideal with diagonal coefficient one. Conversely, every nonzero coefficient of a power of an element of the ideal produces a position chain of the same length. Pigeonhole therefore gives a uniform nilpotence bound.

@[instance_reducible]

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

def MagnitudeConjecture.BoundQuiver.StringWord.Word.ProperMorphismCoefficientStepAt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {x : Q} (i j : C.PositionAt x) : Prop

A directed position step supported by one proper self-component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_properMorphismCoefficientComponentSubspace_rowWitness_of_step {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 : C.ProperMorphismCoefficientStepAt i j) : ∃ f ∈ C.properMorphismCoefficientComponentSubspace hmono, C.morphismCoefficientAt C hmono hmono f ⟨x, (i, j)⟩ = 1 ∧ ∀ (t : C.PositionAt x), C.morphismCoefficientAt C hmono hmono f ⟨x, (i, t)⟩ ≠ 0 → t = j

A single proper-component step is realized by an element of the proper ideal with coefficient one and with no other nonzero coefficient in that input row.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_properMorphismCoefficientComponentSubspace_rowWitness_of_transGen {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 : Relation.TransGen C.ProperMorphismCoefficientStepAt i j) : ∃ f ∈ C.properMorphismCoefficientComponentSubspace hmono, C.morphismCoefficientAt C hmono hmono f ⟨x, (i, j)⟩ = 1 ∧ ∀ (t : C.PositionAt x), C.morphismCoefficientAt C hmono hmono f ⟨x, (i, t)⟩ ≠ 0 → t = j

Row witnesses compose: the product still has coefficient one at the chosen endpoint and a unique nonzero entry in the chosen input row.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.properMorphismCoefficientStepAt_transGen_irrefl {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : ¬Relation.TransGen C.ProperMorphismCoefficientStepAt i i

The directed relation generated by proper graph components has no cycle above any displayed vertex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.properMorphismCoefficientStepAt_of_mem_of_coefficient_ne_zero {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} (hf : f ∈ C.properMorphismCoefficientComponentSubspace hmono) {x : Q} {i j : C.PositionAt x} (hne : C.morphismCoefficientAt C hmono hmono f ⟨x, (i, j)⟩ ≠ 0) : C.ProperMorphismCoefficientStepAt i j

A nonzero coefficient of an element of the proper span is supported by at least one proper component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_properMorphismCoefficientStepAt_chain_of_pow_coefficient_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {f : CategoryTheory.End (C.rightModule hmono)} (hf : f ∈ C.properMorphismCoefficientComponentSubspace hmono) (n : ℕ) {x : Q} (i j : C.PositionAt x) (hne : C.morphismCoefficientAt C hmono hmono (f ^ n) ⟨x, (i, j)⟩ ≠ 0) : ∃ (positions : List (C.PositionAt x)), positions.length = n ∧ List.IsChain C.ProperMorphismCoefficientStepAt (i :: positions)

A nonzero coefficient of the nth power of an element of the proper span produces a directed position chain of exactly n steps.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pow_length_add_one_eq_zero_of_mem_properMorphismCoefficientComponentSubspace {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f : CategoryTheory.End (C.rightModule hmono)) (hf : f ∈ C.properMorphismCoefficientComponentSubspace hmono) : f ^ (length R C + 1) = 0

The uniform nilpotence bound for the proper-component ideal: the number of word positions annihilates every element.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isNilpotent_of_mem_properMorphismCoefficientComponentSubspace {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f : CategoryTheory.End (C.rightModule hmono)) (hf : f ∈ C.properMorphismCoefficientComponentSubspace hmono) : IsNilpotent f

Every element of the proper-component ideal is nilpotent, with the uniform exponent C.length + 1.