Lifted paths and row classes (Lemma A.2)

lem:twisted-trace-surjection (periodic-mesh-calculations.tex). Let π : ℤΔ → Q be a covering commuting with translation, with signed mesh coefficients. A path p of the doubled tree Δ̄ starting at v lifts to ℤΔ from τ X for any X = (v, t) (liftZ); the class of the image of the lift in coker D_m is phiD X p. Since contextual relations of Π(Δ) lift term by term with the same endpoints and heights, the linear extension phiL X of phiD X kills the ideal of Π(Δ) (phiL_eq_zero_of_mem).

theorem MultiplicativeBasisDeformations.Prefunctor.mapPath_cast {U : Type u_1} {W : Type u_2} [Quiver U] [Quiver W] (φ : U ⥤q W) {a b a' b' : U} (ha : a = a') (hb : b = b') (p : Quiver.Path a b) : φ.mapPath (Quiver.Path.cast ha hb p) = Quiver.Path.cast ⋯ ⋯ (φ.mapPath p)

theorem MultiplicativeBasisDeformations.OrientedTree.par_path {D : Type v} (T : OrientedTree D) {a b : T.Dbl} (p : Quiver.Path a b) : T.par b = T.par a + ↑p.length

def MultiplicativeBasisDeformations.OrientedTree.liftEnd {D : Type v} (T : OrientedTree D) (Y : T.ZVert) {b : T.Dbl} (p : Quiver.Path (T.toDbl Y.v) b) : T.ZVert

The vertex of ℤΔ at the end of the lift of a path of Δ̄ from Y.

theorem MultiplicativeBasisDeformations.OrientedTree.liftEnd_nil {D : Type v} (T : OrientedTree D) (Y : T.ZVert) : Y = T.liftEnd Y Quiver.Path.nil

theorem MultiplicativeBasisDeformations.OrientedTree.liftEnd_congr {D : Type v} (T : OrientedTree D) (Y : T.ZVert) {b : T.Dbl} {p q : Quiver.Path (T.toDbl Y.v) b} (h : p.length = q.length) : T.liftEnd Y p = T.liftEnd Y q

def MultiplicativeBasisDeformations.OrientedTree.liftZ {D : Type v} (T : OrientedTree D) (Y : T.ZVert) {b : T.Dbl} (p : Quiver.Path (T.toDbl Y.v) b) : Quiver.Path Y (T.liftEnd Y p)

The lift of a path of Δ̄ to ℤΔ from Y: heights increase by one along each arrow.

theorem MultiplicativeBasisDeformations.OrientedTree.forget_mapPath_liftZ {D : Type v} (T : OrientedTree D) (Y : T.ZVert) {b : T.Dbl} (p : Quiver.Path (T.toDbl Y.v) b) : T.forget.mapPath (T.liftZ Y p) = p

theorem MultiplicativeBasisDeformations.OrientedTree.length_liftZ {D : Type v} (T : OrientedTree D) (Y : T.ZVert) {b : T.Dbl} (p : Quiver.Path (T.toDbl Y.v) b) : (T.liftZ Y p).length = p.length

