The deck transformation of the degree of a row

Proof of Lemma A.2(1) (periodic-mesh-calculations.tex): "Lift a row path from τ(x, j). Its endpoint has the form (ρ^l x, j - sl)." For a deck generator g (v, t) = (ρ v, t + c₀), a row of length m + 1 lifts to a path from τ X to g^n X with n c₀ = m - 1.

theorem MultiplicativeBasisDeformations.StarTrace.par_pow {t : ℕ} {L : Fin t → ℕ} (ρ : StarV L ≃ StarV L) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (n : ℕ) (v : StarV L) : (starTree L).par ((ρ ^ n) v) = (starTree L).par v + ↑↑(n * c0)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.StarTrace.gPow {t : ℕ} {L : Fin t → ℕ} (ρ : 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) (n : ℕ) : (starTree L).ZVert ⥤q (starTree L).ZVert

The deck transformation g^n in height form.

theorem MultiplicativeBasisDeformations.StarTrace.gPow_obj {t : ℕ} {L : Fin t → ℕ} (ρ : 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) (n : ℕ) (Z : (starTree L).ZVert) : (gPow ρ hρ c0 hρp n).obj Z = (StarGauge.gZ ρ hρ c0 hρp)^[n] Z

theorem MultiplicativeBasisDeformations.StarTrace.gPow_deck {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (ρ : 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) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (n : ℕ) (Z : (starTree L).ZVert) : π.obj ((gPow ρ hρ c0 hρp n).obj Z) = π.obj Z

theorem MultiplicativeBasisDeformations.StarTrace.gPow_fib {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hc0 : 0 < c0) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) (n : ℕ) (X E : (starTree L).ZVert) (h1 : π.obj E = π.obj X) (h2 : E.t = X.t + ↑(n * c0)) : E = (gPow ρ hρ c0 hρp n).obj X

theorem MultiplicativeBasisDeformations.StarTrace.row_lift {t : ℕ} {L : Fin t → ℕ} {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)) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hc0 : 0 < c0) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) {m : ℕ} (hm : 1 ≤ m) (x : ↑Q.nonprojective) (p : Quiver.Path ↑(Q.tau x) ↑x) (hp : p.length = m + 1) : ∃ (n : ℕ) (X : (starTree L).ZVert) (P : Quiver.Path ((starTree L).ztau X) ((gPow ρ hρ c0 hρp n).obj X)), ↑(n * c0) = ↑m - 1 ∧ P.length = m + 1 ∧ ScalarMeshCategory.rowClass c m x p = (starTree L).rowZ hQ π c m P

Rows of length m + 1 exist only in degrees c₀ ∣ m - 1, and lift to paths from τ X to g^n X with n c₀ = m - 1.