Deck transformations of ℤΔ → Q

Proof of Proposition 4.1, Steps 3 and 4 (periodic-mesh-calculations.tex).

• A map over π preserving arrows is determined by its value at one vertex ("by unique lifting of undirected walks") — eq_of_over.
• A translation-commuting automorphism of ℤΔ has the form (v, t) ↦ (ρ v, t + c₀) in height coordinates: "Every quiver arrow increases the height by one ... the difference H(Fx) - H(x) is therefore constant along arrows and hence constant on the connected quiver. Its action on translation orbits is a tree automorphism ρ" — height_form.

def MultiplicativeBasisDeformations.OrientedTree.ZAdj {D : Type v} (T : OrientedTree D) (X Y : T.ZVert) : Prop

Two vertices of ℤΔ joined by an arrow in either direction.

def MultiplicativeBasisDeformations.OrientedTree.ZConnected {D : Type v} (T : OrientedTree D) : Prop

ℤΔ is connected.

theorem MultiplicativeBasisDeformations.OrientedTree.eq_of_over {D : Type v} (T : OrientedTree D) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (hW : T.ZConnected) (π : T.ZVert ⥤q V) (hπ : π.IsCovering) (F G : T.ZVert → T.ZVert) (hF : ∀ (X Y : T.ZVert), Nonempty (X ⟶ Y) → Nonempty (F X ⟶ F Y)) (hG : ∀ (X Y : T.ZVert), Nonempty (X ⟶ Y) → Nonempty (G X ⟶ G Y)) (hπF : ∀ (X : T.ZVert), π.obj (F X) = π.obj X) (hπG : ∀ (X : T.ZVert), π.obj (G X) = π.obj X) {X₀ : T.ZVert} (h₀ : F X₀ = G X₀) (X : T.ZVert) : F X = G X

Maps over a covering are determined by one value.

def MultiplicativeBasisDeformations.OrientedTree.baseZ {D : Type v} (T : OrientedTree D) (a : D) : T.ZVert

A vertex of ℤΔ over a, at a height of the right parity.

def MultiplicativeBasisDeformations.OrientedTree.upZ {D : Type v} (T : OrientedTree D) (X : T.ZVert) (n : ℕ) : T.ZVert

Moving up by 2n in height.

theorem MultiplicativeBasisDeformations.OrientedTree.ztau_upZ {D : Type v} (T : OrientedTree D) (X : T.ZVert) (n : ℕ) : T.ztau (T.upZ X (n + 1)) = T.upZ X n

theorem MultiplicativeBasisDeformations.OrientedTree.eq_upZ_or {D : Type v} (T : OrientedTree D) {X Y : T.ZVert} (h : X.v = Y.v) : (∃ (n : ℕ), Y = T.upZ X n) ∨ ∃ (n : ℕ), X = T.upZ Y n

theorem MultiplicativeBasisDeformations.OrientedTree.v_upZ {D : Type v} (T : OrientedTree D) (F : T.ZVert ≃ T.ZVert) (hτ : ∀ (X : T.ZVert), F (T.ztau X) = T.ztau (F X)) (X : T.ZVert) (n : ℕ) : (F (T.upZ X n)).v = (F X).v

theorem MultiplicativeBasisDeformations.OrientedTree.v_eq_of_v_eq {D : Type v} (T : OrientedTree D) (F : T.ZVert ≃ T.ZVert) (hτ : ∀ (X : T.ZVert), F (T.ztau X) = T.ztau (F X)) {X Y : T.ZVert} (h : X.v = Y.v) : (F X).v = (F Y).v

def MultiplicativeBasisDeformations.OrientedTree.aboveZ {D : Type v} (T : OrientedTree D) (X : T.ZVert) (b : D) (h : T.G.Adj X.v b) : T.ZVert

A vertex over b just above a vertex over an adjacent a.

theorem MultiplicativeBasisDeformations.OrientedTree.nonempty_hom_aboveZ {D : Type v} (T : OrientedTree D) (X : T.ZVert) (b : D) (h : T.G.Adj X.v b) : Nonempty (X ⟶ T.aboveZ X b h)

theorem MultiplicativeBasisDeformations.OrientedTree.height_form {D : Type v} (T : OrientedTree D) (F : T.ZVert ≃ T.ZVert) (hτ : ∀ (X : T.ZVert), F (T.ztau X) = T.ztau (F X)) [Nonempty D] (hW : T.ZConnected) (hF : ∀ (X Y : T.ZVert), Nonempty (X ⟶ Y) ↔ Nonempty (F X ⟶ F Y)) : ∃ (c₀ : ℤ) (ρ : D ≃ D), (∀ (a b : D), T.G.Adj a b ↔ T.G.Adj (ρ a) (ρ b)) ∧ ∀ (X : T.ZVert), (F X).v = ρ X.v ∧ (F X).t = X.t + c₀

Step 4: height coordinates of a translation-commuting automorphism (periodic-mesh-calculations.tex).