Lemma B.1: top paths of Π(D_n)

lem:d-top-paths (characteristic-two-mesh-calculations.tex): "Let Π(D_n) be the preprojective algebra of type D_n, and put N = n − 2. Let ν be the identity if N is even and the short-arm interchange if N is odd. At every vertex x, there is a nonzero path of degree 2N from x to ν x. This holds over every field."

The proof computes the recurrence matrices U_d of eq:preprojective-lower-bound through the line formula: on the line −N, …, N, (V_d)_{ij} = 1 exactly when |i − j| ≤ d ≤ 2N − |i + j| and d ≡ i − j (mod 2), and for D_n (U_d)_{rt} = (V_d)_{r,t} + (V_d)_{r,−t}, (U_d)_{ar} = (U_d)_{br} = (V_d)_{0,r}, with the short-leaf block ½[[1 + (−1)^q, 1 − (−1)^q], [1 − (−1)^q, 1 + (−1)^q]] in degree d = 2q and zero in odd degree. We check that this closed form satisfies the recurrence for d ≤ 2N (F_rec), so it equals U_d (U_eq_F); it is nonnegative, and U_{2N} is the permutation matrix of ν: the identity for N even (d_return, the case used in Appendix B) and the short-arm interchange nu for N odd (d_return_odd); both together are dTopPaths.

Labels: the star has short arms a, b with one vertex each and the long arm c; the spine vertex at depth j of the long arm has line position j + 1 and the centre has position 1.

The line formula

def MultiplicativeBasisDeformations.DTop.V (N d : ℕ) (i j : ℤ) : ℤ

V_d(i, j) on the line −N, …, N.

theorem MultiplicativeBasisDeformations.DTop.V_nonneg (N d : ℕ) (i j : ℤ) : 0 ≤ V N d i j

theorem MultiplicativeBasisDeformations.DTop.V_symm (N d : ℕ) (i j : ℤ) : V N d i j = V N d j i

theorem MultiplicativeBasisDeformations.DTop.V_neg (N d : ℕ) (i j : ℤ) : V N d (-i) (-j) = V N d i j

theorem MultiplicativeBasisDeformations.DTop.V_rec (N d : ℕ) (hd : d + 2 ≤ 2 * N) (i j : ℤ) (hi : -↑N ≤ i ∧ i ≤ ↑N) (hj : -↑N ≤ j ∧ j ≤ ↑N) : V N (d + 2) i j = V N (d + 1) (i - 1) j + V N (d + 1) (i + 1) j - V N d i j

The line recurrence V_{d+2} = A V_{d+1} − V_d.

Sums over neighbours

def MultiplicativeBasisDeformations.DTop.nb {t : ℕ} {L : Fin t → ℕ} (g : StarV L → ℤ) : StarV L → ℤ

The sum of a function over the neighbours of a vertex of the star.

theorem MultiplicativeBasisDeformations.DTop.ite_adj {t : ℕ} {L : Fin t → ℕ} {x z : StarV L} (g : ℤ) (P : Prop) [Decidable P] [Decidable (starAdj x z)] (h : starAdj x z ↔ P) : (if starAdj x z then 1 else 0) * g = if P then g else 0

theorem MultiplicativeBasisDeformations.DTop.sum_adjM {t : ℕ} {L : Fin t → ℕ} (x : StarV L) (g : StarV L → ℤ) : ∑ z : (starTree L).Dbl, (starTree L).adjM x z * g z = nb g x

The star of type D

def MultiplicativeBasisDeformations.DTop.spos {L : Fin 3 → ℕ} (c : Fin 3) : StarV L → Option ℤ

The line position of a spine vertex (the centre and the long arm).

def MultiplicativeBasisDeformations.DTop.F {L : Fin 3 → ℕ} (c : Fin 3) (N d : ℕ) (x y : StarV L) : ℤ

The closed form of U_d.

theorem MultiplicativeBasisDeformations.DTop.F_nonneg {L : Fin 3 → ℕ} (c : Fin 3) (N d : ℕ) (x y : StarV L) : 0 ≤ F c N d x y

The recurrence

def MultiplicativeBasisDeformations.DTop.LL (d : ℕ) (same : Prop) [Decidable same] : ℤ

The short-leaf block: [q even] on the diagonal and [q odd] off it, in degree 2q.

