Twisted traces on a star (Lemmas A.2 and A.4)

lem:twisted-trace-surjection, lem:arm-trace-reduction (periodic-mesh-calculations.tex). Let π : ℤΔ → Q be a covering of a star model with signed coefficients, and let (v, t) ↦ (σ v, t + s) be a deck transformation with σ fixing the centre. In degree d = m + 1 = 2 + s, the row class of a closed path at a σ-fixed vertex v (phiV) is independent of the height, kills the relations of Π(Δ), and satisfies twisted rotation.

noncomputable def MultiplicativeBasisDeformations.StarTrace.phiV {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (v : (starTree L).Dbl) (hv : σ v = v) (h : ℤ) (hh : ↑h = (starTree L).par v) (p : Quiver.Path v v) : ScalarMeshCategory.Coker c m

The row class of a closed path at a σ-fixed vertex, lifted at height h.

theorem MultiplicativeBasisDeformations.StarTrace.start_mem_vertices {W : Type u_1} [Quiver W] {a b : W} (U : Quiver.Path a b) : a ∈ U.vertices

theorem MultiplicativeBasisDeformations.StarTrace.dAct_mapPath_eq_cast {t : ℕ} {L : Fin t → ℕ} (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) {a b : (starTree L).Dbl} (U : Quiver.Path a b) (hU : ∀ x ∈ U.vertices, σ x = x) : ((starTree L).dAct σ hσ).mapPath U = Quiver.Path.cast ⋯ ⋯ U

theorem MultiplicativeBasisDeformations.StarTrace.length_cast {W : Type u_1} [Quiver W] {a b a' b' : W} (p : Quiver.Path a b) (ha : a = a') (hb : b = b') : (Quiver.Path.cast ha hb p).length = p.length

theorem MultiplicativeBasisDeformations.StarTrace.comp_cast_right {W : Type u_1} [Quiver W] {a b c c' : W} (p : Quiver.Path a b) (q : Quiver.Path b c) (h : c = c') : Quiver.Path.cast ⋯ h (p.comp q) = p.comp (Quiver.Path.cast ⋯ h q)

theorem MultiplicativeBasisDeformations.StarTrace.cast_comp_cast {W : Type u_1} [Quiver W] {a b b' c c' : W} (p : Quiver.Path a b) (q : Quiver.Path b c) (hb : b = b') (hc : c = c') : (Quiver.Path.cast ⋯ hb p).comp (Quiver.Path.cast hb hc q) = Quiver.Path.cast ⋯ hc (p.comp q)

theorem MultiplicativeBasisDeformations.StarTrace.phiV_height {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (hs : ↑m + 1 = 2 + s) (v : (starTree L).Dbl) (hv : σ v = v) (h h' : ℤ) (hh : ↑h = (starTree L).par v) (hh' : ↑h' = (starTree L).par v) (p : Quiver.Path v v) (hp : p.length = m + 1) : phiV hQ π c σ hσ m v hv h hh p = phiV hQ π c σ hσ m v hv h' hh' p

theorem MultiplicativeBasisDeformations.StarTrace.phiV_rotate {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (hs : ↑m + 1 = 2 + s) (v z : (starTree L).Dbl) (hv : σ v = v) (hz : σ z = z) (h : ℤ) (hh : ↑h = (starTree L).par v) (U : Quiver.Path v z) (W : Quiver.Path z v) (U' : Quiver.Path v z) (hU : ((starTree L).dAct σ hσ).mapPath U = Quiver.Path.cast ⋯ ⋯ U') (hlen : U.length + W.length = m + 1) : phiV hQ π c σ hσ m v hv h hh (U.comp W) = phiV hQ π c σ hσ m z hz (h + ↑U.length) ⋯ (W.comp U')

Twisted rotation in terms of phiV.

theorem MultiplicativeBasisDeformations.StarTrace.phiV_rotate_fixed {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (hs : ↑m + 1 = 2 + s) (v z : (starTree L).Dbl) (hv : σ v = v) (hz : σ z = z) (h : ℤ) (hh : ↑h = (starTree L).par v) (U : Quiver.Path v z) (W : Quiver.Path z v) (hU : ∀ x ∈ U.vertices, σ x = x) (hlen : U.length + W.length = m + 1) : phiV hQ π c σ hσ m v hv h hh (U.comp W) = phiV hQ π c σ hσ m z hz (h + ↑U.length) ⋯ (W.comp U)

Rotation of an initial segment whose vertices are fixed by σ.

noncomputable def MultiplicativeBasisDeformations.StarTrace.phiVL {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (v : (starTree L).Dbl) (hv : σ v = v) (h : ℤ) (hh : ↑h = (starTree L).par v) : (LinearPaths.obj v ⟶ LinearPaths.obj v) →ₗ[k] ScalarMeshCategory.Coker c m

The linear extension of phiV.

theorem MultiplicativeBasisDeformations.StarTrace.phiVL_eq {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (v : (starTree L).Dbl) (hv : σ v = v) (h : ℤ) (hh : ↑h = (starTree L).par v) (f : LinearPaths.obj v ⟶ LinearPaths.obj v) : (phiVL hQ π c σ hσ m v hv h hh) f = ((starTree L).phiL hQ π c m { v := v, t := h, ht := hh } (((starTree L).dAct σ hσ).obj ((starTree L).toDbl v))) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))

theorem MultiplicativeBasisDeformations.StarTrace.phiVL_eq_zero_of_mem {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsig : (starTree L).pullCoeff hQ π c = (starTree L).zSigned k) (v : (starTree L).Dbl) (hv : σ v = v) (h : ℤ) (hh : ↑h = (starTree L).par v) {f : LinearPaths.obj v ⟶ LinearPaths.obj v} (hf : f ∈ ((starTree L).preproj k).ideal (LinearPaths.obj v) (LinearPaths.obj v)) : (phiVL hQ π c σ hσ m v hv h hh) f = 0

Traces of words at the centre

theorem MultiplicativeBasisDeformations.StarTrace.vertices_wordP {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (w : List (Fin t)) : (StarCorner.wordP (i :: w)).vertices = [StarCorner.o L, StarCorner.av L i 0 ⋯] ++ (StarCorner.wordP w).vertices

theorem MultiplicativeBasisDeformations.StarTrace.map_vertices_wordP {t : ℕ} {L : Fin t → ℕ} (σ : StarV L ≃ StarV L) (hσo : σ none = none) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), σ (StarCorner.av L i j hj) = StarCorner.av L (θ i) j ⋯) (w : List (Fin t)) : List.map (⇑σ) (StarCorner.wordP w).vertices = (StarCorner.wordP (List.map (⇑θ) w)).vertices

theorem MultiplicativeBasisDeformations.StarTrace.dAct_wordP {t : ℕ} {L : Fin t → ℕ} (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (hσo : σ none = none) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), σ (StarCorner.av L i j hj) = StarCorner.av L (θ i) j ⋯) (w : List (Fin t)) : ((starTree L).dAct σ hσ).mapPath (StarCorner.wordP w) = Quiver.Path.cast ⋯ ⋯ (StarCorner.wordP (List.map (⇑θ) w))

theorem MultiplicativeBasisDeformations.StarTrace.par_o {t : ℕ} {L : Fin t → ℕ} : ↑0 = (starTree L).par (StarCorner.o L)

noncomputable def MultiplicativeBasisDeformations.StarTrace.wordTr {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (hσo : σ none = none) (w : List (Fin t)) : ScalarMeshCategory.Coker c m

The trace of a word w in the x_i: the row class of the closed path at the centre, in path degree 2 |w| = m + 1, and zero in other degrees.

theorem MultiplicativeBasisDeformations.StarTrace.wordTr_rotate {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (hs : ↑m + 1 = 2 + s) (hσo : σ none = none) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), σ (StarCorner.av L i j hj) = StarCorner.av L (θ i) j ⋯) (u v : List (Fin t)) : wordTr hQ π c σ hσ m hσo (u ++ v) = wordTr hQ π c σ hσ m hσo (v ++ List.map (⇑θ) u)

Twisted rotation of words: [u v] = [v θ(u)].

theorem MultiplicativeBasisDeformations.StarTrace.phiVL_path {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (v : (starTree L).Dbl) (hv : σ v = v) (h : ℤ) (hh : ↑h = (starTree L).par v) (p : Quiver.Path v v) : (phiVL hQ π c σ hσ m v hv h hh) (LinearPaths.path p) = phiV hQ π c σ hσ m v hv h hh p

theorem MultiplicativeBasisDeformations.StarTrace.wordTr_centre {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsig : (starTree L).pullCoeff hQ π c = (starTree L).zSigned k) (hσo : σ none = none) (u v : List (Fin t)) : ∑ i : Fin t, wordTr hQ π c σ hσ m hσo (u ++ i :: v) = 0

The centre relation ∑ x_i = 0 in traces.

theorem MultiplicativeBasisDeformations.StarTrace.wordTr_arm {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsig : (starTree L).pullCoeff hQ π c = (starTree L).zSigned k) (hσo : σ none = none) (u v : List (Fin t)) (i : Fin t) : wordTr hQ π c σ hσ m hσo (u ++ List.replicate (L i + 2) i ++ v) = 0

The arm relation x_i^{L_i+1} = 0 in traces.

Arms fixed by the twist (Lemma A.4, second part)

theorem MultiplicativeBasisDeformations.StarTrace.av_congr {t : ℕ} {L : Fin t → ℕ} {i i' : Fin t} (e : i' = i) (j : ℕ) (h : j ≤ L i') (h' : j ≤ L i) : StarCorner.av L i' j h = StarCorner.av L i j h'

theorem MultiplicativeBasisDeformations.StarTrace.fix_av {t : ℕ} {L : Fin t → ℕ} (σ : StarV L ≃ StarV L) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), σ (StarCorner.av L i j hj) = StarCorner.av L (θ i) j ⋯) {i : Fin t} (hi : θ i = i) (j : ℕ) (hj : j ≤ L i) : σ (StarCorner.av L i j hj) = StarCorner.av L i j hj

theorem MultiplicativeBasisDeformations.StarTrace.phiV_congr {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsig : (starTree L).pullCoeff hQ π c = (starTree L).zSigned k) (v : (starTree L).Dbl) (hv : σ v = v) (h : ℤ) (hh : ↑h = (starTree L).par v) {p p' : Quiver.Path v v} (hp : LinearPaths.path p - LinearPaths.path p' ∈ ((starTree L).preproj k).ideal (LinearPaths.obj v) (LinearPaths.obj v)) : phiV hQ π c σ hσ m v hv h hh p = phiV hQ π c σ hσ m v hv h hh p'

Closed paths with the same class modulo the relations have the same row class.

theorem MultiplicativeBasisDeformations.StarTrace.phiV_mem {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsig : (starTree L).pullCoeff hQ π c = (starTree L).zSigned k) (v : (starTree L).Dbl) (hv : σ v = v) (h : ℤ) (hh : ↑h = (starTree L).par v) {p : Quiver.Path v v} (hp : LinearPaths.path p ∈ ((starTree L).preproj k).ideal (LinearPaths.obj v) (LinearPaths.obj v)) : phiV hQ π c σ hσ m v hv h hh p = 0

theorem MultiplicativeBasisDeformations.StarTrace.cpow_zb_succ_eq {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (r : ℕ) (h : r + 1 ≤ L i) (q : ℕ) : ((StarCorner.cpow (StarCorner.zb i (r + 1) h) q).comp (StarCorner.inS i r h).toPath).comp (StarCorner.outS i r h).toPath = StarCorner.cpow (StarCorner.zb i (r + 1) h) (q + 1)

theorem MultiplicativeBasisDeformations.StarTrace.cpow_zb_zero_succ_eq {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (q : ℕ) : ((StarCorner.cpow (StarCorner.zb i 0 ⋯) q).comp (StarCorner.in0 i).toPath).comp (StarCorner.out0 i).toPath = StarCorner.cpow (StarCorner.zb i 0 ⋯) (q + 1)

theorem MultiplicativeBasisDeformations.StarTrace.phiV_yb_zero {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsig : (starTree L).pullCoeff hQ π c = (starTree L).zSigned k) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (hs : ↑m + 1 = 2 + s) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), σ (StarCorner.av L i j hj) = StarCorner.av L (θ i) j ⋯) {i : Fin t} (hi : θ i = i) (n r : ℕ) (hr : r + 1 ≤ L i) : L i - r = n → ∀ (h : ℤ) (hh : ↑h = (starTree L).par (StarCorner.av L i r ⋯)) (q : ℕ), 1 ≤ q → 2 * q = m + 1 → phiV hQ π c σ hσ m (StarCorner.av L i r ⋯) ⋯ h hh (StarCorner.cpow (StarCorner.yb i r hr) q) = 0

Outward backtracks on a fixed arm have zero trace: rotating the first arrow turns y_r^q into z_{r+1}^q, which the mesh at r + 1 identifies with y_{r+1}^q, or kills at the leaf.

theorem MultiplicativeBasisDeformations.StarTrace.wordTr_replicate {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).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] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsig : (starTree L).pullCoeff hQ π c = (starTree L).zSigned k) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (hs : ↑m + 1 = 2 + s) (hσo : σ none = none) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), σ (StarCorner.av L i j hj) = StarCorner.av L (θ i) j ⋯) {i : Fin t} (hi : θ i = i) (q : ℕ) (hq : 1 ≤ q) : wordTr hQ π c σ hσ m hσo (List.replicate q i) = 0

[x_i^q] = 0 on an arm fixed by the twist (eq:arm-power-trace-zero).