theorem MultiplicativeBasisDeformations.OrientedTree.pathStar_eq_of_forget {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] {Y E E' : T.ZVert} (P : Quiver.Path Y E) (P' : Quiver.Path Y E') (h : ⟨T.forget.obj E, T.forget.mapPath P⟩ = ⟨T.forget.obj E', T.forget.mapPath P'⟩) : ⟨E, P⟩ = ⟨E', P'⟩

Two paths of ℤΔ from the same vertex with the same image in Δ̄ are equal.

noncomputable def MultiplicativeBasisDeformations.OrientedTree.rowZ {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (m : ℕ) {X Y : T.ZVert} (P : Quiver.Path X Y) : ScalarMeshCategory.Coker c m

The row class of the image of a path of ℤΔ.

theorem MultiplicativeBasisDeformations.OrientedTree.rowZ_cast {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (m : ℕ) {X Y X' Y' : T.ZVert} (hX : X = X') (hY : Y = Y') (P : Quiver.Path X Y) : T.rowZ hQ π c m (Quiver.Path.cast hX hY P) = T.rowZ hQ π c m P

theorem MultiplicativeBasisDeformations.OrientedTree.rowZ_eq_of_pathStar {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] {m : ℕ} {X Y Y' : T.ZVert} {P : Quiver.Path X Y} {P' : Quiver.Path X Y'} (h : ⟨Y, P⟩ = ⟨Y', P'⟩) : T.rowZ hQ π c m P = T.rowZ hQ π c m P'

noncomputable def MultiplicativeBasisDeformations.OrientedTree.rowZL {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (m : ℕ) (X Y : T.ZVert) : (LinearPaths.obj X ⟶ LinearPaths.obj Y) →ₗ[k] ScalarMeshCategory.Coker c m

The linear extension of rowZ.

theorem MultiplicativeBasisDeformations.OrientedTree.pathMor_cast {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] {x y x' y' : V} (hx : x = x') (hy : y = y') (w : Quiver.Path x y) : ScalarMeshCategory.pathMor c (Quiver.Path.cast hx hy w) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ScalarMeshCategory.pathMor c w) (CategoryTheory.eqToHom ⋯))

theorem MultiplicativeBasisDeformations.OrientedTree.rowZL_eq_zero_of_mem {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (m : ℕ) {X Y : T.ZVert} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ (RelSystem.mesh (T.pullCoeff hQ π c)).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : (T.rowZL hQ π c m X Y) f = 0

Mesh relations of ℤΔ give zero row classes: the linear extension of rowZ kills the mesh ideal.

noncomputable def MultiplicativeBasisDeformations.OrientedTree.phiD {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (m : ℕ) (X : T.ZVert) {b : T.Dbl} (p : Quiver.Path (T.toDbl X.v) b) : ScalarMeshCategory.Coker c m

The row class of the lift of a path of Δ̄ from τ X.

noncomputable def MultiplicativeBasisDeformations.OrientedTree.phiL {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (m : ℕ) (X : T.ZVert) (b : T.Dbl) : (LinearPaths.obj (T.toDbl X.v) ⟶ LinearPaths.obj b) →ₗ[k] ScalarMeshCategory.Coker c m

The linear extension of phiD.

noncomputable def MultiplicativeBasisDeformations.OrientedTree.liftN {D : Type v} (T : OrientedTree D) {k : Type u} [CommRing k] (Y : T.ZVert) {b : T.Dbl} (p₀ : Quiver.Path (T.toDbl Y.v) b) : (LinearPaths.obj (T.toDbl Y.v) ⟶ LinearPaths.obj b) →ₗ[k] LinearPaths.obj Y ⟶ LinearPaths.obj (T.liftEnd Y p₀)

Lifting combinations of paths of a fixed length, which share their end.

theorem MultiplicativeBasisDeformations.OrientedTree.liftN_induction {D : Type v} (T : OrientedTree D) {k : Type u} [CommRing k] [Fintype D] [DecidableEq D] {Y : T.ZVert} {b : T.Dbl} (p₀ : Quiver.Path (T.toDbl Y.v) b) {P : (LinearPaths.obj (T.toDbl Y.v) ⟶ LinearPaths.obj b) → Prop} (h0 : P 0) (hadd : ∀ (f g : LinearPaths.obj (T.toDbl Y.v) ⟶ LinearPaths.obj b), P f → P g → P (f + g)) (hsmul : ∀ (a : k) (f : LinearPaths.obj (T.toDbl Y.v) ⟶ LinearPaths.obj b), P f → P (a • f)) (hp : ∀ (p : Quiver.Path (T.toDbl Y.v) b), p.length = p₀.length → P (LinearPaths.path p)) {f : LinearPaths.obj (T.toDbl Y.v) ⟶ LinearPaths.obj b} (hf : f ∈ LinearPaths.degreePart p₀.length (T.toDbl Y.v) b) : P f

theorem MultiplicativeBasisDeformations.OrientedTree.forget_liftN {D : Type v} (T : OrientedTree D) {k : Type u} [CommRing k] [Fintype D] [DecidableEq D] (Y : T.ZVert) {b : T.Dbl} (p₀ : Quiver.Path (T.toDbl Y.v) b) {f : LinearPaths.obj (T.toDbl Y.v) ⟶ LinearPaths.obj b} (hf : f ∈ LinearPaths.degreePart p₀.length (T.toDbl Y.v) b) : (LinearPaths.mapPaths T.forget Y (T.liftEnd Y p₀)) ((T.liftN Y p₀) f) = f

theorem MultiplicativeBasisDeformations.OrientedTree.rowZL_liftN {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (m : ℕ) (X : T.ZVert) {b : T.Dbl} (p₀ : Quiver.Path (T.toDbl X.v) b) {f : LinearPaths.obj (T.toDbl X.v) ⟶ LinearPaths.obj b} (hf : f ∈ LinearPaths.degreePart p₀.length (T.toDbl X.v) b) : (T.rowZL hQ π c m (T.ztau X) (T.liftEnd (T.ztau X) p₀)) ((T.liftN (T.ztau X) p₀) f) = (T.phiL hQ π c m X b) f

theorem MultiplicativeBasisDeformations.OrientedTree.preprojRel_mem_degreePart {D : Type v} (T : OrientedTree D) {k : Type u} [CommRing k] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (i : T.Dbl) : T.preprojRel k i ∈ LinearPaths.degreePart 2 i i

theorem MultiplicativeBasisDeformations.OrientedTree.phiL_eq_zero_of_mem {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hsig : T.pullCoeff hQ π c = T.zSigned k) (m : ℕ) (X : T.ZVert) {b : T.Dbl} {f : LinearPaths.obj (T.toDbl X.v) ⟶ LinearPaths.obj b} (hf : f ∈ (T.preproj k).ideal (LinearPaths.obj (T.toDbl X.v)) (LinearPaths.obj b)) : (T.phiL hQ π c m X b) f = 0

Relations of Π(Δ) give zero row classes (proof of Lemma A.2: "contextual mesh relations lift term by term with the same endpoints and heights").

Rotation

theorem MultiplicativeBasisDeformations.OrientedTree.rowQ_rotate' {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (hc : ScalarMeshCategory.OppositeOnMates c hQ) {m : ℕ} {u w₁ y x : V} (hu : u = hQ.tauE y) (hw : w₁ = hQ.tauE x) (b : u ⟶ w₁) (a : y ⟶ x) (q : Quiver.Path w₁ y) (hq : q.length = m) : ScalarMeshCategory.rowQ c hQ m (b.toPath.comp q) = ScalarMeshCategory.rowQ c hQ m (q.cons a)

theorem MultiplicativeBasisDeformations.OrientedTree.rowZ_rotate {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (hc : ScalarMeshCategory.OppositeOnMates c hQ) {m : ℕ} {Z Y₁ E E' : T.ZVert} (a₁ : Z ⟶ Y₁) (B : Quiver.Path Y₁ E) (a₂ : E ⟶ E') (hZ : π.obj Z = hQ.tauE (π.obj E)) (hY : π.obj Y₁ = hQ.tauE (π.obj E')) (hB : B.length = m) : T.rowZ hQ π c m (a₁.toPath.comp B) = T.rowZ hQ π c m (B.cons a₂)

Rotation of a lifted row: the first arrow moves to the end.

def MultiplicativeBasisDeformations.OrientedTree.raise {D : Type v} (T : OrientedTree D) (X : T.ZVert) {y : T.Dbl} (e : T.toDbl X.v ⟶ y) : T.ZVert

X raised by one along an arrow of Δ̄.

def MultiplicativeBasisDeformations.OrientedTree.zAct {D : Type v} (T : OrientedTree D) (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) : T.ZVert ⥤q T.ZVert

An automorphism of ℤΔ of height form (v, t) ↦ (σ v, t + s).

def MultiplicativeBasisDeformations.OrientedTree.dAct {D : Type v} (T : OrientedTree D) (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) : T.Dbl ⥤q T.Dbl

The corresponding automorphism of Δ̄.

theorem MultiplicativeBasisDeformations.OrientedTree.forget_zAct_mapPath {D : Type v} (T : OrientedTree D) (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) {X Y : T.ZVert} (P : Quiver.Path X Y) : T.forget.mapPath ((T.zAct σ hσ s hσp).mapPath P) = (T.dAct σ hσ).mapPath (T.forget.mapPath P)

theorem MultiplicativeBasisDeformations.OrientedTree.mapPath_zAct {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : T.ZVert ⥤q V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) {X Y : T.ZVert} (P : Quiver.Path X Y) : π.mapPath ((T.zAct σ hσ s hσp).mapPath P) = Quiver.Path.cast ⋯ ⋯ (π.mapPath P)

theorem MultiplicativeBasisDeformations.OrientedTree.rowZ_zAct {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) {m : ℕ} {X Y : T.ZVert} (P : Quiver.Path X Y) : T.rowZ hQ π c m ((T.zAct σ hσ s hσp).mapPath P) = T.rowZ hQ π c m P

Row classes are invariant under deck transformations.

theorem MultiplicativeBasisDeformations.OrientedTree.phiD_zAct {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype D] [DecidableEq D] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) {m : ℕ} (X : T.ZVert) {b : T.Dbl} (p : Quiver.Path (T.toDbl X.v) b) : T.phiD hQ π c m ((T.zAct σ hσ s hσp).obj X) ((T.dAct σ hσ).mapPath p) = T.phiD hQ π c m X p

theorem MultiplicativeBasisDeformations.OrientedTree.liftZ_comp_pathStar {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] (Y : T.ZVert) {b b' : T.Dbl} (p : Quiver.Path (T.toDbl Y.v) b) (q : Quiver.Path b b') : ⟨T.liftEnd Y (p.comp q), T.liftZ Y (p.comp q)⟩ = ⟨T.liftEnd (T.liftEnd Y p) q, (T.liftZ Y p).comp (T.liftZ (T.liftEnd Y p) q)⟩

theorem MultiplicativeBasisDeformations.OrientedTree.phiD_congr {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype D] [DecidableEq D] [DecidableRel T.orient] {m : ℕ} {X X' : T.ZVert} (h : X = X') {b : T.Dbl} (p : Quiver.Path (T.toDbl X.v) b) : T.phiD hQ π c m X p = T.phiD hQ π c m X' (Quiver.Path.cast ⋯ ⋯ p)

theorem MultiplicativeBasisDeformations.OrientedTree.phiD_rotate {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) {m : ℕ} (X : T.ZVert) {y : T.Dbl} (e : T.toDbl X.v ⟶ y) (q : Quiver.Path y ((T.dAct σ hσ).obj (T.toDbl X.v))) (hq : q.length = m) (hs : ↑m + 1 = 2 + s) : T.phiD hQ π c m X (e.toPath.comp q) = T.phiD hQ π c m (T.raise X e) (q.comp ((T.dAct σ hσ).map e).toPath)

Twisted rotation of one arrow (proof of Lemma A.2): for a row path e q from v to σ v of length 2 + s, cutting after the initial arrow e and correcting its mesh mate gives [e q] = [q σ(e)], the latter lifted from one level higher.

theorem MultiplicativeBasisDeformations.OrientedTree.phiD_rotate_path {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) {m : ℕ} (hs : ↑m + 1 = 2 + s) (X : T.ZVert) {z : T.Dbl} (U : Quiver.Path (T.toDbl X.v) z) (W : Quiver.Path z ((T.dAct σ hσ).obj (T.toDbl X.v))) : U.length + W.length = m + 1 → T.phiD hQ π c m X (U.comp W) = T.phiD hQ π c m (T.liftEnd X U) (W.comp ((T.dAct σ hσ).mapPath U))

Twisted rotation of an initial segment: [U W] = [W σ(U)].

theorem MultiplicativeBasisDeformations.OrientedTree.phiD_ztauInv {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) {m : ℕ} (hs : ↑m + 1 = 2 + s) (X : T.ZVert) (p : Quiver.Path (T.toDbl X.v) ((T.dAct σ hσ).obj (T.toDbl X.v))) (hp : p.length = m + 1) : T.phiD hQ π c m X p = T.phiD hQ π c m (T.ztauInv X) p

The row class is independent of the repetition coordinate (proof of Lemma A.2: "applying this rotation d times identifies the row with its translate by τ").

theorem MultiplicativeBasisDeformations.OrientedTree.phiD_height {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) {m : ℕ} (hs : ↑m + 1 = 2 + s) (X : T.ZVert) (p : Quiver.Path (T.toDbl X.v) ((T.dAct σ hσ).obj (T.toDbl X.v))) (hp : p.length = m + 1) (t' : ℤ) (ht' : ↑t' = T.par X.v) : T.phiD hQ π c m X p = T.phiD hQ π c m { v := X.v, t := t', ht := ht' } p