Lemma A.1(1): signed coefficients on a periodic star model

lem:periodic-scalar-gauges (1) (periodic-mesh-calculations.tex). Let π : ℤΔ → Q be a covering of a star model commuting with translation, whose fibres are the orbits of g (v, t) = (σ v, t + c₀), with σ fixing the centre. Every coefficient system c on Q becomes the signed preprojective one after rescaling arrows and entire mesh relations: the scales of StarGauge are g-invariant, so they descend to Q.

def MultiplicativeBasisDeformations.StarGauge.child {t : ℕ} {L : Fin t → ℕ} (w w' : StarV L) : StarV L

The endpoint of an edge further from the centre.

theorem MultiplicativeBasisDeformations.StarGauge.child_comm {t : ℕ} {L : Fin t → ℕ} {w w' : StarV L} (h : starAdj w w') : child w w' = child w' w

theorem MultiplicativeBasisDeformations.StarGauge.pa_succ {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j + 1 ≤ L i) : pa i (j + 1) h = ch i j ⋯

theorem MultiplicativeBasisDeformations.StarGauge.adj_cases {t : ℕ} {L : Fin t → ℕ} {w w' : StarV L} (h : starAdj w' w) : (∃ (i : Fin t) (j : ℕ) (hj : j ≤ L i), w = ch i j hj ∧ w' = pa i j hj) ∨ ∃ (i : Fin t) (j : ℕ) (hj : j ≤ L i), w = pa i j hj ∧ w' = ch i j hj

The two ways an edge of the star is seen from its endpoints.

theorem MultiplicativeBasisDeformations.StarGauge.child_ch_pa {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (hj : j ≤ L i) : child (ch i j hj) (pa i j hj) = ch i j hj

theorem MultiplicativeBasisDeformations.StarGauge.child_pa_ch {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (hj : j ≤ L i) : child (pa i j hj) (ch i j hj) = ch i j hj

The coefficient function of Q

theorem MultiplicativeBasisDeformations.StarGauge.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.StarGauge.par_two {t : ℕ} {L : Fin t → ℕ} (w : StarV L) (h : ℤ) (hh : ↑h = (starTree L).par w) : ↑(h + 2) = (starTree L).par w

theorem MultiplicativeBasisDeformations.StarGauge.par_one {t : ℕ} {L : Fin t → ℕ} {w w' : StarV L} (hadj : (starTree L).G.Adj w' w) (h : ℤ) (hh : ↑h = (starTree L).par w) : ↑(h + 1) = (starTree L).par w'

noncomputable def MultiplicativeBasisDeformations.StarGauge.Cf {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) (w w' : StarV L) (h : ℤ) : kˣ

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

theorem MultiplicativeBasisDeformations.StarGauge.pullCoeff_eq {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (X : ↑(starTree L).zQuiver.nonprojective) (Y : (starTree L).ZVert) (A : Y ⟶ ↑X) : (starTree L).pullCoeff hQ π c X Y A = Cf hQ π c (↑X).v Y.v ((↑X).t - 2)

theorem MultiplicativeBasisDeformations.StarGauge.Cf_inv {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (σ : 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) (w w' : StarV L) (h : ℤ) : Cf hQ π c (σ w) (σ w') (h + ↑c0) = Cf hQ π c w w' h

theorem MultiplicativeBasisDeformations.StarGauge.par_ch {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (hj : j ≤ L i) : (starTree L).par (ch i j hj) = ↑(j + 1)

theorem MultiplicativeBasisDeformations.StarGauge.par_pa {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (hj : j ≤ L i) : (starTree L).par (pa i j hj) = ↑j

theorem MultiplicativeBasisDeformations.StarGauge.ne_succ_zmod (j : ℕ) : ↑j ≠ ↑(j + 1)

theorem MultiplicativeBasisDeformations.StarGauge.depth_σ {t : ℕ} {L : Fin t → ℕ} (σ : StarV L ≃ StarV L) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (v : StarV L) : starDepth (σ v) = starDepth v

theorem MultiplicativeBasisDeformations.StarGauge.sgn_σ {t : ℕ} {L : Fin t → ℕ} {k : Type u} [CommRing k] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (w w' : StarV L) : (starTree L).sgn k (σ w) (σ w') = (starTree L).sgn k w w'

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.StarGauge.Nz {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) (c0 : ℕ) (θ : Equiv.Perm (Fin t)) : StarV L → ℤ → kˣ

The relation scales and arrow scales on ℤΔ.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.StarGauge.Mz {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) (c0 : ℕ) (θ : Equiv.Perm (Fin t)) : StarV L → ℤ → kˣ

theorem MultiplicativeBasisDeformations.StarGauge.zEq {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (σ : 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) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (hc0 : 0 < c0) (hc0e : Even c0) (X : ↑(starTree L).zQuiver.nonprojective) (Y : (starTree L).ZVert) (A : Y ⟶ ↑X) : (starTree L).zSigned k X Y A = Nz hQ π c c0 θ (↑X).v (↑X).t * (starTree L).pullCoeff hQ π c X Y A * Mz hQ π c c0 θ (child (↑X).v Y.v) ((↑X).t - 2) * Mz hQ π c c0 θ (child Y.v (↑X).v) Y.t

The gauge equations on ℤΔ.

Descent to Q

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.StarGauge.gZ {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) : (starTree L).ZVert → (starTree L).ZVert

The deck transformation on vertices.

theorem MultiplicativeBasisDeformations.StarGauge.gZ_iter {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 : ℕ) (X : (starTree L).ZVert) : ((gZ σ hσ c0 hσp)^[n] X).v = (σ ^ n) X.v ∧ ((gZ σ hσ c0 hσp)^[n] X).t = X.t + ↑n * ↑c0

theorem MultiplicativeBasisDeformations.StarGauge.gZ_arrow {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 : ℕ) {X Y : (starTree L).ZVert} (A : Nonempty (Y ⟶ X)) : Nonempty ((gZ σ hσ c0 hσp)^[n] Y ⟶ (gZ σ hσ c0 hσp)^[n] X)

theorem MultiplicativeBasisDeformations.StarGauge.π_gZ_iter {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))] (σ : 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 : ℕ) (X : (starTree L).ZVert) : π.obj ((gZ σ hσ c0 hσp)^[n] X) = π.obj X

theorem MultiplicativeBasisDeformations.StarGauge.child_σ {t : ℕ} {L : Fin t → ℕ} (σ : StarV L ≃ StarV L) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (w w' : StarV L) : child (σ w) (σ w') = σ (child w w')

noncomputable def MultiplicativeBasisDeformations.StarGauge.Ez {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) (c0 : ℕ) (θ : Equiv.Perm (Fin t)) (X : (starTree L).ZVert) : kˣ

The relation scale at a vertex of ℤΔ.

noncomputable def MultiplicativeBasisDeformations.StarGauge.Fz {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) (c0 : ℕ) (θ : Equiv.Perm (Fin t)) (Y X : (starTree L).ZVert) : kˣ

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

theorem MultiplicativeBasisDeformations.StarGauge.Ez_iter {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (σ : 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) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (hc0 : 0 < c0) (hc0e : Even c0) (n : ℕ) (X : (starTree L).ZVert) : Ez hQ π c c0 θ ((gZ σ hσ c0 hσp)^[n] X) = Ez hQ π c c0 θ X

theorem MultiplicativeBasisDeformations.StarGauge.Fz_iter {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (σ : 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) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (hc0 : 0 < c0) (hc0e : Even c0) (n : ℕ) (Y X : (starTree L).ZVert) : Fz hQ π c c0 θ ((gZ σ hσ c0 hσp)^[n] Y) ((gZ σ hσ c0 hσp)^[n] X) = Fz hQ π c c0 θ Y X

theorem MultiplicativeBasisDeformations.StarGauge.lift_unique {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))] (hπ : π.IsCovering) (X : (starTree L).ZVert) {Y₁ Y₂ : (starTree L).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.StarGauge.lift_exists {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))] (hπ : π.IsCovering) (X : (starTree L).ZVert) {y : V} (a : y ⟶ π.obj X) : ∃ (Y : (starTree L).ZVert), Nonempty (Y ⟶ X) ∧ π.obj Y = y

noncomputable def MultiplicativeBasisDeformations.StarGauge.ηQ {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) (c0 : ℕ) (θ : Equiv.Perm (Fin t)) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (x : ↑Q.nonprojective) : kˣ

The relation scales on Q.

noncomputable def MultiplicativeBasisDeformations.StarGauge.μQ {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (c0 : ℕ) (θ : Equiv.Perm (Fin t)) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) {y x : V} (a : y ⟶ x) : kˣ

The arrow scales on Q.

theorem MultiplicativeBasisDeformations.StarGauge.ηQ_eq {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (σ : 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) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (gZ σ hσ c0 hσp)^[n] X ∨ X = (gZ σ hσ c0 hσp)^[n] Y) (hc0 : 0 < c0) (hc0e : Even c0) (X : (starTree L).ZVert) : ηQ hQ π c c0 θ hsurj ⟨π.obj X, ⋯⟩ = Ez hQ π c c0 θ X

theorem MultiplicativeBasisDeformations.StarGauge.Fz_fibre {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (σ : 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) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (hπ : π.IsCovering) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (gZ σ hσ c0 hσp)^[n] X ∨ X = (gZ σ hσ c0 hσp)^[n] Y) (hc0 : 0 < c0) (hc0e : Even c0) {X X' Y Y' : (starTree L).ZVert} (hX : π.obj X' = π.obj X) (hY : π.obj Y' = π.obj Y) (A : Y ⟶ X) (A' : Y' ⟶ X') : Fz hQ π c c0 θ Y' X' = Fz hQ π c c0 θ Y X

theorem MultiplicativeBasisDeformations.StarGauge.μQ_eq {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (σ : 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) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (gZ σ hσ c0 hσp)^[n] X ∨ X = (gZ σ hσ c0 hσp)^[n] Y) (hc0 : 0 < c0) (hc0e : Even c0) {Y X : (starTree L).ZVert} (A : Y ⟶ X) : μQ hQ π c c0 θ hπ hsurj (π.map A) = Fz hQ π c c0 θ Y X

theorem MultiplicativeBasisDeformations.StarGauge.μQ_congr {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (c0 : ℕ) (θ : Equiv.Perm (Fin t)) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) {y x y' x' : V} (a : y ⟶ x) (a' : y' ⟶ x') (hy : y = y') (hx : x = x') : μQ hQ π c c0 θ hπ hsurj a = μQ hQ π c c0 θ hπ hsurj a'

theorem MultiplicativeBasisDeformations.StarGauge.exists_signed_gauge {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (σ : 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) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (gZ σ hσ c0 hσp)^[n] X ∨ X = (gZ σ hσ c0 hσp)^[n] Y) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hc0 : 0 < c0) (hc0e : Even c0) : ∃ (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ), ((starTree L).pullCoeff hQ π fun (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x) => η x * c x y a * μ ((Q.mate x y) a) * μ a) = (starTree L).zSigned k

Lemma A.1(1): rescaling arrows and entire mesh relations of Q turns every coefficient system into the signed preprojective coefficients.