Lemma A.1(1) for an arbitrary rooted tree

lem:periodic-scalar-gauges (1), periodic-mesh-calculations.tex: "Let Q = ℤΔ/⟨τ^s ρ⟩, where Δ is a finite tree oriented away from a root fixed by ρ. Every nonzero coefficient system c can be changed to the signed preprojective coefficients." Proof: "Label the arrows over a parent-child edge orbit […] Such labels can be assigned recursively down the rooted orbit tree. […] Dividing the two equations gives a recurrence for μ_a. It closes around the cycle exactly when [a product of the η] equals a prescribed number. Choose the root product freely and assign the child products down the tree. Realize each product by one factor, setting the other factors to one."

The rooted tree is given by a parent map pa reaching the root o (Rooted), and the twist σ fixes o and commutes with pa. For each vertex v ≠ o the edge line {v, pa v} is solved on the representative rep v of the σ-orbit of v, with period per v · c₀, from the relation scales of its parent (step, exists_periodic_line_vertex), and transported along the orbit; the recursion runs on the depth (NM). The solution is g-invariant and solves every edge equation (main). The star version is StarGauge.exists_signed_gauge.

structure MultiplicativeBasisDeformations.RootedGauge.Rooted (D : Type u_1) : Type u_1

A rooted tree with a twist: a parent map reaching the root o, and a permutation σ fixing the root and commuting with the parent map.

• o : D
• pa : D → D
• root (v : D) : ∃ (n : ℕ), self.pa^[n] v = self.o
• σ : Equiv.Perm D
• σ_o : self.σ self.o = self.o
• σ_pa (v : D) : self.σ (self.pa v) = self.pa (self.σ v)

def MultiplicativeBasisDeformations.RootedGauge.Rooted.dep {D : Type u_1} [DecidableEq D] (R : Rooted D) (v : D) : ℕ

