Valley words on a ladder

Let u d : ℕ → A be two families in a ring, read as the steps of a ladder with rungs 0, 1, 2, …: u w climbs from rung w to rung w + 1 and d w descends from rung w + 1 to rung w, and a product is read from right to left, so its rightmost factor is the first step. The valley word

ladderValley u d m s r = u (m + r - 1) ⋯ u (m + 1) u m · d m d (m + 1) ⋯ d (m + s - 1)

descends s rungs to rung m and then climbs r rungs.

Suppose that at every rung the two turns cancel,

d 0 * u 0 = 0    and    d (w + 1) * u (w + 1) + u w * d w = 0,

which are the relations of the signless preprojective algebra of the half-line 0 — 1 — 2 — ⋯. Then a descent following a valley word pushes the bottom of the valley one rung down, at the cost of a sign (TauCeti.d_mul_ladderValley); if the valley already touches rung 0 and then climbs, the product vanishes (TauCeti.d_mul_ladderValley_zero_eq_zero). Since a climb following a valley word is again a valley word (TauCeti.u_mul_ladderValley), these moves reduce every product of composable steps to a valley word up to sign, or to zero. A valley word from rung a to rung b has length at most a + b, so longer products vanish; this bounds the length of the nonzero paths in the preprojective algebra of type A. For two composable valley words, TauCeti.ladderValley_mul_ladderValley gives their product with the exact crossing sign; TauCeti.ladderValley_mul_ladderValley_eq_zero handles a negative formal bottom.

Without the relation d 0 * u 0 = 0 at the bottom rung, a descent after a climb from rung 0 leaves the turn d 0 * u 0 (TauCeti.d_mul_ladderValley_zero_zero). Its powers are, up to sign, the words climbing from rung 0 and descending back, so on a ladder with no climb from some rung N the turn is nilpotent (TauCeti.pow_d_mul_u_eq_zero). This is the situation at the end of an arm of a branched graph, read from its branch node.

Main definitions

• TauCeti.ladderValley: the valley word descending s rungs to rung m and climbing r rungs.

Main results

• TauCeti.u_mul_ladderValley, TauCeti.ladderValley_mul_d: extending a valley word by a final climb or an initial descent.
• TauCeti.d_mul_ladderValley: under the ladder relations, a final descent moves the valley one rung down.
• TauCeti.d_mul_ladderValley_zero_eq_zero: a final descent after a valley at rung 0 vanishes.
• TauCeti.d_mul_ladderValley_zero_zero: without the bottom relation, a descent after a climb from rung 0 leaves the turn at rung 0.
• TauCeti.pow_d_mul_u_eq_zero: on a ladder with no climb from rung N, the turn at rung 0 has vanishing N + 1-st power.

References

See W. Crawley-Boevey, Quiver algebras, weighted projective lines, and the Deligne--Simpson problem, Section 1, for the preprojective relations of a quiver.

def TauCeti.ladderValley {A : Type u_1} [Monoid A] (u d : ℕ → A) (m s r : ℕ) : A

The valley word u (m + r - 1) ⋯ u m · d m ⋯ d (m + s - 1): starting from rung m + s, it descends s rungs to rung m and then climbs r rungs to rung m + r. The first step is the rightmost factor.

Equations

• TauCeti.ladderValley u d m s r = (List.map (fun (i : ℕ) => u (m + i)) (List.range r)).reverse.prod * (List.map (fun (i : ℕ) => d (m + i)) (List.range s)).prod

@[simp]

theorem TauCeti.ladderValley_zero_zero {A : Type u_1} [Monoid A] (u d : ℕ → A) (m : ℕ) : ladderValley u d m 0 0 = 1

The empty valley word is 1.

@[simp]

theorem TauCeti.u_mul_ladderValley {A : Type u_1} [Monoid A] (u d : ℕ → A) (m s r : ℕ) : u (m + r) * ladderValley u d m s r = ladderValley u d m s (r + 1)

A final climb extends a valley word.

@[simp]

theorem TauCeti.ladderValley_mul_d {A : Type u_1} [Monoid A] (u d : ℕ → A) (m s r : ℕ) : ladderValley u d m s r * d (m + s) = ladderValley u d m (s + 1) r

An initial descent extends a valley word.

@[simp]

theorem TauCeti.d_mul_ladderValley_succ_zero {A : Type u_1} [Monoid A] (u d : ℕ → A) (m s : ℕ) : d m * ladderValley u d (m + 1) s 0 = ladderValley u d m (s + 1) 0

A descent onto the bottom of a word without climbs lengthens the descent.

