Lemma A.5: closed paths of degree four in Π(D₄)

lem:d4-four-return (periodic-mesh-calculations.tex): "At the centre, degree-four paths are the six x_i x_j with i ≠ j, and their remaining relations are the row and column sums. In the order 12, 13, 21, 23, 31, 32, their classes are z, -z, -z, z, z, -z. Assigning these values in k gives a nonzero functional annihilating all the relations, so z ≠ 0. At leaf i, the two possible paths b_i a_j b_j a_i, j ≠ i, have only the relation that their sum is zero."

We work in a star with three arms, deleting every vertex at depth at least two: the retained vertices form the D₄ with centre o and leaves a_i. The functional takes the value M i j on o a_i o a_j o and on a_i o a_j o a_i, where M is the cyclic matrix with rows and columns summing to zero.

def MultiplicativeBasisDeformations.D4Return.M {k : Type u} [Field k] (i j : Fin 3) : k

The values M i j = 1 for j = i + 1, -1 for i = j + 1.

theorem MultiplicativeBasisDeformations.D4Return.M_self {k : Type u} [Field k] (i : Fin 3) : M i i = 0

theorem MultiplicativeBasisDeformations.D4Return.M_succ {k : Type u} [Field k] (i : Fin 3) : M i (i + 1) = 1

theorem MultiplicativeBasisDeformations.D4Return.sum_M_left {k : Type u} [Field k] (j : Fin 3) : ∑ i : Fin 3, M i j = 0

theorem MultiplicativeBasisDeformations.D4Return.sum_M_right {k : Type u} [Field k] (i : Fin 3) : ∑ j : Fin 3, M i j = 0

def MultiplicativeBasisDeformations.D4Return.armIdx {L : Fin 3 → ℕ} : StarV L → Option (Fin 3)

The arm of a vertex at depth one.

def MultiplicativeBasisDeformations.D4Return.MA {L : Fin 3 → ℕ} {k : Type u} [Field k] (a b : StarV L) : k

The value on a pair of depth-one vertices.

theorem MultiplicativeBasisDeformations.D4Return.MA_self {L : Fin 3 → ℕ} {k : Type u} [Field k] (a : StarV L) : MA a a = 0

theorem MultiplicativeBasisDeformations.D4Return.depth_of_MA_ne {L : Fin 3 → ℕ} {k : Type u} [Field k] {a b : StarV L} (h : MA a b ≠ 0) : starDepth a = 1 ∧ starDepth b = 1

def MultiplicativeBasisDeformations.D4Return.G {L : Fin 3 → ℕ} {k : Type u} [Field k] : List (StarV L) → k

The functional on vertex lists of length five.

theorem MultiplicativeBasisDeformations.D4Return.sum_centre {L : Fin 3 → ℕ} {k : Type u} [Field k] (h : StarV L → k) : ∑ e : (w : (starTree L).Dbl) × (StarCorner.o L ⟶ w), ↑((starTree L).sgn k (StarCorner.o L) e.fst) * h e.fst = ∑ i : Fin 3, h (StarCorner.av L i 0 ⋯)

Sums over the arrows out of the centre.

theorem MultiplicativeBasisDeformations.D4Return.sum_MA_left {L : Fin 3 → ℕ} {k : Type u} [Field k] (y : StarV L) : ∑ i : Fin 3, MA (StarCorner.av L i 0 ⋯) y = 0

theorem MultiplicativeBasisDeformations.D4Return.sum_MA_right {L : Fin 3 → ℕ} {k : Type u} [Field k] (x : StarV L) : ∑ j : Fin 3, MA x (StarCorner.av L j 0 ⋯) = 0

theorem MultiplicativeBasisDeformations.D4Return.G_len {L : Fin 3 → ℕ} {k : Type u} [Field k] (l : List (StarV L)) (h : l.length ≠ 5) : G l = 0

theorem MultiplicativeBasisDeformations.D4Return.case02 {L : Fin 3 → ℕ} {k : Type u} [Field k] (u y z : (starTree L).Dbl) : ∑ e : (w : (starTree L).Dbl) × (u ⟶ w), ↑((starTree L).sgn k u e.fst) * G [u, e.fst, u, y, z] = 0

theorem MultiplicativeBasisDeformations.D4Return.case11 {L : Fin 3 → ℕ} {k : Type u} [Field k] (u x y : (starTree L).Dbl) : ∑ e : (w : (starTree L).Dbl) × (u ⟶ w), ↑((starTree L).sgn k u e.fst) * G [x, u, e.fst, u, y] = 0

theorem MultiplicativeBasisDeformations.D4Return.case20 {L : Fin 3 → ℕ} {k : Type u} [Field k] (u x x' : (starTree L).Dbl) : ∑ e : (w : (starTree L).Dbl) × (u ⟶ w), ↑((starTree L).sgn k u e.fst) * G [x, x', u, e.fst, u] = 0

theorem MultiplicativeBasisDeformations.D4Return.G_rel {L : Fin 3 → ℕ} {k : Type u} [Field k] (u : (starTree L).Dbl) (l₀ l₂ : List (starTree L).Dbl) : ∑ e : (w : (starTree L).Dbl) × (u ⟶ w), ↑((starTree L).sgn k u e.fst) * G (l₀ ++ u :: e.fst :: u :: l₂) = 0

The functional annihilates the relations.

def MultiplicativeBasisDeformations.D4Return.Del {L : Fin 3 → ℕ} : Set (starTree L).Dbl

The deleted vertices: depth at least two.

theorem MultiplicativeBasisDeformations.D4Return.G_del {L : Fin 3 → ℕ} {k : Type u} [Field k] (l : List (starTree L).Dbl) (h : ∃ d ∈ l, d ∈ Del) : G l = 0

theorem MultiplicativeBasisDeformations.D4Return.not_mem_of_G {L : Fin 3 → ℕ} {k : Type u} [Field k] {v : (starTree L).Dbl} (p : Quiver.Path v v) (hp : G p.vertices ≠ 0) : LinearPaths.path p ∉ (((starTree L).preproj k).del Del).ideal (LinearPaths.obj v) (LinearPaths.obj v)

theorem MultiplicativeBasisDeformations.D4Return.d4_return {L : Fin 3 → ℕ} {k : Type u} [Field k] (v : (starTree L).Dbl) (hv : starDepth v ≤ 1) : ∃ (p : Quiver.Path v v), p.length = 4 ∧ LinearPaths.path p ∉ (((starTree L).preproj k).del Del).ideal (LinearPaths.obj v) (LinearPaths.obj v)

Lemma A.5: every vertex of the D₄ part carries a nonzero closed path of degree four in Π(Δ) modulo the deeper vertices.