Periodic localization of the mesh derivative

Proposition 5.1 (prop:periodic-localization, mesh-deformations.tex).

A correction column has at most two entries (column_eq). On a row (x, w) with w = p a and a : y → x, the column (σ a, p) connects the row to its rotation (y, (σ σ a) p) when y is nonprojective, and has the row as its only entry when y is projective. Rotating moves every vertex of the path one step to the right and brings in the translate of the vertex before the last one; after d rotations a row is translated by τ. A row with a vertex that is not τ-periodic therefore reaches a one-entry column after finitely many rotations, and elimination from that end puts it in the image of D_m (row_mem_imageD_of_not_periodic).

The counting is organized by the potential d·δ(v_i) + (d - 1 - i), minimized over the positions i < d of the path, where δ(v) is the number of times τ can be applied to v. One rotation lowers it by exactly one.

def MultiplicativeBasisDeformations.TranslationQuiver.TauChain {V : Type v} [Quiver V] (Q : TranslationQuiver V) : V → ℕ → Prop

τ^j v is defined for all j < n.

def MultiplicativeBasisDeformations.TranslationQuiver.IsTauPeriodic {V : Type v} [Quiver V] (Q : TranslationQuiver V) (v : V) : Prop

A vertex on which every power of τ is defined. On a finite quiver these are the vertices on the cycles of τ (isTauPeriodic_iff).

theorem MultiplicativeBasisDeformations.TranslationQuiver.tauChain_succ_iff {V : Type v} [Quiver V] {Q : TranslationQuiver V} (v : V) (n : ℕ) : Q.TauChain v (n + 1) ↔ ∃ (h : v ∈ Q.nonprojective), Q.TauChain (↑(Q.tau ⟨v, h⟩)) n

theorem MultiplicativeBasisDeformations.TranslationQuiver.TauChain.mono {V : Type v} [Quiver V] {Q : TranslationQuiver V} {v : V} {n n' : ℕ} : n' ≤ n → Q.TauChain v n → Q.TauChain v n'

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.single_mem_familiesDeg {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] {m : ℕ} {u v : V} (a : u ⟶ v) (p : Quiver.Path u v) (hp : p.length = m) : Pi.single ⟨u, ⟨v, a⟩⟩ (pathMor c p) ∈ familiesDeg c m

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.row_mem_imageD_of_rotation {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] {m : ℕ} (x : ↑Q.nonprojective) {y : V} (a : y ⟶ ↑x) (p : Quiver.Path (↑(Q.tau x)) y) (hp : p.length = m) (hrot : ∀ (hy : y ∈ Q.nonprojective), row c ⟨y, hy⟩ (((Q.mate ⟨y, hy⟩ ↑(Q.tau x)) ((Q.mate x y) a)).toPath.comp p) ∈ imageD c m) : row c x (p.cons a) ∈ imageD c m

One step of the rotation: a row (x, p a) is in the image of D_m if y is projective, and otherwise exactly when its rotation (y, (σ σ a) p) is.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.vertices_rotate {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {x' y z : V} (b : x' ⟶ y) (p : Quiver.Path y z) {z' : V} (p' : Quiver.Path x' z') (a' : z' ⟶ z) (h : b.toPath.comp p = p'.cons a') : p'.vertices = x' :: p.vertices.dropLast

The vertices of the rotated path, without its endpoint.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.exists_eq_cons {V : Type v} [Quiver V] {a b : V} (q : Quiver.Path a b) (hq : 0 < q.length) : ∃ (z : V) (q' : Quiver.Path a z) (e : z ⟶ b), q = q'.cons e

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.vertices_getElem_length {V : Type v} [Quiver V] {a b : V} (q : Quiver.Path a b) (h : q.length < q.vertices.length) : q.vertices[q.length] = b

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.not_tauChain_tau {V : Type v} [Quiver V] {Q : TranslationQuiver V} {v : V} (hv : v ∈ Q.nonprojective) {n : ℕ} (h : ¬Q.TauChain v (n + 1)) : ¬Q.TauChain (↑(Q.tau ⟨v, hv⟩)) n

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.row_mem_imageD_of_potential {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (m N : ℕ) (x : ↑Q.nonprojective) {y : V} (a : y ⟶ ↑x) (p : Quiver.Path (↑(Q.tau x)) y) : p.length = m → (∃ (i : ℕ) (hi : i < p.vertices.length) (n : ℕ), ¬Q.TauChain p.vertices[i] (n + 1) ∧ (m + 1) * n + (m - i) ≤ N) → row c x (p.cons a) ∈ imageD c m

Elimination along rotations, by induction on the potential.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.row_mem_imageD_of_not_periodic {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] {m : ℕ} (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x) (hw : w.length = m + 1) {v : V} (hv : v ∈ w.vertices) (hper : ¬Q.IsTauPeriodic v) : row c x w ∈ imageD c m

Proposition 5.1, the nonperiodic rows (prop:periodic-localization). A row of length m + 1 through a vertex that is not τ-periodic lies in the image of D_m.