Sectional paths

Proof of Proposition 4.1, Step 1 (periodic-mesh-calculations.tex): "A path is sectional if it contains no consecutive pair (σa)a. A sectional path cannot occur as a monomial term in a contextual mesh relation. Its coefficient therefore defines a linear functional annihilating the mesh ideal, and the path is nonzero in the mesh category. Since the mesh category is finite-dimensional, there is an integer N such that all paths of length at least N vanish. Hence every sectional path has length less than N."

A path is recorded by its list of arrows (arrowList), and it is sectional when no two consecutive arrows form a mesh pair (σ a, a).

def Quiver.Path.arrowList {V : Type v} [Quiver V] {x y : V} : Path x y → List ((u : V) × (v : V) × (u ⟶ v))

The arrows of a path, in order.

@[simp]

theorem Quiver.Path.arrowList_nil {V : Type v} [Quiver V] (x : V) : nil.arrowList = []

@[simp]

theorem Quiver.Path.arrowList_cons {V : Type v} [Quiver V] {x y z : V} (p : Path x y) (a : y ⟶ z) : (p.cons a).arrowList = p.arrowList ++ [⟨y, ⟨z, a⟩⟩]

@[simp]

theorem Quiver.Path.arrowList_comp {V : Type v} [Quiver V] {x y z : V} (p : Path x y) (q : Path y z) : (p.comp q).arrowList = p.arrowList ++ q.arrowList

@[simp]

theorem Quiver.Path.arrowList_toPath {V : Type v} [Quiver V] {x y : V} (a : x ⟶ y) : a.toPath.arrowList = [⟨x, ⟨y, a⟩⟩]

def MultiplicativeBasisDeformations.TranslationQuiver.IsMeshPair {V : Type v} [Quiver V] (Q : TranslationQuiver V) (b a : (u : V) × (v : V) × (u ⟶ v)) : Prop

Two consecutive arrows b, a form a mesh pair if b = σ a.

def MultiplicativeBasisDeformations.TranslationQuiver.IsSectional {V : Type v} [Quiver V] (Q : TranslationQuiver V) {x y : V} (p : Quiver.Path x y) : Prop

A path is sectional if no two consecutive arrows form a mesh pair.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.not_isSectional_of_mesh {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {s t : V} (x : ↑Q.nonprojective) {y : V} (a : y ⟶ ↑x) (q : Quiver.Path s ↑(Q.tau x)) (q' : Quiver.Path (↑x) t) : ¬Q.IsSectional ((q.comp (((Q.mate x y) a).toPath.comp a.toPath)).comp q')

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.coeff_eq_zero_of_mem_ideal {V : Type v} [Quiver V] {k : Type u} [Field k] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x y : V} (p : Quiver.Path x y) (hp : Q.IsSectional p) {f : LinearPaths.obj x ⟶ LinearPaths.obj y} (hf : f ∈ CategoricalIdeal.HomIdeal.generatedHomSubmodule k (meshRelations c) (LinearPaths.obj x) (LinearPaths.obj y)) : (LinearPaths.toFinsupp f) p = 0

A sectional path does not occur in the mesh ideal: its coefficient vanishes on the whole ideal.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.pathMor_ne_zero_of_isSectional {V : Type v} [Quiver V] {k : Type u} [Field k] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x y : V} (p : Quiver.Path x y) (hp : Q.IsSectional p) : pathMor c p ≠ 0

A sectional path is nonzero in the mesh category.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.exists_length_lt_of_isSectional {V : Type v} [Quiver V] {k : Type u} [Field k] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Finite V] (hfin : ∀ (x y : V), FiniteDimensional k (obj c x ⟶ obj c y)) : ∃ (N : ℕ), ∀ (x y : V) (p : Quiver.Path x y), Q.IsSectional p → p.length < N

Sectional paths are short in a finite-dimensional scalar mesh category.