The odd quotients of even A (Appendix A)

periodic-mesh-calculations.tex, "The odd quotients of even A": with all mesh coefficients one, "a correction to an arrow gives a relation between a row path and its one-arrow rotation, with opposite classes"; rows are reduced by the sum of their levels to words in the middle arrows ε, and "going around the cycle gives w_j = -w_j".

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowClass_rotate_one {k : Type u} [Field 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] (hQ : Q.IsStable) (hc : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = 1) {m : ℕ} (x : ↑Q.nonprojective) {y : V} (a : y ⟶ ↑x) (q : Quiver.Path (↑(Q.tau x)) y) (hq : q.length = m) : rowClass c m x (q.cons a) = -rowClass c m ⟨y, ⋯⟩ (((Q.mate ⟨y, ⋯⟩ ↑(Q.tau x)) ((Q.mate x y) a)).toPath.comp q)

Rotation with all coefficients one: a row and its one-arrow rotation have opposite classes.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowQ_rotate_one {k : Type u} [Field 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] (hQ : Q.IsStable) [∀ (x y : V), Subsingleton (x ⟶ y)] (hc : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = 1) {m : ℕ} {x y : V} (a : y ⟶ x) (b : hQ.tauE y ⟶ hQ.tauE x) (q : Quiver.Path (hQ.tauE x) y) (hq : q.length = m) : rowQ c hQ m (b.toPath.comp q) = -rowQ c hQ m (q.cons a)

