The tree of sectional paths

Proof of Proposition 4.1, Step 1 (periodic-mesh-calculations.tex). "Fix a vertex x₀ in the component. Let Δ have as vertices all sectional paths starting at x₀, including the empty path. Join a path to each of its sectional one-arrow extensions, orienting the edge towards the extension. This is a finite rooted tree."

Throughout, Q is a stable translation quiver on a finite set with at most one arrow between two vertices. This file builds the type SecPath of sectional paths from x₀, shows it is finite when sectional paths are bounded, and equips it with the oriented tree structure (edges from a path to its sectional one-arrow extensions).

theorem Quiver.Path.eq_nil_of_arrowList_eq_nil {V : Type v} [Quiver V] {x y : V} (p : Path x y) (h : p.arrowList = []) : ⟨y, p⟩ = ⟨x, nil⟩

theorem Quiver.Path.arrowList_injective {V : Type v} [Quiver V] {x y y' : V} (p : Path x y) (q : Path x y') : p.arrowList = q.arrowList → ⟨y, p⟩ = ⟨y', q⟩

A path from a fixed start is determined by its arrows.

theorem Quiver.Path.length_arrowList {V : Type v} [Quiver V] {x y : V} (p : Path x y) : p.arrowList.length = p.length

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath {V : Type v} [Quiver V] (Q : TranslationQuiver V) (x₀ : V) : Type (max v w)

The sectional paths starting at x₀: the vertices of the tree Δ.

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.endv {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} (p : Q.SecPath x₀) : V

The end vertex of a sectional path.

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.len {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} (p : Q.SecPath x₀) : ℕ

The length of a sectional path (its depth in the tree).

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.root {V : Type v} [Quiver V] (Q : TranslationQuiver V) (x₀ : V) : Q.SecPath x₀

The empty path, the root of the tree.

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.IsParent {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} (p q : Q.SecPath x₀) : Prop

q is a sectional one-arrow extension of p.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.len_of_isParent {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} {p q : Q.SecPath x₀} (h : p.IsParent q) : q.len = p.len + 1

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.isSectional_of_cons {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ y z : V} (p : Quiver.Path x₀ y) (a : y ⟶ z) (h : Q.IsSectional (p.cons a)) : Q.IsSectional p

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.parent {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} (p : Q.SecPath x₀) (hp : p.len ≠ 0) : Q.SecPath x₀

The parent of a nonempty sectional path.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.parent_isParent {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} (p : Q.SecPath x₀) (hp : p.len ≠ 0) : (p.parent hp).IsParent p

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.eq_parent_of_isParent {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} {p q : Q.SecPath x₀} (h : p.IsParent q) (hq : q.len ≠ 0) : p = q.parent hq

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.tree {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} : OrientedTree (Q.SecPath x₀)

The tree Δ of sectional paths, oriented from each path to its extensions. Its two-colouring is the parity of the length.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.finite_of_bound {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} [Finite V] [∀ (x y : V), Finite (x ⟶ y)] (N : ℕ) (hN : ∀ (y : V) (p : Quiver.Path x₀ y), Q.IsSectional p → p.length < N) : Finite (Q.SecPath x₀)

With a bound on the lengths of sectional paths, Δ is finite.