Descending invariant scales from ℤΔ to Q

Relation scales E X and arrow scales F Y X on ℤΔ which are invariant under the deck generator g descend to scales on Q = ℤΔ / ⟨g⟩: the fibres of π are the g-orbits, and an arrow into a given vertex is determined by the image of its source.

noncomputable def MultiplicativeBasisDeformations.StarGauge.ηD {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (π : (starTree L).ZVert ⥤q V) {k : Type u} [Field k] (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (E : (starTree L).ZVert → kˣ) (x : ↑Q.nonprojective) : kˣ

The descended relation scales.

noncomputable def MultiplicativeBasisDeformations.StarGauge.μD {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) {k : Type u} [Field k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (F : (starTree L).ZVert → (starTree L).ZVert → kˣ) {y x : V} (a : y ⟶ x) : kˣ

The descended arrow scales.

theorem MultiplicativeBasisDeformations.StarGauge.E_iter {t : ℕ} {L : Fin t → ℕ} {k : Type u} [Field k] (σ : 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) (E : (starTree L).ZVert → kˣ) (hE : ∀ (X : (starTree L).ZVert), E (gZ σ hσ c0 hσp X) = E X) (n : ℕ) (X : (starTree L).ZVert) : E ((gZ σ hσ c0 hσp)^[n] X) = E X

theorem MultiplicativeBasisDeformations.StarGauge.F_iter {t : ℕ} {L : Fin t → ℕ} {k : Type u} [Field k] (σ : 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) (F : (starTree L).ZVert → (starTree L).ZVert → kˣ) (hF : ∀ (Y X : (starTree L).ZVert), F (gZ σ hσ c0 hσp Y) (gZ σ hσ c0 hσp X) = F Y X) (n : ℕ) (Y X : (starTree L).ZVert) : F ((gZ σ hσ c0 hσp)^[n] Y) ((gZ σ hσ c0 hσp)^[n] X) = F Y X

theorem MultiplicativeBasisDeformations.StarGauge.ηD_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} [Field k] [(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) (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) (E : (starTree L).ZVert → kˣ) (hE : ∀ (X : (starTree L).ZVert), E (gZ σ hσ c0 hσp X) = E X) (X : (starTree L).ZVert) : ηD π hsurj E ⟨π.obj X, ⋯⟩ = E X

theorem MultiplicativeBasisDeformations.StarGauge.F_fibre {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) {k : Type u} [Field k] [(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) (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) (F : (starTree L).ZVert → (starTree L).ZVert → kˣ) (hF : ∀ (Y X : (starTree L).ZVert), F (gZ σ hσ c0 hσp Y) (gZ σ hσ c0 hσp X) = F Y X) {X X' Y Y' : (starTree L).ZVert} (hX : π.obj X' = π.obj X) (hY : π.obj Y' = π.obj Y) (A : Y ⟶ X) (A' : Y' ⟶ X') : F Y' X' = F Y X

theorem MultiplicativeBasisDeformations.StarGauge.μD_eq {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) {k : Type u} [Field k] [(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) (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) (F : (starTree L).ZVert → (starTree L).ZVert → kˣ) (hF : ∀ (Y X : (starTree L).ZVert), F (gZ σ hσ c0 hσp Y) (gZ σ hσ c0 hσp X) = F Y X) {Y X : (starTree L).ZVert} (A : Y ⟶ X) : μD π hπ hsurj F (π.map A) = F Y X

theorem MultiplicativeBasisDeformations.StarGauge.μD_congr {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) {k : Type u} [Field k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (F : (starTree L).ZVert → (starTree L).ZVert → kˣ) {y x y' x' : V} (a : y ⟶ x) (a' : y' ⟶ x') (hy : y = y') (hx : x = x') : μD π hπ hsurj F a = μD π hπ hsurj F a'