The centre corner of the preprojective category of a star (Lemma A.3)

lem:star-return-reduction (periodic-mesh-calculations.tex). For a star rooted at its centre o, oriented away from o, let x_i be the closed path of length two along arm i. The vertices of arm i are v_0 = o, v_1, …. "For j ≥ 2, the mesh at v_{j-1} replaces the backtrack v_{j-1} v_j v_{j-1} by v_{j-1} v_{j-2} v_{j-1}. … Iteration expresses every closed path at o as a word in the x_i. The centre mesh gives ∑ x_i = 0. Moving a power down its arm gives x_i^{L_i+1} = 0."

We prove the iteration in the following form: every path from o to v is, modulo the relations, a word in the x_i followed by the geodesic from o to v (normal_form). (In StarV L the arm i has L i + 1 vertices, so the manuscript's L_i is L i + 1.)

@[instance_reducible]

instance MultiplicativeBasisDeformations.StarCorner.instDecidableRelStarVOrientStarTree {t : ℕ} (L : Fin t → ℕ) : DecidableRel (starTree L).orient

def MultiplicativeBasisDeformations.StarCorner.o {t : ℕ} (L : Fin t → ℕ) : (starTree L).Dbl

The centre.

def MultiplicativeBasisDeformations.StarCorner.av {t : ℕ} (L : Fin t → ℕ) (i : Fin t) (j : ℕ) (h : j ≤ L i) : (starTree L).Dbl

The vertex j of arm i, at depth j + 1.

def MultiplicativeBasisDeformations.StarCorner.out0 {t : ℕ} {L : Fin t → ℕ} (i : Fin t) : o L ⟶ av L i 0 ⋯

def MultiplicativeBasisDeformations.StarCorner.in0 {t : ℕ} {L : Fin t → ℕ} (i : Fin t) : av L i 0 ⋯ ⟶ o L

def MultiplicativeBasisDeformations.StarCorner.outS {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j + 1 ≤ L i) : av L i j ⋯ ⟶ av L i (j + 1) h

def MultiplicativeBasisDeformations.StarCorner.inS {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j + 1 ≤ L i) : av L i (j + 1) h ⟶ av L i j ⋯

def MultiplicativeBasisDeformations.StarCorner.xp {t : ℕ} {L : Fin t → ℕ} (i : Fin t) : Quiver.Path (o L) (o L)

The closed path x_i of length two along arm i.

def MultiplicativeBasisDeformations.StarCorner.wordP {t : ℕ} {L : Fin t → ℕ} : List (Fin t) → Quiver.Path (o L) (o L)

The path of a word in the x_i.

theorem MultiplicativeBasisDeformations.StarCorner.wordP_append {t : ℕ} {L : Fin t → ℕ} (w w' : List (Fin t)) : wordP (w ++ w') = (wordP w).comp (wordP w')

theorem MultiplicativeBasisDeformations.StarCorner.length_wordP {t : ℕ} {L : Fin t → ℕ} (w : List (Fin t)) : (wordP w).length = 2 * w.length

def MultiplicativeBasisDeformations.StarCorner.geodA {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j ≤ L i) : Quiver.Path (o L) (av L i j h)

The geodesic from the centre to the vertex j of arm i.

def MultiplicativeBasisDeformations.StarCorner.geod {t : ℕ} {L : Fin t → ℕ} (v : (starTree L).Dbl) : Quiver.Path (o L) v

The geodesic from the centre.

theorem MultiplicativeBasisDeformations.StarCorner.length_geodA {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j ≤ L i) : (geodA i j h).length = j + 1

theorem MultiplicativeBasisDeformations.StarCorner.length_geod {t : ℕ} {L : Fin t → ℕ} (v : (starTree L).Dbl) : (geod v).length = starDepth v

def MultiplicativeBasisDeformations.StarCorner.yb {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j + 1 ≤ L i) : Quiver.Path (av L i j ⋯) (av L i j ⋯)

The outward backtrack at the vertex j of arm i.

def MultiplicativeBasisDeformations.StarCorner.zb {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j ≤ L i) : Quiver.Path (av L i j h) (av L i j h)

The inward backtrack at the vertex j of arm i.

def MultiplicativeBasisDeformations.StarCorner.pe {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j ≤ L i) : (y : (starTree L).Dbl) × (av L i j h ⟶ y)

The edge from the vertex j of arm i towards the centre.

theorem MultiplicativeBasisDeformations.StarCorner.sigma_ext' {t : ℕ} {L : Fin t → ℕ} {x : (starTree L).Dbl} (e e' : (y : (starTree L).Dbl) × (x ⟶ y)) (h : e.fst = e'.fst) : e = e'

theorem MultiplicativeBasisDeformations.StarCorner.nbr_arm {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j ≤ L i) (e : (y : (starTree L).Dbl) × (av L i j h ⟶ y)) : e = pe i j h ∨ ∃ (h' : j + 1 ≤ L i), e = ⟨av L i (j + 1) h', outS i j h'⟩

The neighbours of an arm vertex: towards the centre, or one step out.

theorem MultiplicativeBasisDeformations.StarCorner.nbr_centre {t : ℕ} {L : Fin t → ℕ} (e : (y : (starTree L).Dbl) × (o L ⟶ y)) : ∃ (i : Fin t), e = ⟨av L i 0 ⋯, out0 i⟩

The neighbours of the centre: one per arm.

theorem MultiplicativeBasisDeformations.StarCorner.path_back {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] {a b : (starTree L).Dbl} (e : a ⟶ b) (f g : b ⟶ a) : LinearPaths.path (e.toPath.comp f.toPath) = LinearPaths.path (e.toPath.comp g.toPath)

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.StarCorner.term {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] {x : (starTree L).Dbl} (e : (y : (starTree L).Dbl) × (x ⟶ y)) : LinearPaths.obj x ⟶ LinearPaths.obj x

The summand of the relation at x for the edge e.

theorem MultiplicativeBasisDeformations.StarCorner.preprojRel_eq {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (x : (starTree L).Dbl) : (starTree L).preprojRel k x = ∑ e : (y : (starTree L).Dbl) × (x ⟶ y), term k e

theorem MultiplicativeBasisDeformations.StarCorner.term_out {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) (j : ℕ) (h : j + 1 ≤ L i) : term k ⟨av L i (j + 1) h, outS i j h⟩ = LinearPaths.path (yb i j h)

theorem MultiplicativeBasisDeformations.StarCorner.term_pe {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) (j : ℕ) (h : j ≤ L i) : term k (pe i j h) = -LinearPaths.path (zb i j h)

theorem MultiplicativeBasisDeformations.StarCorner.term_out0 {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) : term k ⟨av L i 0 ⋯, out0 i⟩ = LinearPaths.path (xp i)

theorem MultiplicativeBasisDeformations.StarCorner.preprojRel_centre {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] : (starTree L).preprojRel k (o L) = ∑ i : Fin t, LinearPaths.path (xp i)

The centre relation ∑ x_i.

theorem MultiplicativeBasisDeformations.StarCorner.preprojRel_arm {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) (j : ℕ) (h : j + 1 ≤ L i) : (starTree L).preprojRel k (av L i j ⋯) = LinearPaths.path (yb i j h) - LinearPaths.path (zb i j ⋯)

The relation at an arm vertex with a successor: y_j - z_j.

theorem MultiplicativeBasisDeformations.StarCorner.preprojRel_leaf {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) : (starTree L).preprojRel k (av L i (L i) ⋯) = -LinearPaths.path (zb i (L i) ⋯)

The relation at the leaf of an arm: -z.

The normal form

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.StarCorner.I {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (x y : (starTree L).Dbl) : Submodule k (LinearPaths.obj x ⟶ LinearPaths.obj y)

The ideal of Π(Δ) on the star.

theorem MultiplicativeBasisDeformations.StarCorner.rel_mem {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (x : (starTree L).Dbl) : (starTree L).preprojRel k x ∈ I k x x

theorem MultiplicativeBasisDeformations.StarCorner.yb_sub_zb_mem {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) (j : ℕ) (h : j + 1 ≤ L i) : LinearPaths.path (yb i j h) - LinearPaths.path (zb i j ⋯) ∈ I k (av L i j ⋯) (av L i j ⋯)

x_i lies in the arm i; the mesh at an arm vertex with a successor identifies its two backtracks.

theorem MultiplicativeBasisDeformations.StarCorner.zb_leaf_mem {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) : LinearPaths.path (zb i (L i) ⋯) ∈ I k (av L i (L i) ⋯) (av L i (L i) ⋯)

theorem MultiplicativeBasisDeformations.StarCorner.sum_xp_mem {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] : ∑ i : Fin t, LinearPaths.path (xp i) ∈ I k (o L) (o L)

theorem MultiplicativeBasisDeformations.StarCorner.sub_comp_mem {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] {x y z : (starTree L).Dbl} {f g : LinearPaths.obj x ⟶ LinearPaths.obj y} (h : f - g ∈ I k x y) (q : LinearPaths.obj y ⟶ LinearPaths.obj z) : CategoryTheory.CategoryStruct.comp f q - CategoryTheory.CategoryStruct.comp g q ∈ I k x z

theorem MultiplicativeBasisDeformations.StarCorner.comp_sub_mem {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] {x y z : (starTree L).Dbl} {f g : LinearPaths.obj y ⟶ LinearPaths.obj z} (q : LinearPaths.obj x ⟶ LinearPaths.obj y) (h : f - g ∈ I k y z) : CategoryTheory.CategoryStruct.comp q f - CategoryTheory.CategoryStruct.comp q g ∈ I k x z

theorem MultiplicativeBasisDeformations.StarCorner.geod_yb {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) (j : ℕ) (h : j + 1 ≤ L i) : LinearPaths.path ((geodA i j ⋯).comp (yb i j h)) - LinearPaths.path ((xp i).comp (geodA i j ⋯)) ∈ I k (o L) (av L i j ⋯)

Claim: γ_j y_j ≡ x_i γ_j, where γ_j is the geodesic to the vertex j of arm i.

theorem MultiplicativeBasisDeformations.StarCorner.normal_form {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] {b : (starTree L).Dbl} (p : Quiver.Path (o L) b) : ∃ (w : List (Fin t)), LinearPaths.path p - LinearPaths.path ((wordP w).comp (geod b)) ∈ I k (o L) b ∧ p.length = 2 * w.length + starDepth b

Lemma A.3, iteration: every path from the centre is a word in the x_i followed by a geodesic, modulo the relations.

Powers

def MultiplicativeBasisDeformations.StarCorner.cpow {t : ℕ} {L : Fin t → ℕ} {a : (starTree L).Dbl} (p : Quiver.Path a a) : ℕ → Quiver.Path a a

Powers of a closed path.

theorem MultiplicativeBasisDeformations.StarCorner.cpow_succ' {t : ℕ} {L : Fin t → ℕ} {a : (starTree L).Dbl} (p : Quiver.Path a a) (n : ℕ) : cpow p (n + 1) = (cpow p n).comp p

theorem MultiplicativeBasisDeformations.StarCorner.length_cpow {t : ℕ} {L : Fin t → ℕ} {a : (starTree L).Dbl} (p : Quiver.Path a a) (n : ℕ) : (cpow p n).length = n * p.length

theorem MultiplicativeBasisDeformations.StarCorner.wordP_replicate {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (n : ℕ) : wordP (List.replicate n i) = cpow (xp i) n

theorem MultiplicativeBasisDeformations.StarCorner.cpow_sub_mem {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] {a : (starTree L).Dbl} {p p' : Quiver.Path a a} (h : LinearPaths.path p - LinearPaths.path p' ∈ I k a a) (n : ℕ) : LinearPaths.path (cpow p n) - LinearPaths.path (cpow p' n) ∈ I k a a

theorem MultiplicativeBasisDeformations.StarCorner.cpow_xp_succ {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (q : ℕ) : cpow (xp i) (q + 1) = (out0 i).toPath.comp ((cpow (zb i 0 ⋯) q).comp (in0 i).toPath)

theorem MultiplicativeBasisDeformations.StarCorner.cpow_yb_succ {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (r : ℕ) (h : r + 1 ≤ L i) (q : ℕ) : cpow (yb i r h) (q + 1) = (outS i r h).toPath.comp ((cpow (zb i (r + 1) h) q).comp (inS i r h).toPath)

theorem MultiplicativeBasisDeformations.StarCorner.cpow_zb_mem {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) (n r : ℕ) (hr : r ≤ L i) : L i - r = n → ∀ (q : ℕ), 1 ≤ q → L i + 1 - r ≤ q → LinearPaths.path (cpow (zb i r hr) q) ∈ I k (av L i r hr) (av L i r hr)

Inward backtracks die when pushed to the leaf: z_r^q = 0 for q ≥ L i + 1 - r, q ≥ 1.

theorem MultiplicativeBasisDeformations.StarCorner.xp_pow_mem {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) : LinearPaths.path (wordP (List.replicate (L i + 2) i)) ∈ I k (o L) (o L)

x_i^{L_i+1} = 0 (in the manuscript's indexing; arm i has L i + 1 vertices): moving a power down its arm.

Paths in an arm beyond a vertex

def MultiplicativeBasisDeformations.StarCorner.geodR {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (r n : ℕ) (h : r + n ≤ L i) : Quiver.Path (av L i r ⋯) (av L i (r + n) h)

The geodesic out along arm i from its vertex r.

theorem MultiplicativeBasisDeformations.StarCorner.length_geodR {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (r n : ℕ) (h : r + n ≤ L i) : (geodR i r n h).length = n

theorem MultiplicativeBasisDeformations.StarCorner.geodR_yb {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) (r : ℕ) (hr : r + 1 ≤ L i) (n : ℕ) (h : r + n + 1 ≤ L i) : LinearPaths.path ((geodR i r n ⋯).comp (yb i (r + n) h)) - LinearPaths.path ((yb i r hr).comp (geodR i r n ⋯)) ∈ I k (av L i r ⋯) (av L i (r + n) ⋯)

γ y_{r+n} ≡ y_r γ along the arm beyond r.

theorem MultiplicativeBasisDeformations.StarCorner.arm_normal_form {t : ℕ} {L : Fin t → ℕ} (k : Type u) [CommRing k] (i : Fin t) (r : ℕ) (hr : r + 1 ≤ L i) {b : (starTree L).Dbl} (p : Quiver.Path (av L i r ⋯) b) (hp : ∀ v ∈ p.vertices, ∃ (n : ℕ) (h : r + n ≤ L i), v = av L i (r + n) h) : ∃ (q : ℕ) (n : ℕ) (h : r + n ≤ L i) (hb : av L i (r + n) h = b), LinearPaths.path p - LinearPaths.path ((cpow (yb i r hr) q).comp (Quiver.Path.cast ⋯ hb (geodR i r n h))) ∈ I k (av L i r ⋯) b ∧ p.length = 2 * q + n

Normal form beyond an arm vertex: a path from the vertex r of arm i that stays in the arm beyond r is a power of the outward backtrack y_r followed by a geodesic.