theorem MultiplicativeBasisDeformations.DTop.V_out (N d : ℕ) (j : ℤ) (hj : -↑N ≤ j ∧ j ≤ ↑N) : V N d (↑N + 1) j = 0

theorem MultiplicativeBasisDeformations.DTop.V_zero_neg (N d : ℕ) (t : ℤ) : V N d 0 (-t) = V N d 0 t

theorem MultiplicativeBasisDeformations.DTop.V_neg_one (N d : ℕ) (t : ℤ) : V N d (-1) t = V N d 1 (-t)

theorem MultiplicativeBasisDeformations.DTop.I1 (N d : ℕ) (hd : d + 2 ≤ 2 * N) (r t : ℤ) (hr : 2 ≤ r ∧ r ≤ ↑N) (ht : 1 ≤ t ∧ t ≤ ↑N) : V N (d + 2) r t + V N (d + 2) r (-t) = (V N (d + 1) (r - 1) t + V N (d + 1) (r - 1) (-t) + if r < ↑N then V N (d + 1) (r + 1) t + V N (d + 1) (r + 1) (-t) else 0) - (V N d r t + V N d r (-t))

theorem MultiplicativeBasisDeformations.DTop.I2 (N d : ℕ) (hd : d + 2 ≤ 2 * N) (r : ℤ) (hr : 2 ≤ r ∧ r ≤ ↑N) : V N (d + 2) r 0 = (V N (d + 1) (r - 1) 0 + if r < ↑N then V N (d + 1) (r + 1) 0 else 0) - V N d r 0

theorem MultiplicativeBasisDeformations.DTop.I3 (N d : ℕ) (hd : d + 2 ≤ 2 * N) (t : ℤ) (ht : 1 ≤ t ∧ t ≤ ↑N) : V N (d + 2) 1 t + V N (d + 2) 1 (-t) = V N (d + 1) 0 t + V N (d + 1) 0 t + (V N (d + 1) 2 t + V N (d + 1) 2 (-t)) - (V N d 1 t + V N d 1 (-t))

theorem MultiplicativeBasisDeformations.DTop.V00 (N d : ℕ) (hd : d + 2 ≤ 2 * N) : V N (d + 1) 0 0 = LL (d + 1) True + LL (d + 1) False

theorem MultiplicativeBasisDeformations.DTop.I4 (N d : ℕ) (hd : d + 2 ≤ 2 * N) : V N (d + 2) 1 0 = LL (d + 1) True + LL (d + 1) False + V N (d + 1) 2 0 - V N d 1 0

theorem MultiplicativeBasisDeformations.DTop.I5 (N d : ℕ) (hd : d + 2 ≤ 2 * N) (t : ℤ) (ht : 1 ≤ t ∧ t ≤ ↑N) : V N (d + 2) 0 t = V N (d + 1) 1 t + V N (d + 1) 1 (-t) - V N d 0 t

theorem MultiplicativeBasisDeformations.DTop.I6 (N d : ℕ) (hd : d + 2 ≤ 2 * N) (same : Prop) [Decidable same] : LL (d + 2) same = V N (d + 1) 1 0 - LL d same

Values of the closed form by vertex kind

theorem MultiplicativeBasisDeformations.DTop.F_ss {L : Fin 3 → ℕ} (c : Fin 3) (N d : ℕ) {x y : StarV L} {r t : ℤ} (hx : spos c x = some r) (hy : spos c y = some t) : F c N d x y = V N d r t + V N d r (-t)

theorem MultiplicativeBasisDeformations.DTop.F_ls {L : Fin 3 → ℕ} (c : Fin 3) (N d : ℕ) {x y : StarV L} {t : ℤ} (hx : spos c x = none) (hy : spos c y = some t) : F c N d x y = V N d 0 t

theorem MultiplicativeBasisDeformations.DTop.F_sl {L : Fin 3 → ℕ} (c : Fin 3) (N d : ℕ) {x y : StarV L} {r : ℤ} (hx : spos c x = some r) (hy : spos c y = none) : F c N d x y = V N d r 0

theorem MultiplicativeBasisDeformations.DTop.F_ll {L : Fin 3 → ℕ} (c : Fin 3) (N d : ℕ) {x y : StarV L} (hx : spos c x = none) (hy : spos c y = none) : F c N d x y = LL d (x = y)

