The covering ℤΔ → Q of a periodic component

Proof of Proposition 4.1, Step 1 (periodic-mesh-calculations.tex): "Define π(p, j) = τ^{-j}(end p). ... At the root the children give all outgoing arrows. At a nonroot path ending in a, the children give all outgoing arrows except σ^{-1} a; the repetition edge towards the parent gives that arrow. Thus π is bijective on outgoing stars, and mates give the same conclusion on incoming stars."

In height coordinates the vertex (p, t) of ℤΔ has t = 2j + |p|, and π(p, t) = τ^{-j}(end p).

theorem MultiplicativeBasisDeformations.star_bijective_of {W : Type v'} [Quiver W] {V : Type v} [Quiver V] [∀ (x y : W), Subsingleton (x ⟶ y)] [∀ (x y : V), Subsingleton (x ⟶ y)] (φ : W ⥤q V) {X : W} (hinj : ∀ {Y Y' : W}, Nonempty (X ⟶ Y) → Nonempty (X ⟶ Y') → φ.obj Y = φ.obj Y' → Y = Y') (hsurj : ∀ (y : V), Nonempty (φ.obj X ⟶ y) → ∃ (Y : W), Nonempty (X ⟶ Y) ∧ φ.obj Y = y) : Function.Bijective (φ.star X)

Bijectivity on outgoing stars, for quivers with at most one arrow between two vertices.

theorem MultiplicativeBasisDeformations.costar_bijective_of {W : Type v'} [Quiver W] {V : Type v} [Quiver V] [∀ (x y : W), Subsingleton (x ⟶ y)] [∀ (x y : V), Subsingleton (x ⟶ y)] (φ : W ⥤q V) {X : W} (hinj : ∀ {Y Y' : W}, Nonempty (Y ⟶ X) → Nonempty (Y' ⟶ X) → φ.obj Y = φ.obj Y' → Y = Y') (hsurj : ∀ (y : V), Nonempty (y ⟶ φ.obj X) → ∃ (Y : W), Nonempty (Y ⟶ X) ∧ φ.obj Y = y) : Function.Bijective (φ.costar X)

Bijectivity on incoming stars, for quivers with at most one arrow between two vertices.

theorem MultiplicativeBasisDeformations.eq_of_star_bijective {W : Type v'} [Quiver W] {V : Type v} [Quiver V] [∀ (x y : W), Subsingleton (x ⟶ y)] [∀ (x y : V), Subsingleton (x ⟶ y)] (φ : W ⥤q V) {X : W} (h : Function.Bijective (φ.star X)) {Y Y' : W} (hY : Nonempty (X ⟶ Y)) (hY' : Nonempty (X ⟶ Y')) (he : φ.obj Y = φ.obj Y') : Y = Y'

theorem MultiplicativeBasisDeformations.exists_of_star_bijective {W : Type v'} [Quiver W] {V : Type v} [Quiver V] [∀ (x y : W), Subsingleton (x ⟶ y)] [∀ (x y : V), Subsingleton (x ⟶ y)] (φ : W ⥤q V) {X : W} (h : Function.Bijective (φ.star X)) {y : V} (hy : Nonempty (φ.obj X ⟶ y)) : ∃ (Y : W), Nonempty (X ⟶ Y) ∧ φ.obj Y = y

theorem MultiplicativeBasisDeformations.exists_of_costar_bijective {W : Type v'} [Quiver W] {V : Type v} [Quiver V] [∀ (x y : W), Subsingleton (x ⟶ y)] [∀ (x y : V), Subsingleton (x ⟶ y)] (φ : W ⥤q V) {X : W} (h : Function.Bijective (φ.costar X)) {y : V} (hy : Nonempty (y ⟶ φ.obj X)) : ∃ (Y : W), Nonempty (Y ⟶ X) ∧ φ.obj Y = y

theorem MultiplicativeBasisDeformations.TranslationQuiver.isMeshPair_iff {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {u e w : V} (a : u ⟶ e) (b : e ⟶ w) : Q.IsMeshPair ⟨u, ⟨e, a⟩⟩ ⟨e, ⟨w, b⟩⟩ ↔ u = hQ.tauE w

In a stable quiver with at most one arrow between two vertices, consecutive arrows u → e → w form a mesh pair exactly when u = τ w.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.not_isMeshPair_of_sectional {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} {x₀ u e w : V} (p' : Quiver.Path x₀ u) (a : u ⟶ e) (b : e ⟶ w) (h : Q.IsSectional ((p'.cons a).cons b)) : ¬Q.IsMeshPair ⟨u, ⟨e, a⟩⟩ ⟨e, ⟨w, b⟩⟩

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.isSectional_cons {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} {x₀ y w : V} (p : Quiver.Path x₀ y) (hp : Q.IsSectional p) (b : y ⟶ w) (hb : ∀ {u : V} (p' : Quiver.Path x₀ u) (a : u ⟶ y), p = p'.cons a → ¬Q.IsMeshPair ⟨u, ⟨y, a⟩⟩ ⟨y, ⟨w, b⟩⟩) : Q.IsSectional (p.cons b)

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.jco {V : Type v} [Quiver V] {Q : TranslationQuiver V} (x₀ : V) (X : tree.ZVert) : ℤ

The repetition coordinate j of a vertex (p, t) of ℤΔ, with t = 2j + |p|.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.two_mul_jco {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (x₀ : V) (X : tree.ZVert) : 2 * jco x₀ X = X.t - ↑X.v.len

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piV {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (x₀ : V) (X : tree.ZVert) : V

The covering map π(p, t) = τ^{-j}(end p).

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.tauE_zpow_neg_sub_one {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (n : ℤ) (v : V) : (hQ.tauE ^ (-(n - 1))) v = hQ.tauE ((hQ.tauE ^ (-n)) v)

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.tauE_zpow_neg_add_one {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (n : ℤ) (v : V) : (hQ.tauE ^ (-n)) v = (hQ.tauE ^ (-(n + 1))) (hQ.tauE v)

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.jco_child {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} {x₀ : V} {X Y : tree.ZVert} (h : X.v.IsParent Y.v) (ht : Y.t = X.t + 1) : jco x₀ Y = jco x₀ X

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.jco_parent {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} {x₀ : V} {X Y : tree.ZVert} (h : Y.v.IsParent X.v) (ht : Y.t = X.t + 1) : jco x₀ Y = jco x₀ X + 1

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.endv_of_isParent {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} {x₀ : V} {p q : Q.SecPath x₀} {w : V} {a : p.endv ⟶ w} (h : ↑q = ⟨w, (↑p).snd.cons a⟩) : q.endv = w

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.nonempty_piV {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} {X Y : tree.ZVert} (a : X ⟶ Y) : Nonempty (piV hQ x₀ X ⟶ piV hQ x₀ Y)

Arrows of ℤΔ map to arrows of Q.

noncomputable def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piQ {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} : tree.ZVert ⥤q V

The covering map π : ℤΔ → Q.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piV_ztau {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} (X : tree.ZVert) : piV hQ x₀ (tree.ztau X) = hQ.tauE (piV hQ x₀ X)

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piV_child {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} {X Y : tree.ZVert} {w : V} {b : X.v.endv ⟶ w} (hY : ↑Y.v = ⟨w, (↑X.v).snd.cons b⟩) (ht : Y.t = X.t + 1) : piV hQ x₀ Y = (hQ.tauE ^ (-jco x₀ X)) w

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piV_parent {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} {X Y : tree.ZVert} {e : V} {a : Y.v.endv ⟶ e} (hX : ↑X.v = ⟨e, (↑Y.v).snd.cons a⟩) (ht : Y.t = X.t + 1) : hQ.tauE (piV hQ x₀ Y) = (hQ.tauE ^ (-jco x₀ X)) Y.v.endv

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.zv {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} (p : Q.SecPath x₀) (t : ℤ) (ht : ↑t = ↑p.len) : tree.ZVert

A vertex of ℤΔ above the given sectional path, at height t.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.nonempty_hom_iff' {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} {x₀ : V} {X Y : tree.ZVert} : Nonempty (X ⟶ Y) ↔ (X.v.IsParent Y.v ∨ Y.v.IsParent X.v) ∧ Y.t = X.t + 1

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piV_child_ne_parent {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} {X Y Y' : tree.ZVert} (hc : X.v.IsParent Y.v) (ht : Y.t = X.t + 1) (hc' : Y'.v.IsParent X.v) (ht' : Y'.t = X.t + 1) : piV hQ x₀ Y ≠ piV hQ x₀ Y'

A child and the parent of a vertex of Δ have different images.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.exists_child {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} (X : tree.ZVert) {z : V} (b : X.v.endv ⟶ z) (hsec : Q.IsSectional ((↑X.v).snd.cons b)) : ∃ (Y : tree.ZVert), Nonempty (X ⟶ Y) ∧ piV hQ x₀ Y = (hQ.tauE ^ (-jco x₀ X)) z

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.exists_parent {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} (X : tree.ZVert) {u : V} (p' : Quiver.Path x₀ u) (a : u ⟶ X.v.endv) (hX : ↑X.v = ⟨X.v.endv, p'.cons a⟩) (hsec : Q.IsSectional p') : ∃ (Y : tree.ZVert), Nonempty (X ⟶ Y) ∧ hQ.tauE (piV hQ x₀ Y) = (hQ.tauE ^ (-jco x₀ X)) u

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piQ_star_bijective {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} (X : tree.ZVert) : Function.Bijective ((piQ hQ).star X)

π is bijective on outgoing stars.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piQ_costar_bijective {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} (X : tree.ZVert) : Function.Bijective ((piQ hQ).costar X)

π is bijective on incoming stars ("mates give the same conclusion on incoming stars").

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piQ_isCovering {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} : (piQ hQ).IsCovering

π : ℤΔ → Q is a covering of quivers.

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.rootZ {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} : tree.ZVert

The root at height 0.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piV_rootZ {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} : piV hQ x₀ rootZ = x₀

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.ConnAdj {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (a b : V) : Prop

Adjacency in Q together with the translation edges.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piV_surjective_of_conn {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ v : V} (hv : Relation.EqvGen (ConnAdj hQ) x₀ v) : ∃ (X : tree.ZVert), piV hQ x₀ X = v

The image of π is the whole component of x₀.