Long paths of Π(A_N) vanish

characteristic-two-mesh-calculations.tex: "For the preprojective category of A_N, … the interior relations interchange s₊s₋ and s₋s₊, while the endpoint backtracks are zero. For paths starting at i, sorting the steps in either order shows that the paths s₊^a s₋^b, 0 ≤ a ≤ N − i, 0 ≤ b ≤ i − 1, span. An interchange at an endpoint makes the path zero. … In particular all paths of degree at least N are zero."

We work on the path rooted at an end (starTree L with one arm, depths 0, …, L 0 + 1). A path has rc steps to the right (away from the root) and lc steps to the left. Replacing a peak u → u+1 → u by the dip u → u−1 → u (the relation at u), or by zero at the root, lowers the number inv of pairs (right step, later left step). A path without such pairs makes all its left steps first, so it has at most depth left steps. Hence a path with more left steps than its start depth lies in the ideal (left_overflow); symmetrically for right steps (right_overflow), and every path of length at least L 0 + 2 lies in the ideal (long_mem).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ASort.dep {L : Fin 1 → ℕ} (u : (starTree L).Dbl) : ℕ

The depth of a vertex of the doubled path.

theorem MultiplicativeBasisDeformations.ASort.arrow_dep {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} (e : u ⟶ v) : dep v = dep u + 1 ∨ dep u = dep v + 1

theorem MultiplicativeBasisDeformations.ASort.dep_injective {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} (h : dep u = dep v) : u = v

def MultiplicativeBasisDeformations.ASort.isR {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} : (u ⟶ v) → Prop

A step to the right.

@[instance_reducible]

instance MultiplicativeBasisDeformations.ASort.instDecidableIsR {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} (e : u ⟶ v) : Decidable (isR e)

@[irreducible]

def MultiplicativeBasisDeformations.ASort.rc {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} : Quiver.Path a b → ℕ

The numbers of right steps, left steps and inversions.

@[irreducible]

def MultiplicativeBasisDeformations.ASort.lc {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} : Quiver.Path a b → ℕ

@[irreducible]

def MultiplicativeBasisDeformations.ASort.inv {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} : Quiver.Path a b → ℕ

theorem MultiplicativeBasisDeformations.ASort.dep_end {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) : dep b + lc p = dep a + rc p

theorem MultiplicativeBasisDeformations.ASort.length_eq {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) : p.length = rc p + lc p

theorem MultiplicativeBasisDeformations.ASort.rc_comp {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) {c : (starTree L).Dbl} (q : Quiver.Path b c) : rc (p.comp q) = rc p + rc q

theorem MultiplicativeBasisDeformations.ASort.lc_comp {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) {c : (starTree L).Dbl} (q : Quiver.Path b c) : lc (p.comp q) = lc p + lc q

theorem MultiplicativeBasisDeformations.ASort.inv_comp {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) {c : (starTree L).Dbl} (q : Quiver.Path b c) : inv (p.comp q) = inv p + inv q + rc p * lc q

theorem MultiplicativeBasisDeformations.ASort.sorted_lc {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) : inv p = 0 → lc p ≤ dep a

Sorted paths make their left steps first.

theorem MultiplicativeBasisDeformations.ASort.back_eq {L : Fin 1 → ℕ} {u v x : (starTree L).Dbl} (e₁ : u ⟶ v) (e₂ : v ⟶ x) (h1 : isR e₁) (h2 : ¬isR e₂) : x = u

theorem MultiplicativeBasisDeformations.ASort.exists_peak {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) : 0 < inv p → ∃ (u : (starTree L).Dbl) (v : (starTree L).Dbl) (q : Quiver.Path a u) (e₁ : u ⟶ v) (e₂ : v ⟶ u) (r : Quiver.Path u b), isR e₁ ∧ p = q.comp (e₁.toPath.comp (e₂.toPath.comp r))

A path with an inversion contains a peak.

The relation at a vertex of the path

def MultiplicativeBasisDeformations.ASort.bt {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} (e : u ⟶ v) : Quiver.Path u u

The backtrack along an arrow.

theorem MultiplicativeBasisDeformations.ASort.bt_eq {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} (e₁ : u ⟶ v) (e₂ : v ⟶ u) : bt e₁ = e₁.toPath.comp e₂.toPath

theorem MultiplicativeBasisDeformations.ASort.rel_mem {L : Fin 1 → ℕ} (k : Type u_1) [Field k] (u : (starTree L).Dbl) : (starTree L).preprojRel k u ∈ ((starTree L).preproj k).ideal (LinearPaths.obj u) (LinearPaths.obj u)

theorem MultiplicativeBasisDeformations.ASort.out_cases {L : Fin 1 → ℕ} (u : (starTree L).Dbl) (x : (y : (starTree L).Dbl) × (u ⟶ y)) : dep x.fst = dep u + 1 ∨ dep u = dep x.fst + 1

The neighbours of a vertex are its depth neighbours.

theorem MultiplicativeBasisDeformations.ASort.out_eq {L : Fin 1 → ℕ} {u : (starTree L).Dbl} (x y : (y : (starTree L).Dbl) × (u ⟶ y)) (h : dep x.fst = dep y.fst) : x = y

