Deck transformations for star models

Proof of Proposition 4.1, Step 3 (periodic-mesh-calculations.tex), for the repetition of a star model Δ covering a finite stable translation quiver Q by π:

"For each z with π z = π o, construct a map H_z : R → R over π by sending o to z, lifting the rooted tree edges, and extending by translation and mates. Since Δ is a tree, these choices are consistent."

Here o is the centre at height 0; the rooted tree edges are the arms.

def MultiplicativeBasisDeformations.StarDeck.B {t : ℕ} (L : Fin t → ℕ) (x : StarV L) : (starTree L).ZVert

The base vertex of ℤΔ over a star vertex: height equal to its depth.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.StarDeck.o {t : ℕ} (L : Fin t → ℕ) : (starTree L).ZVert

The centre at height zero.

theorem MultiplicativeBasisDeformations.StarDeck.B_none_arrow {t : ℕ} (L : Fin t → ℕ) (i : Fin t) : Nonempty (B L none ⟶ B L (some ⟨i, 0⟩))

theorem MultiplicativeBasisDeformations.StarDeck.B_arm_arrow {t : ℕ} (L : Fin t → ℕ) (i : Fin t) (k : Fin (L i)) : Nonempty (B L (some ⟨i, k.castSucc⟩) ⟶ B L (some ⟨i, k.succ⟩))

def MultiplicativeBasisDeformations.StarDeck.nb {t : ℕ} {L : Fin t → ℕ} (ht : 0 < t) : StarV L → StarV L

A neighbour of each star vertex (when there is an arm).

theorem MultiplicativeBasisDeformations.StarDeck.adj_nb {t : ℕ} {L : Fin t → ℕ} (ht : 0 < t) (x : StarV L) : starAdj x (nb ht x)

theorem MultiplicativeBasisDeformations.StarDeck.zadj_up {t : ℕ} {L : Fin t → ℕ} (ht : 0 < t) (X : (starTree L).ZVert) : Relation.EqvGen (starTree L).ZAdj X ((starTree L).upZ X 1)

theorem MultiplicativeBasisDeformations.StarDeck.eqvGen_upZ {t : ℕ} {L : Fin t → ℕ} (ht : 0 < t) (X : (starTree L).ZVert) (n : ℕ) : Relation.EqvGen (starTree L).ZAdj X ((starTree L).upZ X n)

theorem MultiplicativeBasisDeformations.StarDeck.eqvGen_B {t : ℕ} {L : Fin t → ℕ} (x : StarV L) : Relation.EqvGen (starTree L).ZAdj (o L) (B L x)

theorem MultiplicativeBasisDeformations.StarDeck.zconnected {t : ℕ} {L : Fin t → ℕ} (ht : 0 < t) : (starTree L).ZConnected

ℤΔ is connected.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.StarDeck.τW {t : ℕ} (L : Fin t → ℕ) : Equiv.Perm (starTree L).ZVert

Translation of ℤΔ, as a permutation.

theorem MultiplicativeBasisDeformations.StarDeck.τW_apply {t : ℕ} (L : Fin t → ℕ) (X : (starTree L).ZVert) : (τW L) X = (starTree L).ztau X

theorem MultiplicativeBasisDeformations.StarDeck.τW_zpow_v {t : ℕ} (L : Fin t → ℕ) (n : ℤ) (X : (starTree L).ZVert) : ((τW L ^ n) X).v = X.v

theorem MultiplicativeBasisDeformations.StarDeck.τW_zpow_t {t : ℕ} (L : Fin t → ℕ) (n : ℤ) (X : (starTree L).ZVert) : ((τW L ^ n) X).t = X.t - 2 * n

def MultiplicativeBasisDeformations.StarDeck.jco {t : ℕ} (L : Fin t → ℕ) (X : (starTree L).ZVert) : ℤ

The repetition coordinate j, with t = depth + 2j.

theorem MultiplicativeBasisDeformations.StarDeck.two_mul_jco {t : ℕ} (L : Fin t → ℕ) (X : (starTree L).ZVert) : 2 * jco L X = X.t - ↑(starDepth X.v)

theorem MultiplicativeBasisDeformations.StarDeck.eq_τW_zpow_B {t : ℕ} (L : Fin t → ℕ) (X : (starTree L).ZVert) : X = (τW L ^ (-jco L X)) (B L X.v)

