Lemma 8.21(2): the primitive return corner is cyclic Nakayama

primitive-ray-equations.tex (lem:primitive-cyclic-corners(2)): "the full corner S_x … is a cyclic Nakayama algebra. … List them as y_1, …, y_t. The comparison maps satisfy f_i h_{ij} = f_j, h_{ij} h_j = h_i, h_{ji} = h_j f_i. … Hence the full corner is generated by the cycle x → y_1 → ⋯ → y_t → x. Every simple forward or wraparound path is a generating ray, and full cycles are the local generators. All rays are these paths times powers of a full cycle; the only relations are zero paths."

We list the return partners y_1, …, y_t of x by the degrees of their generating rays f_i : x → y_i (a chain under factorization, partner_chain), take the cycle arrows x → y_1 → ⋯ → y_t → x (f_1, the comparison maps, the reverse h_t), and show: full cycles are the local generators, consecutive paths between distinct vertices of S_x are its generating rays (by degrees), and every nonidentity ray of S_x is a consecutive path (cyclicNakayama). Consecutive products are cpath a i ℓ = a_i a_{i+1} ⋯ a_{i+ℓ-1}.

Consecutive products

def MultiplicativeBasisDeformations.RaySys.Sys.cpath {V R L : Type} [AddCommGroup L] (S : Sys V R L) (a : ℕ → R) (i ℓ : ℕ) : M S.P.toMult