The depth: the number of parent steps to the root.

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.iter_σ {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (n : ℕ) (v : D) : R.pa^[n] (R.σ v) = R.σ (R.pa^[n] v)

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.σ_eq_o_iff {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (v : D) : R.σ v = R.o ↔ v = R.o

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.dep_σ {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (v : D) : R.dep (R.σ v) = R.dep v

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.dep_pa {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (v : D) (hv : v ≠ R.o) : R.dep (R.pa v) < R.dep v

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.pow_σ_o {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (n : ℕ) : (R.σ ^ n) R.o = R.o

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.pow_σ_pa {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (n : ℕ) (v : D) : (R.σ ^ n) (R.pa v) = R.pa ((R.σ ^ n) v)

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.dep_pow {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (n : ℕ) (v : D) : R.dep ((R.σ ^ n) v) = R.dep v

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.rep_ne {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (v : D) (hv : v ≠ R.o) : OrbitReps.rep R.σ v ≠ R.o

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.dep_rep {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (v : D) : R.dep (OrbitReps.rep R.σ v) = R.dep v

The edge lines

def MultiplicativeBasisDeformations.RootedGauge.Rooted.lineS {k : Type u} [CommRing k] {D : Type u_1} (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (v : D) (Np : ℤ → kˣ) (s : ℤ) : kˣ

The prescribed products on the edge line {v, pa v}, given the relation scales Np of the parent.

noncomputable def MultiplicativeBasisDeformations.RootedGauge.Rooted.step {k : Type u} [CommRing k] {D : Type u_1} (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (P : ℕ) (v : D) (Np : ℤ → kˣ) : (ℤ → kˣ) × (ℤ → kˣ)

One edge: the child's relation scales and the edge's arrow scales.

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.step_spec {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (P : ℕ) (v : D) (Np : ℤ → kˣ) (hP : 0 < P) (hPe : Even P) (hS : ∀ (s : ℤ), R.lineS Cf sg pr v Np (s + ↑P) = R.lineS Cf sg pr v Np s) : (∀ (s : ℤ), (R.step Cf sg pr P v Np).1 (s + ↑P) = (R.step Cf sg pr P v Np).1 s) ∧ (∀ (s : ℤ), (R.step Cf sg pr P v Np).2 (s + ↑P) = (R.step Cf sg pr P v Np).2 s) ∧ ∀ (s : ℤ), ((R.step Cf sg pr P v Np).2 s * (R.step Cf sg pr P v Np).2 (s + 1) * if ↑s = pr v then (R.step Cf sg pr P v Np).1 (s + 2) else 1) = R.lineS Cf sg pr v Np s

@[irreducible]

def MultiplicativeBasisDeformations.RootedGauge.Rooted.NM {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) (v : D) : (ℤ → kˣ) × (ℤ → kˣ)

The scales, recursively down the tree: at v ≠ o, the relation scales of v and the arrow scales of the edge {v, pa v}, solved on the orbit representative and transported.

noncomputable def MultiplicativeBasisDeformations.RootedGauge.Rooted.N {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) (v : D) : ℤ → kˣ

The relation scales.

noncomputable def MultiplicativeBasisDeformations.RootedGauge.Rooted.M {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) (v : D) : ℤ → kˣ

The arrow scales of the edge {v, pa v}.

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.N_o {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) : R.N Cf sg pr c0 R.o = fun (x : ℤ) => 1

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.M_o {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) : R.M Cf sg pr c0 R.o = fun (x : ℤ) => 1

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.RootedGauge.Rooted.B {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) (v : D) : (ℤ → kˣ) × (ℤ → kˣ)

The step on the representative of v.

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.N_ne {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) (v : D) (hv : v ≠ R.o) (s : ℤ) : R.N Cf sg pr c0 v s = (R.B Cf sg pr c0 v).1 (s - ↑(OrbitReps.ord R.σ v) * ↑c0)

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.M_ne {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) (v : D) (hv : v ≠ R.o) (s : ℤ) : R.M Cf sg pr c0 v s = (R.B Cf sg pr c0 v).2 (s - ↑(OrbitReps.ord R.σ v) * ↑c0)

Invariance and the edge equations

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.Cf_pow {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (c0 : ℕ) (hCinv : ∀ (w w' : D) (s : ℤ), Cf (R.σ w) (R.σ w') (s + ↑c0) = Cf w w' s) (n : ℕ) (w w' : D) (s : ℤ) : Cf ((R.σ ^ n) w) ((R.σ ^ n) w') (s + ↑n * ↑c0) = Cf w w' s

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.sg_pow {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (sg : D → D → kˣ) (hsg : ∀ (w w' : D), sg (R.σ w) (R.σ w') = sg w w') (n : ℕ) (w w' : D) : sg ((R.σ ^ n) w) ((R.σ ^ n) w') = sg w w'

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.pr_pow {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (pr : D → ZMod 2) (hpr : ∀ (w : D), pr (R.σ w) = pr w) (n : ℕ) (w : D) : pr ((R.σ ^ n) w) = pr w

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.par_even (c0 : ℕ) (hc0e : Even c0) (s n : ℤ) : ↑(s + n * ↑c0) = ↑s

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.N_pow {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) (x : D) (hx : ∀ (j : ℕ) (s : ℤ), R.N Cf sg pr c0 (R.σ ((R.σ ^ j) x)) (s + ↑c0) = R.N Cf sg pr c0 ((R.σ ^ j) x) s) (n : ℕ) (s : ℤ) : R.N Cf sg pr c0 ((R.σ ^ n) x) (s + ↑n * ↑c0) = R.N Cf sg pr c0 x s

One-step invariance iterates.

theorem MultiplicativeBasisDeformations.RootedGauge.Rooted.main {k : Type u} [CommRing k] {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (Cf : D → D → ℤ → kˣ) (sg : D → D → kˣ) (pr : D → ZMod 2) (c0 : ℕ) (hc0 : 0 < c0) (hc0e : Even c0) (hCinv : ∀ (w w' : D) (s : ℤ), Cf (R.σ w) (R.σ w') (s + ↑c0) = Cf w w' s) (hsg : ∀ (w w' : D), sg (R.σ w) (R.σ w') = sg w w') (hpr : ∀ (w : D), pr (R.σ w) = pr w) (d : ℕ) (v : D) : R.dep v = d → (∀ (s : ℤ), R.N Cf sg pr c0 (R.σ v) (s + ↑c0) = R.N Cf sg pr c0 v s ∧ R.M Cf sg pr c0 (R.σ v) (s + ↑c0) = R.M Cf sg pr c0 v s) ∧ (v ≠ R.o → ∀ (s : ℤ), (R.M Cf sg pr c0 v s * R.M Cf sg pr c0 v (s + 1) * if ↑s = pr v then R.N Cf sg pr c0 v (s + 2) else 1) = R.lineS Cf sg pr v (R.N Cf sg pr c0 (R.pa v)) s)

The scales are g-invariant and solve the edge equations, by induction on the depth.

The coefficients of Q along the covering

theorem MultiplicativeBasisDeformations.RootedGauge.c_congr {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x x' : ↑Q.nonprojective} {y y' : V} (hx : x = x') (hy : y = y') (a : y ⟶ ↑x) (a' : y' ⟶ ↑x') : c x y a = c x' y' a'

theorem MultiplicativeBasisDeformations.RootedGauge.par_two {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] (w : D) (h : ℤ) (hh : ↑h = T.par w) : ↑(h + 2) = T.par w

theorem MultiplicativeBasisDeformations.RootedGauge.par_one {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {w w' : D} (hadj : T.G.Adj w' w) (h : ℤ) (hh : ↑h = T.par w) : ↑(h + 1) = T.par w'

noncomputable def MultiplicativeBasisDeformations.RootedGauge.Cf {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) (w w' : D) (h : ℤ) : kˣ

The coefficient of Q at π (w, h + 2) of the image of the arrow from (w', h + 1).

theorem MultiplicativeBasisDeformations.RootedGauge.pullCoeff_eq {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (X : ↑T.zQuiver.nonprojective) (Y : T.ZVert) (A : Y ⟶ ↑X) : T.pullCoeff hQ π c X Y A = Cf T hQ π c (↑X).v Y.v ((↑X).t - 2)

theorem MultiplicativeBasisDeformations.RootedGauge.Cf_inv {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (w w' : D) (h : ℤ) : Cf T hQ π c (R.σ w) (R.σ w') (h + ↑c0) = Cf T hQ π c w w' h

def MultiplicativeBasisDeformations.RootedGauge.child {D : Type u_1} [DecidableEq D] (R : Rooted D) (w w' : D) : D

The endpoint of an edge further from the root.

theorem MultiplicativeBasisDeformations.RootedGauge.pa_pa_ne {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (v : D) (hv : v ≠ R.o) (hpv : R.pa v ≠ R.o) : R.pa (R.pa v) ≠ v

theorem MultiplicativeBasisDeformations.RootedGauge.child_up {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (v : D) (hv : v ≠ R.o) : child R v (R.pa v) = v

theorem MultiplicativeBasisDeformations.RootedGauge.child_down {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (v : D) (hv : v ≠ R.o) : child R (R.pa v) v = v

theorem MultiplicativeBasisDeformations.RootedGauge.child_σ {D : Type u_1} [Fintype D] [DecidableEq D] [LinearOrder D] (R : Rooted D) (w w' : D) : child R (R.σ w) (R.σ w') = R.σ (child R w w')

theorem MultiplicativeBasisDeformations.RootedGauge.sgn_σ {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {k : Type u} [CommRing k] [LinearOrder D] (R : Rooted D) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (w w' : D) : T.sgn k (R.σ w) (R.σ w') = T.sgn k w w'

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.RootedGauge.Nz {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (c0 : ℕ) (v : D) : ℤ → kˣ

The relation scales and arrow scales on ℤΔ.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.RootedGauge.Mz {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (c0 : ℕ) (v : D) : ℤ → kˣ

theorem MultiplicativeBasisDeformations.RootedGauge.hpr_of {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] [LinearOrder D] (R : Rooted D) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hc0e : Even c0) (w : D) : T.par (R.σ w) = T.par w

theorem MultiplicativeBasisDeformations.RootedGauge.zEq {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (hadj : ∀ (u w : D), T.G.Adj u w ↔ u ≠ R.o ∧ R.pa u = w ∨ w ≠ R.o ∧ R.pa w = u) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (hc0 : 0 < c0) (hc0e : Even c0) (X : ↑T.zQuiver.nonprojective) (Y : T.ZVert) (A : Y ⟶ ↑X) : T.zSigned k X Y A = Nz T hQ π c R c0 (↑X).v (↑X).t * T.pullCoeff hQ π c X Y A * Mz T hQ π c R c0 (child R (↑X).v Y.v) ((↑X).t - 2) * Mz T hQ π c R c0 (child R Y.v (↑X).v) Y.t

The gauge equations on ℤΔ.

Descent to Q

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RootedGauge.gZ {D : Type u_1} (T : OrientedTree D) (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) : T.ZVert → T.ZVert

The deck transformation on vertices.

theorem MultiplicativeBasisDeformations.RootedGauge.gZ_iter {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (n : ℕ) (X : T.ZVert) : ((gZ T R hσ c0 hσp)^[n] X).v = (R.σ ^ n) X.v ∧ ((gZ T R hσ c0 hσp)^[n] X).t = X.t + ↑n * ↑c0

theorem MultiplicativeBasisDeformations.RootedGauge.gZ_arrow {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (n : ℕ) {X Y : T.ZVert} (A : Nonempty (Y ⟶ X)) : Nonempty ((gZ T R hσ c0 hσp)^[n] Y ⟶ (gZ T R hσ c0 hσp)^[n] X)

theorem MultiplicativeBasisDeformations.RootedGauge.π_gZ_iter {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : T.ZVert ⥤q V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (n : ℕ) (X : T.ZVert) : π.obj ((gZ T R hσ c0 hσp)^[n] X) = π.obj X

noncomputable def MultiplicativeBasisDeformations.RootedGauge.Ez {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (c0 : ℕ) (X : T.ZVert) : kˣ

The relation scale at a vertex of ℤΔ.

noncomputable def MultiplicativeBasisDeformations.RootedGauge.Fz {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (c0 : ℕ) (Y X : T.ZVert) : kˣ

The arrow scale of the arrow Y → X of ℤΔ.

theorem MultiplicativeBasisDeformations.RootedGauge.inv_all {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (hc0 : 0 < c0) (hc0e : Even c0) (v : D) (s : ℤ) : Nz T hQ π c R c0 (R.σ v) (s + ↑c0) = Nz T hQ π c R c0 v s ∧ Mz T hQ π c R c0 (R.σ v) (s + ↑c0) = Mz T hQ π c R c0 v s

theorem MultiplicativeBasisDeformations.RootedGauge.Ez_iter {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (hc0 : 0 < c0) (hc0e : Even c0) (n : ℕ) (X : T.ZVert) : Ez T hQ π c R c0 ((gZ T R hσ c0 hσp)^[n] X) = Ez T hQ π c R c0 X

theorem MultiplicativeBasisDeformations.RootedGauge.Fz_iter {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (hc0 : 0 < c0) (hc0e : Even c0) (n : ℕ) (Y X : T.ZVert) : Fz T hQ π c R c0 ((gZ T R hσ c0 hσp)^[n] Y) ((gZ T R hσ c0 hσp)^[n] X) = Fz T hQ π c R c0 Y X

theorem MultiplicativeBasisDeformations.RootedGauge.lift_unique {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : T.ZVert ⥤q V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [LinearOrder D] (hπ : π.IsCovering) (X : T.ZVert) {Y₁ Y₂ : T.ZVert} (A₁ : Y₁ ⟶ X) (A₂ : Y₂ ⟶ X) (h : π.obj Y₁ = π.obj Y₂) : Y₁ = Y₂

Arrows into a vertex of ℤΔ are determined by the image of their source.

theorem MultiplicativeBasisDeformations.RootedGauge.lift_exists {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : T.ZVert ⥤q V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [LinearOrder D] (hπ : π.IsCovering) (X : T.ZVert) {y : V} (a : y ⟶ π.obj X) : ∃ (Y : T.ZVert), Nonempty (Y ⟶ X) ∧ π.obj Y = y

noncomputable def MultiplicativeBasisDeformations.RootedGauge.ηQ {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (c0 : ℕ) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (x : ↑Q.nonprojective) : kˣ

The relation scales on Q.

noncomputable def MultiplicativeBasisDeformations.RootedGauge.μQ {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (c0 : ℕ) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) {y x : V} (a : y ⟶ x) : kˣ

The arrow scales on Q.

theorem MultiplicativeBasisDeformations.RootedGauge.ηQ_eq {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (hfib : ∀ (X Y : T.ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (gZ T R hσ c0 hσp)^[n] X ∨ X = (gZ T R hσ c0 hσp)^[n] Y) (hc0 : 0 < c0) (hc0e : Even c0) (X : T.ZVert) : ηQ T hQ π c R c0 hsurj ⟨π.obj X, ⋯⟩ = Ez T hQ π c R c0 X

theorem MultiplicativeBasisDeformations.RootedGauge.Fz_fibre {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (hπ : π.IsCovering) (hfib : ∀ (X Y : T.ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (gZ T R hσ c0 hσp)^[n] X ∨ X = (gZ T R hσ c0 hσp)^[n] Y) (hc0 : 0 < c0) (hc0e : Even c0) {X X' Y Y' : T.ZVert} (hX : π.obj X' = π.obj X) (hY : π.obj Y' = π.obj Y) (A : Y ⟶ X) (A' : Y' ⟶ X') : Fz T hQ π c R c0 Y' X' = Fz T hQ π c R c0 Y X

theorem MultiplicativeBasisDeformations.RootedGauge.μQ_eq {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (hfib : ∀ (X Y : T.ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (gZ T R hσ c0 hσp)^[n] X ∨ X = (gZ T R hσ c0 hσp)^[n] Y) (hc0 : 0 < c0) (hc0e : Even c0) {Y X : T.ZVert} (A : Y ⟶ X) : μQ T hQ π c R c0 hπ hsurj (π.map A) = Fz T hQ π c R c0 Y X

theorem MultiplicativeBasisDeformations.RootedGauge.μQ_congr {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (c0 : ℕ) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) {y x y' x' : V} (a : y ⟶ x) (a' : y' ⟶ x') (hy : y = y') (hx : x = x') : μQ T hQ π c R c0 hπ hsurj a = μQ T hQ π c R c0 hπ hsurj a'

theorem MultiplicativeBasisDeformations.RootedGauge.exists_signed_gauge {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [LinearOrder D] (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (hadj : ∀ (u w : D), T.G.Adj u w ↔ u ≠ R.o ∧ R.pa u = w ∨ w ≠ R.o ∧ R.pa w = u) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (hfib : ∀ (X Y : T.ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (gZ T R hσ c0 hσp)^[n] X ∨ X = (gZ T R hσ c0 hσp)^[n] Y) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hc0 : 0 < c0) (hc0e : Even c0) : ∃ (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ), (T.pullCoeff hQ π fun (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x) => η x * c x y a * μ ((Q.mate x y) a) * μ a) = T.zSigned k

Lemma A.1(1) (lem:periodic-scalar-gauges), for an arbitrary finite tree Δ oriented away from a root o fixed by the twist σ: for a covering π : ℤΔ → Q commuting with translation whose fibres are the orbits of g (v, t) = (σ v, t + c₀), rescaling arrows and entire mesh relations of Q turns every coefficient system into the signed preprojective coefficients.

theorem MultiplicativeBasisDeformations.RootedGauge.exists_signed_gauge' {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (R : Rooted D) (hσ : ∀ (a b : D), T.G.Adj (R.σ a) (R.σ b) ↔ T.G.Adj a b) (c0 : ℕ) (hσp : ∀ (v : D), T.par (R.σ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct R.σ hσ (↑c0) hσp).obj Z) = π.obj Z) (hadj : ∀ (u w : D), T.G.Adj u w ↔ u ≠ R.o ∧ R.pa u = w ∨ w ≠ R.o ∧ R.pa w = u) (horient : ∀ (u w : D), T.orient u w ↔ w ≠ R.o ∧ R.pa w = u) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (hfib : ∀ (X Y : T.ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (gZ T R hσ c0 hσp)^[n] X ∨ X = (gZ T R hσ c0 hσp)^[n] Y) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hc0 : 0 < c0) (hc0e : Even c0) : ∃ (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ), (T.pullCoeff hQ π fun (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x) => η x * c x y a * μ ((Q.mate x y) a) * μ a) = T.zSigned k

Lemma A.1(1), without an auxiliary order on the vertices.