Proposition 4.1(2): the generator of the deck group

scalar-normalization.tex (prop:periodic-tree-model(2)): "Root Δ at its trivalent vertex if Δ has type D or E, and at its middle vertex if Δ = A_{2n+1}, and orient Δ away from the root. Then Θ is generated by τ^s ρ for some s ≥ 1, where ρ is the automorphism (v, j) ↦ (ρ v, j) of ℤΔ induced by an automorphism ρ of Δ; it fixes the root. If Δ = A_{2n}, then Θ is generated by η^r for some r ≥ 1, where η is an automorphism of ℤΔ with η² = τ⁻¹ that exchanges the two halves of Δ."

The star models of PeriodicModel.lean use height coordinates (v, j), j ≡ depth v (mod 2), with τ(v, j) = (v, j − 2); type A is a one-arm star. The deck group is infinite cyclic, generated by g = deck z₀ (deck_cyclic), and g(v, j) = (ρ v, j + c₀) for a tree automorphism ρ (deck_height_form). Comparing parities: a three-arm star has ρ fixing the centre (fixes_centre_three), so c₀ = 2s and g = τ^{−s} ρ; a path has ρ the identity or the reversal (path_aut), which fixes the middle vertex when the number of vertices is odd; for A_{2n} the reversal changes parity, and g = η^{c₀} with η(v, j) = (rev v, j + 1). (We state the generator g; its inverse τ^s ρ⁻¹ is the form of the source.)

theorem MultiplicativeBasisDeformations.StarDeck.par_eq {t : ℕ} {L : Fin t → ℕ} (x : StarV L) : (starTree L).par x = ↑(starDepth x)

theorem MultiplicativeBasisDeformations.StarDeck.natCast_zmod2_eq {a b : ℕ} (h : a % 2 = b % 2) : ↑a = ↑b

theorem MultiplicativeBasisDeformations.StarDeck.zmod2_mod_eq {a b : ℕ} (h : ↑a = ↑b) : a % 2 = b % 2

The reversal of a path and η

def MultiplicativeBasisDeformations.StarDeck.rev {L : Fin 1 → ℕ} (x : StarV L) : StarV L

The reversal of a path: depth d ↦ L₀ + 1 − d.

theorem MultiplicativeBasisDeformations.StarDeck.depth_rev {L : Fin 1 → ℕ} (x : StarV L) : starDepth (rev x) = L 0 + 1 - starDepth x

theorem MultiplicativeBasisDeformations.StarDeck.rev_rev {L : Fin 1 → ℕ} (x : StarV L) : rev (rev x) = x

def MultiplicativeBasisDeformations.StarDeck.eta {L : Fin 1 → ℕ} (hodd : Odd (L 0 + 1)) (X : (starTree L).ZVert) : (starTree L).ZVert

η (for A_{2n}, L₀ + 1 odd): (v, j) ↦ (rev v, j + 1).

theorem MultiplicativeBasisDeformations.StarDeck.eta_v {L : Fin 1 → ℕ} (hodd : Odd (L 0 + 1)) (X : (starTree L).ZVert) : (eta hodd X).v = rev X.v

theorem MultiplicativeBasisDeformations.StarDeck.eta_t {L : Fin 1 → ℕ} (hodd : Odd (L 0 + 1)) (X : (starTree L).ZVert) : (eta hodd X).t = X.t + 1

theorem MultiplicativeBasisDeformations.StarDeck.eta_eta {L : Fin 1 → ℕ} (hodd : Odd (L 0 + 1)) (X : (starTree L).ZVert) : eta hodd (eta hodd X) = (starTree L).ztauInv X

η² = τ⁻¹.

theorem MultiplicativeBasisDeformations.StarDeck.eta_iter {L : Fin 1 → ℕ} (hodd : Odd (L 0 + 1)) (n : ℕ) (X : (starTree L).ZVert) : (((eta hodd)^[n] X).v = if Even n then X.v else rev X.v) ∧ ((eta hodd)^[n] X).t = X.t + ↑n

The generator