theorem MultiplicativeBasisDeformations.StarDeck.π_τW_zpow {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τ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (n : ℤ) (Y : (starTree L).ZVert) : π.obj ((τW L ^ n) Y) = (hQ.tauE ^ n) (π.obj Y)

noncomputable def MultiplicativeBasisDeformations.StarDeck.stepLift {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (X : (starTree L).ZVert) (y : V) (h : Nonempty (π.obj X ⟶ y)) : (starTree L).ZVert

One lifting step: the out-neighbour of X over a given out-neighbour of π X.

theorem MultiplicativeBasisDeformations.StarDeck.stepLift_spec {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (X : (starTree L).ZVert) (y : V) (h : Nonempty (π.obj X ⟶ y)) : Nonempty (X ⟶ stepLift L π hπ X y h) ∧ π.obj (stepLift L π hπ X y h) = y

def MultiplicativeBasisDeformations.StarDeck.liftArm {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (i : Fin t) (k : ℕ) (hk : k < L i + 1) : { Y : (starTree L).ZVert // π.obj Y = π.obj (B L (some ⟨i, ⟨k, hk⟩⟩)) }

Lifting the arm i from z.

theorem MultiplicativeBasisDeformations.StarDeck.liftArm_zero_arrow {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (i : Fin t) (hk : 0 < L i + 1) : Nonempty (z ⟶ ↑(liftArm L π hπ z hz i 0 hk))

theorem MultiplicativeBasisDeformations.StarDeck.liftArm_succ_arrow {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (i : Fin t) (k : ℕ) (hk : k + 1 < L i + 1) : Nonempty (↑(liftArm L π hπ z hz i k ⋯) ⟶ ↑(liftArm L π hπ z hz i (k + 1) hk))

noncomputable def MultiplicativeBasisDeformations.StarDeck.Lz {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) : StarV L → (starTree L).ZVert

The lift of the star from z.

theorem MultiplicativeBasisDeformations.StarDeck.π_Lz {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (x : StarV L) : π.obj (Lz L π hπ z hz x) = π.obj (B L x)

theorem MultiplicativeBasisDeformations.StarDeck.Lz_child {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) {x y : StarV L} (h : starAdj x y) (hd : starDepth y = starDepth x + 1) : Nonempty (Lz L π hπ z hz x ⟶ Lz L π hπ z hz y)

noncomputable def MultiplicativeBasisDeformations.StarDeck.Hz {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (X : (starTree L).ZVert) : (starTree L).ZVert

The deck transformation H_z (periodic-mesh-calculations.tex): lift the arms from z, then extend by translation.

theorem MultiplicativeBasisDeformations.StarDeck.π_Hz {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)) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (X : (starTree L).ZVert) : π.obj (Hz L π hπ z hz X) = π.obj X

theorem MultiplicativeBasisDeformations.StarDeck.Hz_o {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) : Hz L π hπ z hz (o L) = z

theorem MultiplicativeBasisDeformations.StarDeck.jco_ztau {t : ℕ} (L : Fin t → ℕ) (X : (starTree L).ZVert) : jco L ((starTree L).ztau X) = jco L X - 1

theorem MultiplicativeBasisDeformations.StarDeck.Hz_ztau {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (X : (starTree L).ZVert) : Hz L π hπ z hz ((starTree L).ztau X) = (starTree L).ztau (Hz L π hπ z hz X)

theorem MultiplicativeBasisDeformations.StarDeck.jco_child {t : ℕ} (L : Fin t → ℕ) {X Y : (starTree L).ZVert} (hd : starDepth Y.v = starDepth X.v + 1) (ht : Y.t = X.t + 1) : jco L Y = jco L X

theorem MultiplicativeBasisDeformations.StarDeck.jco_parent {t : ℕ} (L : Fin t → ℕ) {X Y : (starTree L).ZVert} (hd : starDepth X.v = starDepth Y.v + 1) (ht : Y.t = X.t + 1) : jco L Y = jco L X + 1

theorem MultiplicativeBasisDeformations.StarDeck.Hz_arrow {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) {X Y : (starTree L).ZVert} (h : Nonempty (X ⟶ Y)) : Nonempty (Hz L π hπ z hz X ⟶ Hz L π hπ z hz Y)

H_z preserves arrows ("extending by translation and mates").

theorem MultiplicativeBasisDeformations.StarDeck.Hz_out {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)) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) {X Y' : (starTree L).ZVert} (h : Nonempty (Hz L π hπ z hz X ⟶ Y')) : ∃ (Y : (starTree L).ZVert), Nonempty (X ⟶ Y) ∧ Hz L π hπ z hz Y = Y'

The image of H_z is closed under neighbours (outgoing).

theorem MultiplicativeBasisDeformations.StarDeck.Hz_in {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)) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) {X Y' : (starTree L).ZVert} (h : Nonempty (Y' ⟶ Hz L π hπ z hz X)) : ∃ (Y : (starTree L).ZVert), Nonempty (Y ⟶ X) ∧ Hz L π hπ z hz Y = Y'

The image of H_z is closed under neighbours (incoming).

theorem MultiplicativeBasisDeformations.StarDeck.Hz_surjective {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) : Function.Surjective (Hz L π hπ z hz)

H_z is surjective ("Its image is closed under neighbours and it is surjective").

theorem MultiplicativeBasisDeformations.StarDeck.Hz_comp {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (z' : (starTree L).ZVert) (hz' : π.obj z' = π.obj (o L)) (X : (starTree L).ZVert) : Hz L π hπ z hz (Hz L π hπ z' hz' X) = Hz L π hπ (Hz L π hπ z hz z') ⋯ X

theorem MultiplicativeBasisDeformations.StarDeck.Hz_eq_self_of {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) {X₀ : (starTree L).ZVert} (h₀ : Hz L π hπ z hz X₀ = X₀) (X : (starTree L).ZVert) : Hz L π hπ z hz X = X

theorem MultiplicativeBasisDeformations.StarDeck.Hz_bijective {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) : Function.Bijective (Hz L π hπ z hz)

H_z is an automorphism.

theorem MultiplicativeBasisDeformations.StarDeck.Hz_τW_zpow {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)) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (n : ℤ) (X : (starTree L).ZVert) : Hz L π hπ z hz ((τW L ^ n) X) = (τW L ^ n) (Hz L π hπ z hz X)

theorem MultiplicativeBasisDeformations.StarDeck.fibre_B_arm {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)) (i : Fin t) (k : ℕ) (hk : k < L i + 1) (Y : (starTree L).ZVert) : π.obj Y = π.obj (B L (some ⟨i, ⟨k, hk⟩⟩)) → ∃ (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)), Hz L π hπ z hz (B L (some ⟨i, ⟨k, hk⟩⟩)) = Y

theorem MultiplicativeBasisDeformations.StarDeck.fibre_transitive {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)) {X Y : (starTree L).ZVert} (h : π.obj X = π.obj Y) : ∃ (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)), Hz L π hπ z hz X = Y