a_i a_{i+1} ⋯ a_{i+ℓ-1}.

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_zero {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (a : ℕ → R) (i : ℕ) : S.cpath a i 0 = 1

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_succ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (a : ℕ → R) (i ℓ : ℕ) : S.cpath a i (ℓ + 1) = S.cpath a i ℓ * S.rr (a (i + ℓ))

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_one {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (a : ℕ → R) (i : ℕ) : S.cpath a i 1 = S.rr (a i)

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_add {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (a : ℕ → R) (i ℓ ℓ' : ℕ) : S.cpath a i (ℓ + ℓ') = S.cpath a i ℓ * S.cpath a (i + ℓ) ℓ'

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_const {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (g : R) (i ℓ : ℕ) : S.cpath (fun (x : ℕ) => g) i ℓ = S.rr g ^ ℓ

Generating rays

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_gen_of_deg {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {c g : R} (hg : S.IsGen g) (h1 : S.P.src c = S.P.src g) (h2 : S.P.tgt c = S.P.tgt g) (hd : S.P.deg (S.P.wt c) ≤ S.P.deg (S.P.wt g)) : c = g

A ray of the degree of a generating ray with the same endpoints is that ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_le_gen {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {c g : R} (hg : S.IsGen g) (h1 : S.P.src c = S.P.src g) (h2 : S.P.tgt c = S.P.tgt g) : S.P.deg (S.P.wt g) ≤ S.P.deg (S.P.wt c)

theorem MultiplicativeBasisDeformations.RaySys.Sys.isGen_of_deg {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {c : R} (h : ∀ (s : R), S.P.src s = S.P.src c → S.P.tgt s = S.P.tgt c → S.P.deg (S.P.wt c) ≤ S.P.deg (S.P.wt s)) : S.IsGen c

theorem MultiplicativeBasisDeformations.RaySys.Sys.rf_deg_lt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f f' : R} (hr : S.P.RF f f') (ht : S.P.tgt f ≠ S.P.tgt f') : S.P.deg (S.P.wt f) < S.P.deg (S.P.wt f')

A strict factorization between rays with distinct targets raises the degree.

The cycle of an ordered list of partners

def MultiplicativeBasisDeformations.RaySys.Sys.cv {V : Type} (x : V) (t : ℕ) (y : ℕ → V) (m : ℕ) : V

The vertices of the cycle: σ 0 = x, σ (i+1) = y_i, with period t + 1.

def MultiplicativeBasisDeformations.RaySys.Sys.ca {R : Type} (t : ℕ) (F H c : ℕ → R) (m : ℕ) : R

The arrows of the cycle: a_0 = f_1, a_i = c_i (the comparison maps), a_t = h_t.

theorem MultiplicativeBasisDeformations.RaySys.Sys.cv_period {V : Type} [Fintype V] [DecidableEq V] {x : V} {t : ℕ} {y : ℕ → V} (m : ℕ) : cv x t y (m + (t + 1)) = cv x t y m

theorem MultiplicativeBasisDeformations.RaySys.Sys.cv_period' {V : Type} [Fintype V] [DecidableEq V] {x : V} {t : ℕ} {y : ℕ → V} (j n : ℕ) : cv x t y (j + n * (t + 1)) = cv x t y j

theorem MultiplicativeBasisDeformations.RaySys.Sys.ca_period {R : Type} [Fintype R] [DecidableEq R] {t : ℕ} {F H c : ℕ → R} (m : ℕ) : ca t F H c (m + (t + 1)) = ca t F H c m

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_period {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {t : ℕ} {F H c : ℕ → R} (i ℓ : ℕ) : S.cpath (ca t F H c) (i + (t + 1)) ℓ = S.cpath (ca t F H c) i ℓ

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_period' {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {t : ℕ} {F H c : ℕ → R} (i n ℓ : ℕ) : S.cpath (ca t F H c) (i + n * (t + 1)) ℓ = S.cpath (ca t F H c) i ℓ

theorem MultiplicativeBasisDeformations.RaySys.Sys.F_src_tgt_H {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} {y : ℕ → V} {F H : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) {i : ℕ} (hi : i < t) : S.P.src (H i) = y i ∧ S.P.tgt (H i) = x

theorem MultiplicativeBasisDeformations.RaySys.Sys.ca_ends {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} (ht : 1 ≤ t) {y : ℕ → V} {F H c : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) (m : ℕ) : S.P.src (ca t F H c m) = cv x t y m ∧ S.P.tgt (ca t F H c m) = cv x t y (m + 1)

The arrows join consecutive vertices.

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_forward {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {t : ℕ} (ht : 1 ≤ t) {F H c : ℕ → R} (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) (j : ℕ) : 1 ≤ j → j ≤ t → S.cpath (ca t F H c) 0 j = S.rr (F (j - 1))

The forward paths from x are the f_i.

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_full_zero {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} (ht : 1 ≤ t) {y : ℕ → V} {F H c : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) : S.cpath (ca t F H c) 0 (t + 1) = S.q x

The full cycle at x is q_x.

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_back {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} (ht : 1 ≤ t) {y : ℕ → V} {F H c : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) (hy : ∀ i < t, y i ≠ x) {i : ℕ} (hi1 : 1 ≤ i) (hit : i ≤ t) : S.cpath (ca t F H c) i (t + 1 - i) = S.rr (H (i - 1))

The backward paths to x are the reverses h_i.

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_full {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} (ht : 1 ≤ t) {y : ℕ → V} {F H c : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) (hy : ∀ i < t, y i ≠ x) (i : ℕ) : S.cpath (ca t F H c) i (t + 1) = S.q (cv x t y i)

Full cycles are the local generators.

theorem MultiplicativeBasisDeformations.RaySys.Sys.cv_zero {V : Type} [Fintype V] [DecidableEq V] {x : V} {t : ℕ} {y : ℕ → V} : cv x t y 0 = x

theorem MultiplicativeBasisDeformations.RaySys.Sys.cv_succ {V : Type} [Fintype V] [DecidableEq V] {x : V} {t : ℕ} {y : ℕ → V} {i : ℕ} (hi : i < t) : cv x t y (i + 1) = y i

theorem MultiplicativeBasisDeformations.RaySys.Sys.cv_cases {V : Type} [Fintype V] [DecidableEq V] {x : V} {t : ℕ} {y : ℕ → V} (m : ℕ) : cv x t y m = x ∨ ∃ i < t, cv x t y m = y i

theorem MultiplicativeBasisDeformations.RaySys.Sys.χ_y {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} {y : ℕ → V} {F H : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) {i : ℕ} (hi : i < t) : S.χ (y i) = S.χ x ∧ S.q (y i) ≠ 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.χ_cv {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} {y : ℕ → V} {F H : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hqx : S.q x ≠ 0) (m : ℕ) : S.χ (cv x t y m) = S.χ x ∧ S.q (cv x t y m) ≠ 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_pow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} (ht : 1 ≤ t) {y : ℕ → V} {F H c : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) (hy : ∀ i < t, y i ≠ x) (i n : ℕ) : S.cpath (ca t F H c) i (n * (t + 1)) = S.q (cv x t y i) ^ n

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_ray {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} (ht : 1 ≤ t) {y : ℕ → V} {F H c : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) (i ℓ : ℕ) : 1 ≤ ℓ → S.cpath (ca t F H c) i ℓ ≠ 0 → ∃ (r : R), S.cpath (ca t F H c) i ℓ = S.rr r ∧ S.P.src r = cv x t y i ∧ S.P.tgt r = cv x t y (i + ℓ)

A nonzero consecutive path is a ray from σ_i to σ_{i+ℓ}.

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_ne_zero {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} (ht : 1 ≤ t) {y : ℕ → V} {F H c : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) (hy : ∀ i < t, y i ≠ x) (hqx : S.q x ≠ 0) {i ℓ : ℕ} (hℓ : ℓ ≤ t + 1) : S.cpath (ca t F H c) i ℓ ≠ 0

Consecutive paths of length at most t + 1 are nonzero (they divide a full cycle).

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_InU {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r g : R} {χ₀ : L} (hU : S.InU r g) (h1 : S.χ (S.P.src g) = χ₀) (h2 : S.χ (S.P.tgt g) = χ₀) (hd0 : 0 ≤ S.P.deg χ₀) (hlt : S.P.deg (S.P.wt g) < S.P.deg (S.P.wt r)) : S.P.deg (S.P.wt g) + S.P.deg χ₀ ≤ S.P.deg (S.P.wt r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.cpath_gen {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} (ht : 1 ≤ t) {y : ℕ → V} {F H c : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) (hy : ∀ i < t, y i ≠ x) (hyinj : ∀ (i j : ℕ), i < t → j < t → y i = y j → i = j) (hmono : ∀ (i j : ℕ), i < t → j < t → i < j → S.P.deg (S.P.wt (F i)) < S.P.deg (S.P.wt (F j))) (hqx : S.q x ≠ 0) {i ℓ : ℕ} (hi : i < t + 1) (hℓ1 : 1 ≤ ℓ) (hℓ : ℓ ≤ t) {r : R} (hr : S.cpath (ca t F H c) i ℓ = S.rr r) : S.IsGen r

Consecutive paths between distinct vertices are generating rays ("every simple forward or wraparound path is a generating ray").

theorem MultiplicativeBasisDeformations.RaySys.Sys.ray_eq_cpath {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : ℕ} (ht : 1 ≤ t) {y : ℕ → V} {F H c : ℕ → R} (hF : ∀ i < t, S.IsGen (F i) ∧ S.P.src (F i) = x ∧ S.P.tgt (F i) = y i ∧ S.PrimRev (F i) (H i) ∧ S.q x * S.rr (F i) = S.rr (F i) * S.q (y i) ∧ S.q x * S.rr (F i) ≠ 0) (hc : ∀ (i : ℕ), i + 1 < t → S.rr (F i) * S.rr (c i) = S.rr (F (i + 1))) (hy : ∀ i < t, y i ≠ x) (hyinj : ∀ (i j : ℕ), i < t → j < t → y i = y j → i = j) (hmono : ∀ (i j : ℕ), i < t → j < t → i < j → S.P.deg (S.P.wt (F i)) < S.P.deg (S.P.wt (F j))) (hqx : S.q x ≠ 0) {r : R} {i j : ℕ} (hi : i < t + 1) (hj : j < t + 1) (hsrc : S.P.src r = cv x t y i) (htgt : S.P.tgt r = cv x t y j) (hr0 : r ≠ S.P.e (S.P.src r)) : ∃ (m : ℕ) (ℓ : ℕ), 1 ≤ ℓ ∧ S.rr r = S.cpath (ca t F H c) m ℓ

Every nonidentity ray between vertices of the cycle is a consecutive path.

theorem MultiplicativeBasisDeformations.RaySys.Sys.cyclicNakayama {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {x : V} (hqx : S.q x ≠ 0) : ∃ (n : ℕ) (σ : ℕ → V) (a : ℕ → R), σ 0 = x ∧ (∀ (m : ℕ), σ (m + (n + 1)) = σ m) ∧ Set.InjOn σ (Set.Iio (n + 1)) ∧ (∀ (v : V), S.InS x v ↔ ∃ i < n + 1, σ i = v) ∧ (∀ (m : ℕ), S.P.src (a m) = σ m ∧ S.P.tgt (a m) = σ (m + 1)) ∧ (∀ (i : ℕ), S.cpath a i (n + 1) = S.q (σ i)) ∧ ∀ (r : R), S.InS x (S.P.src r) → S.InS x (S.P.tgt r) → r ≠ S.P.e (S.P.src r) → ∃ (m : ℕ) (ℓ : ℕ), 1 ≤ ℓ ∧ S.rr r = S.cpath a m ℓ

Lemma 8.21(2) (lem:primitive-cyclic-corners(2)): the primitive return corner S_x is a cyclic Nakayama algebra. Its vertices are σ_0 = x, σ_1, …, σ_t (the return partners, in the order of the chain of their generating rays), the arrows a_i : σ_i → σ_{i+1} (indices mod t + 1) form a cycle, each full cycle is the local generator, and every nonidentity ray between vertices of S_x is a consecutive path a_m a_{m+1} ⋯ a_{m+ℓ-1}; products of rays are thus concatenations, and the only relations are zero paths.