theorem MultiplicativeBasisDeformations.DTop.spos_none {L : Fin 3 → ℕ} (c : Fin 3) : spos c none = some 1

theorem MultiplicativeBasisDeformations.DTop.spos_c {L : Fin 3 → ℕ} (c : Fin 3) (j : Fin (L c + 1)) : spos c (some ⟨c, j⟩) = some (↑↑j + 2)

theorem MultiplicativeBasisDeformations.DTop.spos_leaf {L : Fin 3 → ℕ} (c : Fin 3) {i : Fin 3} (hi : i ≠ c) (j : Fin (L i + 1)) : spos c (some ⟨i, j⟩) = none

theorem MultiplicativeBasisDeformations.DTop.LL_congr (d : ℕ) {P P' : Prop} [Decidable P] [Decidable P'] (h : P ↔ P') : LL d P = LL d P'

theorem MultiplicativeBasisDeformations.DTop.F_rec {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) (d : ℕ) (hd : d + 2 ≤ 2 * (L c + 2)) (x y : StarV L) : F c (L c + 2) (d + 2) x y = nb (fun (z : StarV L) => F c (L c + 2) (d + 1) z y) x - F c (L c + 2) d x y

Initial values and the identification with U_d

theorem MultiplicativeBasisDeformations.DTop.adjM_eq {t : ℕ} {L : Fin t → ℕ} (x y : StarV L) (P : Prop) [Decidable P] (h : starAdj x y ↔ P) : (starTree L).adjM x y = if P then 1 else 0

theorem MultiplicativeBasisDeformations.DTop.F_init {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) (x y : StarV L) : (F c (L c + 2) 0 x y = if x = y then 1 else 0) ∧ F c (L c + 2) 1 x y = (starTree L).adjM x y

theorem MultiplicativeBasisDeformations.DTop.U_eq_F {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) (d : ℕ) : d ≤ 2 * (L c + 2) → ∀ (x y : (starTree L).Dbl), UBound.U (starTree L).adjM d x y = F c (L c + 2) d x y

The closed form is the recurrence matrix in degrees up to 2N.

theorem MultiplicativeBasisDeformations.DTop.d_return {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) (hN : Even (L c)) {k : Type u_1} [Field k] (v : (starTree L).Dbl) : ∃ (p : Quiver.Path v v), p.length = 2 * (L c + 2) ∧ LinearPaths.path p ∉ (starTree L).Id k v v

Lemma B.1 for N even: every vertex of Π(D_n), n = N + 2, carries a closed path of degree 2N outside the ideal, over every field.

def MultiplicativeBasisDeformations.DTop.nu {L : Fin 3 → ℕ} (a b : Fin 3) : StarV L → StarV L

The short-arm interchange ν: it swaps the leaves of the short arms a, b and fixes the other vertices.

def MultiplicativeBasisDeformations.DTop.nuD {L : Fin 3 → ℕ} (a b : Fin 3) (v : (starTree L).Dbl) : (starTree L).Dbl

ν on the vertices of the doubled quiver.

theorem MultiplicativeBasisDeformations.DTop.d_return_odd {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) (hN : Odd (L c)) {k : Type u_1} [Field k] (v : (starTree L).Dbl) : ∃ (p : Quiver.Path v (nuD a b v)), p.length = 2 * (L c + 2) ∧ LinearPaths.path p ∉ (starTree L).Id k v (nuD a b v)

Lemma B.1 for N odd: every vertex x of Π(D_n), n = N + 2, carries a path of degree 2N from x to ν x outside the ideal, over every field.

theorem MultiplicativeBasisDeformations.DTop.dTopPaths {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) {k : Type u_1} [Field k] (v : (starTree L).Dbl) : ∃ (w : (starTree L).Dbl), (w = if Even (L c) then v else nuD a b v) ∧ ∃ (p : Quiver.Path v w), p.length = 2 * (L c + 2) ∧ LinearPaths.path p ∉ (starTree L).Id k v w

Lemma B.1 (lem:d-top-paths): at every vertex x of Π(D_n), N = n − 2, there is a path of degree 2N from x to ν x outside the ideal, where ν is the identity for N even and the short-arm interchange for N odd; over every field.