theorem MultiplicativeBasisDeformations.ASort.peak_rel {L : Fin 1 → ℕ} (k : Type u_1) [Field k] {u v : (starTree L).Dbl} (e₁ : u ⟶ v) (e₂ : v ⟶ u) (hv : isR e₁) : LinearPaths.path (e₁.toPath.comp e₂.toPath) ∈ ((starTree L).preproj k).ideal (LinearPaths.obj u) (LinearPaths.obj u) ∨ ∃ (w : (starTree L).Dbl) (d₁ : u ⟶ w) (d₂ : w ⟶ u) (c : k), ¬isR d₁ ∧ isR d₂ ∧ LinearPaths.path (e₁.toPath.comp e₂.toPath) - c • LinearPaths.path (d₁.toPath.comp d₂.toPath) ∈ ((starTree L).preproj k).ideal (LinearPaths.obj u) (LinearPaths.obj u)

The relation at a vertex: the peak through the right neighbour lies in the ideal at the root, and is a multiple of the dip modulo the ideal otherwise.

Sorting

theorem MultiplicativeBasisDeformations.ASort.rc_toPath {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} (e : u ⟶ v) : rc e.toPath = if isR e then 1 else 0

theorem MultiplicativeBasisDeformations.ASort.lc_toPath {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} (e : u ⟶ v) : lc e.toPath = if isR e then 0 else 1

theorem MultiplicativeBasisDeformations.ASort.inv_toPath {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} (e : u ⟶ v) : inv e.toPath = 0

theorem MultiplicativeBasisDeformations.ASort.left_overflow {L : Fin 1 → ℕ} (k : Type u_1) [Field k] (n : ℕ) {a b : (starTree L).Dbl} (p : Quiver.Path a b) : inv p = n → dep a < lc p → LinearPaths.path p ∈ ((starTree L).preproj k).ideal (LinearPaths.obj a) (LinearPaths.obj b)

A path with more left steps than its start depth lies in the ideal.

The mirror image: right steps

@[irreducible]

def MultiplicativeBasisDeformations.ASort.inv2 {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} : Quiver.Path a b → ℕ

The number of pairs (left step, later right step).

theorem MultiplicativeBasisDeformations.ASort.inv2_comp {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) {c : (starTree L).Dbl} (q : Quiver.Path b c) : inv2 (p.comp q) = inv2 p + inv2 q + lc p * rc q

theorem MultiplicativeBasisDeformations.ASort.inv2_toPath {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} (e : u ⟶ v) : inv2 e.toPath = 0

theorem MultiplicativeBasisDeformations.ASort.dep_le_of_arrow {L : Fin 1 → ℕ} {u v : (starTree L).Dbl} : ∀ (x : u ⟶ v), dep v ≤ L 0 + 1

theorem MultiplicativeBasisDeformations.ASort.sorted_rc {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) : inv2 p = 0 → dep a + rc p ≤ L 0 + 1

theorem MultiplicativeBasisDeformations.ASort.fwd_eq {L : Fin 1 → ℕ} {u w x : (starTree L).Dbl} (e₁ : u ⟶ w) (e₂ : w ⟶ x) (h1 : ¬isR e₁) (h2 : isR e₂) : x = u

theorem MultiplicativeBasisDeformations.ASort.exists_dip {L : Fin 1 → ℕ} {a b : (starTree L).Dbl} (p : Quiver.Path a b) : 0 < inv2 p → ∃ (u : (starTree L).Dbl) (w : (starTree L).Dbl) (q : Quiver.Path a u) (e₁ : u ⟶ w) (e₂ : w ⟶ u) (r : Quiver.Path u b), ¬isR e₁ ∧ p = q.comp (e₁.toPath.comp (e₂.toPath.comp r))

theorem MultiplicativeBasisDeformations.ASort.dip_rel {L : Fin 1 → ℕ} (k : Type u_1) [Field k] {u w : (starTree L).Dbl} (e₁ : u ⟶ w) (e₂ : w ⟶ u) (hw : ¬isR e₁) : LinearPaths.path (e₁.toPath.comp e₂.toPath) ∈ ((starTree L).preproj k).ideal (LinearPaths.obj u) (LinearPaths.obj u) ∨ ∃ (v : (starTree L).Dbl) (d₁ : u ⟶ v) (d₂ : v ⟶ u) (c : k), isR d₁ ∧ ¬isR d₂ ∧ LinearPaths.path (e₁.toPath.comp e₂.toPath) - c • LinearPaths.path (d₁.toPath.comp d₂.toPath) ∈ ((starTree L).preproj k).ideal (LinearPaths.obj u) (LinearPaths.obj u)

The relation at a vertex, mirrored: the dip lies in the ideal at the far end, and is a multiple of the peak modulo the ideal otherwise.

theorem MultiplicativeBasisDeformations.ASort.right_overflow {L : Fin 1 → ℕ} (k : Type u_1) [Field k] (n : ℕ) {a b : (starTree L).Dbl} (p : Quiver.Path a b) : inv2 p = n → L 0 + 1 < dep a + rc p → LinearPaths.path p ∈ ((starTree L).preproj k).ideal (LinearPaths.obj a) (LinearPaths.obj b)

A path with more right steps than room lies in the ideal.

theorem MultiplicativeBasisDeformations.ASort.long_mem {L : Fin 1 → ℕ} (k : Type u_1) [Field k] {a b : (starTree L).Dbl} (p : Quiver.Path a b) (hp : L 0 + 2 ≤ p.length) : LinearPaths.path p ∈ ((starTree L).preproj k).ideal (LinearPaths.obj a) (LinearPaths.obj b)

All paths of degree at least N vanish in Π(A_N), N = L 0 + 2.