Lemma A.1(2) on Q

For a covering π : ℤA_{2h} → Q whose deck group is generated by g (d, s) = (2h - 1 - d, s + c₀) (c₀ odd), every coefficient system on Q becomes the system with all coefficients one after rescaling arrows and entire mesh relations.

def MultiplicativeBasisDeformations.OddGauge.vd (L : Fin 1 → ℕ) (d : ℕ) : StarV L

The vertex at a given depth (the centre outside the range).

theorem MultiplicativeBasisDeformations.OddGauge.vd_depth {L : Fin 1 → ℕ} (v : StarV L) : vd L (starDepth v) = v

theorem MultiplicativeBasisDeformations.OddGauge.depth_vd {L : Fin 1 → ℕ} (d : ℕ) (hd : d ≤ L 0 + 1) : starDepth (vd L d) = d

noncomputable def MultiplicativeBasisDeformations.OddGauge.Cd {L : Fin 1 → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [Field k] (c : MeshCoefficients k Q) (a b : ℕ) (s : ℤ) : kˣ

The coefficients of Q by depths.

theorem MultiplicativeBasisDeformations.OddGauge.σ_vd {L : Fin 1 → ℕ} (σ : StarV L ≃ StarV L) (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (hrev : ∀ (x : StarV L), starDepth (σ x) + starDepth x = L 0 + 1) (a : ℕ) (ha : a < 2 * h) : σ (vd L a) = vd L (2 * h - 1 - a)

theorem MultiplicativeBasisDeformations.OddGauge.Cd_inv {L : Fin 1 → ℕ} {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) (σ : 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) (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (hrev : ∀ (x : StarV L), starDepth (σ x) + starDepth x = L 0 + 1) (a b : ℕ) (s : ℤ) (ha : a < 2 * h) (hb : b < 2 * h) : Cd hQ π c (2 * h - 1 - a) (2 * h - 1 - b) (s + ↑c0) = Cd hQ π c a b s

theorem MultiplicativeBasisDeformations.OddGauge.Cd_per {L : Fin 1 → ℕ} {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) (σ : 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) (h : ℕ) (hL : L 0 = 2 * h - 2) (hrev : ∀ (x : StarV L), starDepth (σ x) + starDepth x = L 0 + 1) (a b : ℕ) (s : ℤ) : Cd hQ π c a b (s + ↑(2 * c0)) = Cd hQ π c a b s

noncomputable def MultiplicativeBasisDeformations.OddGauge.EZ {L : Fin 1 → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [Field k] (c : MeshCoefficients k Q) (c0 h : ℕ) (X : (starTree L).ZVert) : kˣ

The relation scales on ℤΔ.

noncomputable def MultiplicativeBasisDeformations.OddGauge.FZ {L : Fin 1 → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [Field k] (c : MeshCoefficients k Q) (c0 h : ℕ) (Y X : (starTree L).ZVert) : kˣ

The arrow scales on ℤΔ.

theorem MultiplicativeBasisDeformations.OddGauge.EZ_inv {L : Fin 1 → ℕ} {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) (σ : 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) (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (hrev : ∀ (x : StarV L), starDepth (σ x) + starDepth x = L 0 + 1) (hodd : Odd c0) (X : (starTree L).ZVert) : EZ hQ π c c0 h (StarGauge.gZ σ hσ c0 hσp X) = EZ hQ π c c0 h X

theorem MultiplicativeBasisDeformations.OddGauge.FZ_inv {L : Fin 1 → ℕ} {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) (σ : 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) (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (hrev : ∀ (x : StarV L), starDepth (σ x) + starDepth x = L 0 + 1) (hodd : Odd c0) (Y X : (starTree L).ZVert) : FZ hQ π c c0 h (StarGauge.gZ σ hσ c0 hσp Y) (StarGauge.gZ σ hσ c0 hσp X) = FZ hQ π c c0 h Y X

theorem MultiplicativeBasisDeformations.OddGauge.zEq_one {L : Fin 1 → ℕ} {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) (σ : 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) (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (hrev : ∀ (x : StarV L), starDepth (σ x) + starDepth x = L 0 + 1) (hodd : Odd c0) (X : ↑(starTree L).zQuiver.nonprojective) (Y : (starTree L).ZVert) (A : Y ⟶ ↑X) : 1 = EZ hQ π c c0 h ↑X * (starTree L).pullCoeff hQ π c X Y A * FZ hQ π c c0 h (↑((starTree L).zQuiver.tau X)) Y * FZ hQ π c c0 h Y ↑X

The gauge equations on ℤΔ, with all target coefficients one.

theorem MultiplicativeBasisDeformations.OddGauge.exists_one_gauge {L : Fin 1 → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) {k : Type u} [Field 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) (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (hrev : ∀ (x : StarV L), starDepth (σ x) + starDepth x = L 0 + 1) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (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) (hodd : Odd 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) = fun (x : ↑(starTree L).zQuiver.nonprojective) (x_1 : (starTree L).ZVert) (x_2 : x_1 ⟶ ↑x) => 1

Lemma A.1(2): on an odd quotient of even A, every coefficient system becomes the system with all coefficients one after rescaling arrows and entire mesh relations.