Proposition 4.1: the periodic tree model

prop:periodic-tree-model (scalar-normalization.tex), parts (1) and (3): a finite connected stable translation quiver with at most one arrow between two vertices, containing an arrow and carrying a finite-dimensional scalar mesh category, is covered by the repetition ℤΔ of a Dynkin star model Δ; the covering commutes with translation and is surjective. Combined with StarDeck.deck_cyclic, its fibres are the orbits of an infinite cyclic group of translation-commuting automorphisms acting freely.

The proof assembles Steps 1–4 (SectionalCover, SectionalDynkin, ModelDeck), transporting the covering from the tree of sectional paths to the star model along the isomorphism of Step 2 (ZTransport).

theorem MultiplicativeBasisDeformations.TranslationQuiver.card_starV_zero (L : Fin 0 → ℕ) (x y : StarV L) : x = y

theorem MultiplicativeBasisDeformations.TranslationQuiver.periodic_model {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), (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

Proposition 4.1 (1): the periodic tree model of a component.