The deck group is transitive on fibres (periodic-mesh-calculations.tex).

noncomputable def MultiplicativeBasisDeformations.StarDeck.deck {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) : Equiv.Perm (starTree L).ZVert

The deck transformation H_z, as a permutation.

theorem MultiplicativeBasisDeformations.StarDeck.deck_apply {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (X : (starTree L).ZVert) : (deck L hQ π hπ hτ ht z hz) X = Hz L π hπ z hz X

theorem MultiplicativeBasisDeformations.StarDeck.deck_arrow_iff {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (X Y : (starTree L).ZVert) : Nonempty (X ⟶ Y) ↔ Nonempty ((deck L hQ π hπ hτ ht z hz) X ⟶ (deck L hQ π hπ hτ ht z hz) Y)

theorem MultiplicativeBasisDeformations.StarDeck.deck_height_form {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) : ∃ (ρ : StarV L ≃ StarV L), (∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) ∧ ∀ (X : (starTree L).ZVert), (Hz L π hπ z hz X).v = ρ X.v ∧ (Hz L π hπ z hz X).t = X.t + z.t

Height form of the deck transformations: H_z (v, t) = (ρ v, t + z.t).

theorem MultiplicativeBasisDeformations.StarDeck.Hz_eq_id_of_t {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (h0 : z.t = 0) (X : (starTree L).ZVert) : Hz L π hπ z hz X = X

A height-preserving deck transformation is the identity ("a kernel element fixes a root vertex and the deck action is free").

theorem MultiplicativeBasisDeformations.StarDeck.Hz_t {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) (z : (starTree L).ZVert) (hz : π.obj z = π.obj (o L)) (X : (starTree L).ZVert) : (Hz L π hπ z hz X).t = X.t + z.t

theorem MultiplicativeBasisDeformations.StarDeck.Hz_o_id {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) (X : (starTree L).ZVert) : Hz L π hπ (o L) ⋯ X = X

theorem MultiplicativeBasisDeformations.StarDeck.Hz_congr {t : ℕ} (L : Fin t → ℕ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) {w w' : (starTree L).ZVert} (h : w = w') (hw : π.obj w = π.obj (o L)) (hw' : π.obj w' = π.obj (o L)) (X : (starTree L).ZVert) : Hz L π hπ w hw X = Hz L π hπ w' hw' X

theorem MultiplicativeBasisDeformations.StarDeck.deck_zpow {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) (z₀ : (starTree L).ZVert) (hz₀ : π.obj z₀ = π.obj (o L)) (l : ℤ) : ∃ (w : (starTree L).ZVert) (hw : π.obj w = π.obj (o L)), w.t = l * z₀.t ∧ ∀ (X : (starTree L).ZVert), (deck L hQ π hπ hτ ht z₀ hz₀ ^ l) X = Hz L π hπ w hw X

Powers of a deck transformation are deck transformations.

theorem MultiplicativeBasisDeformations.StarDeck.eq_of_t_eq {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) {w w' : (starTree L).ZVert} (hw : π.obj w = π.obj (o L)) (hw' : π.obj w' = π.obj (o L)) (h : w.t = w'.t) : w = w'

Deck transformations with the same height shift coincide.

theorem MultiplicativeBasisDeformations.StarDeck.deck_cyclic {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) : ∃ (z₀ : (starTree L).ZVert) (hz₀ : π.obj z₀ = π.obj (o L)), 0 < z₀.t ∧ ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y ↔ ∃ (l : ℤ), (deck L hQ π hπ hτ ht z₀ hz₀ ^ l) X = Y

Step 4: the deck group is infinite cyclic, and the fibres of π are its orbits (periodic-mesh-calculations.tex).