theorem TauCeti.ladderValley_succ_zero_mul_u {A : Type u_1} [Monoid A] (u d : ℕ → A) (m r : ℕ) : ladderValley u d (m + 1) 0 r * u m = ladderValley u d m 0 (r + 1)

An initial climb from rung m extends a climb from rung m + 1.

theorem TauCeti.ladderValley_zero_mul_ladderValley {A : Type u_1} [Monoid A] (u d : ℕ → A) (m s r : ℕ) : ladderValley u d m 0 r * ladderValley u d m s 0 = ladderValley u d m s r

A valley word is its descent followed by its climb.

@[simp]

theorem TauCeti.ladderValley_climb_mul {A : Type u_1} [Monoid A] (u d : ℕ → A) (m s r t : ℕ) : ladderValley u d (m + r) 0 t * ladderValley u d m s r = ladderValley u d m s (r + t)

Two consecutive climbs concatenate, including the descent preceding the first climb.

@[simp]

theorem TauCeti.d_mul_ladderValley {A : Type u_1} [Ring A] {u d : ℕ → A} (hud : ∀ (w : ℕ), d (w + 1) * u (w + 1) + u w * d w = 0) (m s r : ℕ) : d (m + r) * ladderValley u d (m + 1) s r = (-1) ^ r * ladderValley u d m (s + 1) r

A final descent moves the valley down. If the turns at every positive rung cancel, then descending one rung after the valley word with bottom m + 1 gives, up to the sign (-1) ^ r, the valley word with bottom m, one more descent and the same number r of climbs.

@[simp]

theorem TauCeti.d_mul_ladderValley_zero_eq_zero {A : Type u_1} [Ring A] {u d : ℕ → A} (hud₀ : d 0 * u 0 = 0) (hud : ∀ (w : ℕ), d (w + 1) * u (w + 1) + u w * d w = 0) (s r : ℕ) : d r * ladderValley u d 0 s (r + 1) = 0

A valley at the bottom rung cannot be followed by a descent. If the turns at every rung cancel, then descending after a valley word which reaches rung 0 and climbs back up vanishes.

@[simp]

theorem TauCeti.ladderValley_mul_ladderValley {A : Type u_1} [Ring A] {u d : ℕ → A} (hud : ∀ (w : ℕ), d (w + 1) * u (w + 1) + u w * d w = 0) {m l s t r q : ℕ} (hcomp : m + s = l + q) (hbottom : s ≤ l) : ladderValley u d m s r * ladderValley u d l t q = (-1) ^ (s * q) * ladderValley u d (l - s) (t + s) (q + r)

The product of two composable valley words, when its bottom is nonnegative. Each descent in the later word crosses every climb in the earlier word.

@[simp]

theorem TauCeti.ladderValley_mul_ladderValley_eq_zero {A : Type u_1} [Ring A] {u d : ℕ → A} (hud₀ : d 0 * u 0 = 0) (hud : ∀ (w : ℕ), d (w + 1) * u (w + 1) + u w * d w = 0) {m l s t r q : ℕ} (hcomp : m + s = l + q) (hbottom : l < s) : ladderValley u d m s r * ladderValley u d l t q = 0

Two composable valley words multiply to zero if their formal bottom is negative.

theorem TauCeti.d_mul_ladderValley_zero_zero {A : Type u_1} [Ring A] {u d : ℕ → A} (hud : ∀ (w : ℕ), d (w + 1) * u (w + 1) + u w * d w = 0) (r : ℕ) : d r * ladderValley u d 0 0 (r + 1) = (-1) ^ r * (ladderValley u d 0 0 r * (d 0 * u 0))

A descent after a climb from rung 0 leaves a turn at rung 0. If the turns at every positive rung cancel, then climbing r + 1 rungs from rung 0 and descending one rung gives, up to the sign (-1) ^ r, the turn d 0 * u 0 at rung 0 followed by a climb of r rungs.

theorem TauCeti.pow_d_mul_u_eq_zero {A : Type u_1} [Ring A] {u d : ℕ → A} (hud : ∀ (w : ℕ), d (w + 1) * u (w + 1) + u w * d w = 0) {N : ℕ} (hN : u N = 0) : (d 0 * u 0) ^ (N + 1) = 0

The turn at the bottom of a finite ladder is nilpotent. If the turns at every positive rung cancel and there is no climb from rung N, then (d 0 * u 0) ^ (N + 1) = 0: the power (d 0 * u 0) ^ j is, up to sign, the word climbing j rungs from rung 0 and descending back, and no word climbs N + 1 rungs.