theorem MultiplicativeBasisDeformations.OrientedTree.one_of_pull {D : Type u_1} (T : OrientedTree D) [Fintype D] [DecidableEq D] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field k] [(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] (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (hone : T.pullCoeff hQ π c = fun (x : ↑T.zQuiver.nonprojective) (x_1 : T.ZVert) (x_2 : x_1 ⟶ ↑x) => 1) (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x) : c x y a = 1

All coefficients one on Q, from all coefficients one upstairs.

theorem MultiplicativeBasisDeformations.OrientedTree.rowZ_rotate_one {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field k] [(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] (hc : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = 1) {m : ℕ} {Z Y₁ E E' : T.ZVert} (a₁ : Z ⟶ Y₁) (B : Quiver.Path Y₁ E) (a₂ : E ⟶ E') (hZ : π.obj Z = hQ.tauE (π.obj E)) (hY : π.obj Y₁ = hQ.tauE (π.obj E')) (hB : B.length = m) : T.rowZ hQ π c m (a₁.toPath.comp B) = -T.rowZ hQ π c m (B.cons a₂)

Rotation of a lifted row, all coefficients one.

def MultiplicativeBasisDeformations.OrientedTree.tauInvQ {D : Type u_1} (T : OrientedTree D) : T.ZVert ⥤q T.ZVert

Inverse translation as an automorphism of the quiver ℤΔ.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrientedTree.rowEnd {D : Type u_1} (T : OrientedTree D) (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (Z : T.ZVert) : T.ZVert

The deck image of the inverse translate: the end of a row path from Z.

def MultiplicativeBasisDeformations.OrientedTree.shiftPath {D : Type u_1} (T : OrientedTree D) (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) {Z Y : T.ZVert} (U : Quiver.Path Z Y) : Quiver.Path (T.rowEnd σ hσ s hσp Z) (T.rowEnd σ hσ s hσp Y)

The translate of an initial segment, appended at the end in a rotation.

theorem MultiplicativeBasisDeformations.OrientedTree.row_cond {D : Type u_1} (T : OrientedTree D) [Fintype D] [DecidableEq D] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (Z : T.ZVert) : π.obj Z = hQ.tauE (π.obj (T.rowEnd σ hσ s hσp Z))

theorem MultiplicativeBasisDeformations.OrientedTree.rowZ_rotate_path {D : Type u_1} (T : OrientedTree D) [Fintype D] [DecidableEq D] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field k] [(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] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hc : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = 1) {m : ℕ} {Z Y : T.ZVert} (U : Quiver.Path Z Y) (W : Quiver.Path Y (T.rowEnd σ hσ s hσp Z)) : U.length + W.length = m + 1 → T.rowZ hQ π c m (U.comp W) = (-1) ^ U.length • T.rowZ hQ π c m (W.comp (T.shiftPath σ hσ s hσp U))

Rotation of an initial segment of a lifted row, all coefficients one: [U W] = (-1)^{|U|} [W U'].

theorem MultiplicativeBasisDeformations.OrientedTree.sigma_eq_of_fst {D : Type u_1} (T : OrientedTree D) [Fintype D] [DecidableEq D] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [DecidableRel T.orient] {X : T.ZVert} (e e' : (Y : T.ZVert) × (Y ⟶ X)) (h : e.fst = e'.fst) : e = e'

theorem MultiplicativeBasisDeformations.OrientedTree.rowZ_two_term {D : Type u_1} (T : OrientedTree D) [Fintype D] [DecidableEq D] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field k] [(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] [DecidableRel T.orient] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hone : T.pullCoeff hQ π c = fun (x : ↑T.zQuiver.nonprojective) (x_1 : T.ZVert) (x_2 : x_1 ⟶ ↑x) => 1) {m : ℕ} {X Y₁ Y₂ : T.ZVert} (hne : Y₁ ≠ Y₂) (a₁ : Y₁ ⟶ X) (a₂ : Y₂ ⟶ X) (hall : ∀ (e : (Y : T.ZVert) × (Y ⟶ X)), e.fst = Y₁ ∨ e.fst = Y₂) (b₁ : T.ztau X ⟶ Y₁) (b₂ : T.ztau X ⟶ Y₂) {Z E : T.ZVert} (A : Quiver.Path Z (T.ztau X)) (B : Quiver.Path X E) : T.rowZ hQ π c m (A.comp ((b₁.toPath.comp a₁.toPath).comp B)) + T.rowZ hQ π c m (A.comp ((b₂.toPath.comp a₂.toPath).comp B)) = 0

A mesh with two terms (all coefficients one): replacing one two-arrow path through the mesh by the other changes the sign of the class.

theorem MultiplicativeBasisDeformations.OrientedTree.rowZ_peak {D : Type u_1} (T : OrientedTree D) [Fintype D] [DecidableEq D] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field k] [(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] [DecidableRel T.orient] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hone : T.pullCoeff hQ π c = fun (x : ↑T.zQuiver.nonprojective) (x_1 : T.ZVert) (x_2 : x_1 ⟶ ↑x) => 1) {m : ℕ} {Z₀ W W' Z₂ E : T.ZVert} (hZ : Z₀ = T.ztau Z₂) (b₁ : Z₀ ⟶ W) (b₂ : W ⟶ Z₂) (c₁ : Z₀ ⟶ W') (c₂ : W' ⟶ Z₂) (hne : W ≠ W') (hall : ∀ (e : (Y : T.ZVert) × (Y ⟶ Z₂)), e.fst = W ∨ e.fst = W') (B : Quiver.Path Z₂ E) : T.rowZ hQ π c m (b₁.toPath.comp (b₂.toPath.comp B)) = -T.rowZ hQ π c m (c₁.toPath.comp (c₂.toPath.comp B))

Peak replacement: at a vertex with exactly two in-neighbours, a row beginning Z₀ → W → Z₂ has the opposite class of the row beginning Z₀ → W' → Z₂.

def MultiplicativeBasisDeformations.EvenA.lev (h d : ℕ) : ℕ

The level of a depth: the distance to the middle edge, plus one.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.EvenA.levZ {L : Fin 1 → ℕ} (h : ℕ) (X : (starTree L).ZVert) : ℕ

The level of a vertex of ℤΔ.

theorem MultiplicativeBasisDeformations.EvenA.lev_pos (h d : ℕ) : 1 ≤ lev h d ∨ d < h ∧ h = 0

theorem MultiplicativeBasisDeformations.EvenA.lev_ge_one (h : ℕ) (hh : 1 ≤ h) (d : ℕ) : 1 ≤ lev h d

theorem MultiplicativeBasisDeformations.EvenA.lev_adj (h d : ℕ) : (lev h (d + 1) = lev h d + 1 ∨ lev h d = lev h (d + 1) + 1) ∨ d + 1 = h

Levels of adjacent depths differ by one, except across the middle edge.

theorem MultiplicativeBasisDeformations.EvenA.lev_rev (h d : ℕ) (hd : d < 2 * h) : lev h (2 * h - 1 - d) = lev h d

theorem MultiplicativeBasisDeformations.EvenA.lev_adj' (h a b : ℕ) (hab : b = a + 1 ∨ a = b + 1) (hb : 2 ≤ lev h b) : lev h a = lev h b + 1 ∨ lev h a + 1 = lev h b

Across an edge at a vertex of level at least two, levels differ by one.

theorem MultiplicativeBasisDeformations.EvenA.inward_unique (h d d₁ d₂ : ℕ) (h2 : 2 ≤ lev h d) (h1 : d₁ = d + 1 ∨ d = d₁ + 1) (h1' : lev h d₁ < lev h d) (h2' : d₂ = d + 1 ∨ d = d₂ + 1) (h2'' : lev h d₂ < lev h d) : d₁ = d₂

A vertex of level at least two has a unique neighbour of smaller level.

def MultiplicativeBasisDeformations.EvenA.lamC {L : Fin 1 → ℕ} (h : ℕ) {Z E : (starTree L).ZVert} (P : Quiver.Path Z E) : ℕ

The sum of the levels of a row, the last vertex omitted.

theorem MultiplicativeBasisDeformations.EvenA.dropLast_vertices_comp {W : Type u_1} [Quiver W] {a b c : W} (p : Quiver.Path a b) (q : Quiver.Path b c) : (p.comp q).vertices.dropLast = p.vertices.dropLast ++ q.vertices.dropLast

theorem MultiplicativeBasisDeformations.EvenA.lamC_comp {L : Fin 1 → ℕ} (h : ℕ) {Z Y E : (starTree L).ZVert} (p : Quiver.Path Z Y) (q : Quiver.Path Y E) : lamC h (p.comp q) = lamC h p + lamC h q

theorem MultiplicativeBasisDeformations.EvenA.lamC_shift {L : Fin 1 → ℕ} (h : ℕ) (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hσlev : ∀ (v : StarV L), lev h (starDepth (σ v)) = lev h (starDepth v)) {Z Y : (starTree L).ZVert} (U : Quiver.Path Z Y) : lamC h ((starTree L).shiftPath σ hσ s hσp U) = lamC h U

theorem MultiplicativeBasisDeformations.EvenA.lamC_rot {L : Fin 1 → ℕ} (h : ℕ) (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hσlev : ∀ (v : StarV L), lev h (starDepth (σ v)) = lev h (starDepth v)) {Z Y : (starTree L).ZVert} (U : Quiver.Path Z Y) (W : Quiver.Path Y ((starTree L).rowEnd σ hσ s hσp Z)) : lamC h (W.comp ((starTree L).shiftPath σ hσ s hσp U)) = lamC h (U.comp W)

Rotation preserves the level sum.

theorem MultiplicativeBasisDeformations.EvenA.levZ_shift_mem {L : Fin 1 → ℕ} (h : ℕ) (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hσlev : ∀ (v : StarV L), lev h (starDepth (σ v)) = lev h (starDepth v)) {Z Y : (starTree L).ZVert} (U : Quiver.Path Z Y) {v : (starTree L).ZVert} (hv : v ∈ ((starTree L).shiftPath σ hσ s hσp U).vertices) : ∃ v' ∈ U.vertices, levZ h v = levZ h v'

theorem MultiplicativeBasisDeformations.EvenA.exists_arrow_to {W : Type u_1} [Quiver W] {a b : W} (P : Quiver.Path a b) {v : W} (hv : v ∈ P.vertices) (hne : v ≠ a) : ∃ (c : W) (U : Quiver.Path a c) (e : c ⟶ v) (X : Quiver.Path v b), P = U.comp (e.toPath.comp X)

theorem MultiplicativeBasisDeformations.EvenA.lamC_cons_front {L : Fin 1 → ℕ} (h : ℕ) {Z Y E : (starTree L).ZVert} (e : Z ⟶ Y) (X : Quiver.Path Y E) : lamC h (e.toPath.comp X) = levZ h Z + lamC h X

theorem MultiplicativeBasisDeformations.EvenA.adj_depth {L : Fin 1 → ℕ} {a b : StarV L} : (starTree L).G.Adj a b ↔ starDepth b = starDepth a + 1 ∨ starDepth a = starDepth b + 1

theorem MultiplicativeBasisDeformations.EvenA.other_in {L : Fin 1 → ℕ} (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (Z₂ W : (starTree L).ZVert) (b : W ⟶ Z₂) (hout : levZ h W = levZ h Z₂ + 1) : ∃ (W' : (starTree L).ZVert) (c₂ : W' ⟶ Z₂) (c₁ : (starTree L).ztau Z₂ ⟶ W'), W ≠ W' ∧ levZ h W' < levZ h W ∧ ∀ (e : (Y : (starTree L).ZVert) × (Y ⟶ Z₂)), e.fst = W ∨ e.fst = W'

The other in-neighbour: at a vertex Z₂ with an outward in-neighbour W, there is exactly one further in-neighbour W', of smaller level than W.

theorem MultiplicativeBasisDeformations.EvenA.reduce {L : Fin 1 → ℕ} (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hσlev : ∀ (v : StarV L), lev h (starDepth (σ v)) = lev h (starDepth v)) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [Field k] [(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] (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hone : (starTree L).pullCoeff hQ π c = fun (x : ↑(starTree L).zQuiver.nonprojective) (x_1 : (starTree L).ZVert) (x_2 : x_1 ⟶ ↑x) => 1) (hc : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = 1) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (m : ℕ) (hm : 1 ≤ m) (hs : ↑m + 1 = 2 + s) (hε : ∀ (Z : (starTree L).ZVert) (P : Quiver.Path Z ((starTree L).rowEnd σ hσ s hσp Z)), P.length = m + 1 → (∀ v ∈ P.vertices, levZ h v = 1) → (starTree L).rowZ hQ π c m P = 0) (n : ℕ) (Z : (starTree L).ZVert) (P : Quiver.Path Z ((starTree L).rowEnd σ hσ s hσp Z)) : P.length = m + 1 → lamC h P ≤ n → (starTree L).rowZ hQ π c m P = 0

Reduction by the sum of levels (periodic-mesh-calculations.tex): if every row whose vertices all have level one (a word in the middle arrows) has zero class, every row of length m + 1 has zero class.

Words in the middle arrows

theorem MultiplicativeBasisDeformations.EvenA.lev_one_iff (h d : ℕ) : lev h d = 1 ↔ d + 1 = h ∨ d = h

theorem MultiplicativeBasisDeformations.EvenA.dbl_mid_unique {L : Fin 1 → ℕ} (h : ℕ) (hh : 1 ≤ h) {a b b' : (starTree L).Dbl} (p : Quiver.Path a b) (q : Quiver.Path a b') (hl : p.length = q.length) (hp : ∀ v ∈ p.vertices, lev h (starDepth v) = 1) (hq : ∀ v ∈ q.vertices, lev h (starDepth v) = 1) : ⟨b, p⟩ = ⟨b', q⟩

Middle paths are determined by their start and length.

theorem MultiplicativeBasisDeformations.EvenA.mid_eq_of_par (h : ℕ) (hh : 1 ≤ h) {a b : ℕ} (ha : lev h a = 1) (hb : lev h b = 1) (hab : ↑a = ↑b) : a = b

Two middle depths of the same parity coincide.

theorem MultiplicativeBasisDeformations.EvenA.eps_rotate {L : Fin 1 → ℕ} (h : ℕ) (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hσlev : ∀ (v : StarV L), lev h (starDepth (σ v)) = lev h (starDepth v)) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [Field k] [(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] (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hc : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = 1) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (m j : ℕ) (Z : (starTree L).ZVert) (P : Quiver.Path Z ((starTree L).rowEnd σ hσ s hσp Z)) : P.length = m + 1 → (∀ v ∈ P.vertices, levZ h v = 1) → ∃ (Z' : (starTree L).ZVert) (P' : Quiver.Path Z' ((starTree L).rowEnd σ hσ s hσp Z')), Z'.t = Z.t + ↑j ∧ P'.length = m + 1 ∧ (∀ v ∈ P'.vertices, levZ h v = 1) ∧ (starTree L).rowZ hQ π c m P = (-1) ^ j • (starTree L).rowZ hQ π c m P'

Rotating a middle row j times.

theorem MultiplicativeBasisDeformations.EvenA.eps_zero {L : Fin 1 → ℕ} (h : ℕ) (hh : 1 ≤ h) (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hσlev : ∀ (v : StarV L), lev h (starDepth (σ v)) = lev h (starDepth v)) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [Field k] [(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] (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hc : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = 1) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hdeckg : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hodd : Odd c0) (hρlev : ∀ (v : StarV L), lev h (starDepth (ρ v)) = lev h (starDepth v)) (h2 : 2 ≠ 0) (m : ℕ) (Z : (starTree L).ZVert) (P : Quiver.Path Z ((starTree L).rowEnd σ hσ s hσp Z)) (hP : P.length = m + 1) (hlev : ∀ v ∈ P.vertices, levZ h v = 1) : (starTree L).rowZ hQ π c m P = 0

Middle words vanish (periodic-mesh-calculations.tex): rotating a word in the middle arrows c₀ times gives its image under the deck generator with the sign (-1)^{c₀} = -1, so twice its class is zero.