theorem MultiplicativeBasisDeformations.StarDeck.periodicTreeModel_generator {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (ht : 0 < t) (hcl : t = 1 ∨ t = 3) (hnt : ∃ (X : (starTree L).ZVert) (Y : (starTree L).ZVert), X ≠ Y ∧ π.obj X = π.obj Y) : ∃ (g : Equiv.Perm (starTree L).ZVert), (∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y ↔ ∃ (l : ℤ), (g ^ l) X = Y) ∧ ∃ (c₀ : ℕ) (ρ : StarV L ≃ StarV L), 1 ≤ c₀ ∧ (∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) ∧ (∀ (X : (starTree L).ZVert), (g X).v = ρ X.v ∧ (g X).t = X.t + ↑c₀) ∧ (t = 3 → Even c₀ ∧ ρ none = none) ∧ (t = 1 → Even (L ⟨0, ht⟩ + 1) → Even c₀ ∧ ∀ (x : StarV L), 2 * starDepth x = L ⟨0, ht⟩ + 1 → ρ x = x) ∧ (t = 1 → Odd (L ⟨0, ht⟩ + 1) → (Even c₀ ∧ ∀ (x : StarV L), ρ x = x) ∨ Odd c₀ ∧ ∀ (x : StarV L), starDepth (ρ x) + starDepth x = L ⟨0, ht⟩ + 1)

Proposition 4.1(2) (prop:periodic-tree-model(2)), in height coordinates: the deck group is generated by g with g(v, j) = (ρ v, j + c₀), c₀ ≥ 1, ρ a tree automorphism. For a three-arm star (types D, E) c₀ is even and ρ fixes the centre: g = τ^{−c₀/2} ρ. For a path with an odd number of vertices (A_{2n+1}) c₀ is even and ρ fixes the middle vertex. For a path with an even number of vertices (A_{2n}) either c₀ is even and ρ = 1, or c₀ is odd and ρ is the reversal; in both cases g = η^{c₀} (generator_A_even).

theorem MultiplicativeBasisDeformations.StarDeck.generator_A_even {L : Fin 1 → ℕ} (hodd : Odd (L 0 + 1)) (g : (starTree L).ZVert → (starTree L).ZVert) (c₀ : ℕ) (ρ : StarV L ≃ StarV L) (hg : ∀ (X : (starTree L).ZVert), (g X).v = ρ X.v ∧ (g X).t = X.t + ↑c₀) (h : (Even c₀ ∧ ∀ (x : StarV L), ρ x = x) ∨ Odd c₀ ∧ ∀ (x : StarV L), starDepth (ρ x) + starDepth x = L 0 + 1) (X : (starTree L).ZVert) : g X = (eta hodd)^[c₀] X

Proposition 4.1(2) for A_{2n}: the generator of generator form is η^{c₀}.

theorem MultiplicativeBasisDeformations.TranslationQuiver.infinite_zvert {t : ℕ} (L : Fin t → ℕ) : Infinite (starTree L).ZVert

ℤΔ is infinite.

theorem MultiplicativeBasisDeformations.TranslationQuiver.periodicTreeModel {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [Field k] [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (hQ : Q.IsStable) (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {x₀ y₀ : V} (a₀ : x₀ ⟶ y₀) (hconn : ∀ (v : V), Relation.EqvGen (SecPath.ConnAdj hQ) x₀ v) : ∃ (t : ℕ) (L : Fin t → ℕ) (π : (starTree L).ZVert ⥤q V) (ht : 0 < t), (t = 1 ∨ t = 3 ∧ ∑ i : Fin t, (↑(L i) + 1) / (↑(L i) + 2) < 2) ∧ π.IsCovering ∧ (∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) ∧ Function.Surjective π.obj ∧ ∃ (g : Equiv.Perm (starTree L).ZVert), (∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y ↔ ∃ (l : ℤ), (g ^ l) X = Y) ∧ ∃ (c₀ : ℕ) (ρ : StarV L ≃ StarV L), 1 ≤ c₀ ∧ (∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) ∧ (∀ (X : (starTree L).ZVert), (g X).v = ρ X.v ∧ (g X).t = X.t + ↑c₀) ∧ (t = 3 → Even c₀ ∧ ρ none = none) ∧ (t = 1 → Even (L ⟨0, ht⟩ + 1) → Even c₀ ∧ ∀ (x : StarV L), 2 * starDepth x = L ⟨0, ht⟩ + 1 → ρ x = x) ∧ (t = 1 → Odd (L ⟨0, ht⟩ + 1) → (Even c₀ ∧ ∀ (x : StarV L), ρ x = x) ∨ Odd c₀ ∧ ∀ (x : StarV L), starDepth (ρ x) + starDepth x = L ⟨0, ht⟩ + 1)

Proposition 4.1(1)(2) for a finite connected component: the covering ℤΔ → Q by a Dynkin star model, and the generator of the deck group in the form of periodicTreeModel_generator.