Every row class is a word trace (Lemmas A.2 and A.4) #
lem:twisted-trace-surjection (surjectivity) and lem:arm-trace-reduction
(first part), periodic-mesh-calculations.tex: "Lift a row path from
τ(x, j). … The map from twisted paths to row classes is well defined and
surjective." and "If a path from v to θ v meets the centre o, cut it there.
Twisted rotation gives a path from o to θ o = o, and Lemma A.3 expresses it
in the x_i. A path avoiding o stays on one arm. That arm is fixed pointwise
by θ … the process ends in zero."
theorem
MultiplicativeBasisDeformations.Quiver.Path.vertices_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).vertices = p.vertices
theorem
MultiplicativeBasisDeformations.Quiver.Path.mem_of_mem_left
{W : Type u_1}
[Quiver W]
{a b x y : W}
(U : Quiver.Path a x)
(V' : Quiver.Path x b)
(hy : y ∈ U.vertices)
:
y ∈ (U.comp V').vertices
theorem
MultiplicativeBasisDeformations.Quiver.Path.mem_of_mem_right
{W : Type u_1}
[Quiver W]
{a b x y : W}
(U : Quiver.Path a x)
(V' : Quiver.Path x b)
(hy : y ∈ V'.vertices)
:
y ∈ (U.comp V').vertices
theorem
MultiplicativeBasisDeformations.Quiver.Path.mem_rotate
{W : Type u_1}
[Quiver W]
{a x y : W}
(U : Quiver.Path a x)
(V' : Quiver.Path x a)
(hy : y ∈ (V'.comp U).vertices)
:
y ∈ (U.comp V').vertices
theorem
MultiplicativeBasisDeformations.OrientedTree.t_path
{D : Type u_1}
(T : OrientedTree D)
{X E : T.ZVert}
(P : Quiver.Path X E)
:
theorem
MultiplicativeBasisDeformations.StarTrace.av_eq_of
{t : ℕ}
{L : Fin t → ℕ}
{i : Fin t}
{j j' : ℕ}
(e : j = j')
(h : j ≤ L i)
(h' : j' ≤ L i)
:
StarCorner.av L i j h = StarCorner.av L i j' h'
theorem
MultiplicativeBasisDeformations.StarTrace.arm_of_avoid
{t : ℕ}
{L : Fin t → ℕ}
(i : Fin t)
(j : ℕ)
(hj : j ≤ L i)
{b : (starTree L).Dbl}
(p : Quiver.Path (StarCorner.av L i j hj) b)
(hp : StarCorner.o L ∉ p.vertices)
(y : (starTree L).Dbl)
:
y ∈ p.vertices → ∃ (j' : ℕ) (h' : j' ≤ L i), y = StarCorner.av L i j' h'
A path avoiding the centre stays on its arm.
theorem
MultiplicativeBasisDeformations.StarTrace.length_eq_zero_of_const
{t : ℕ}
{L : Fin t → ℕ}
{a b : (starTree L).Dbl}
(p : Quiver.Path a b)
(hp : ∀ y ∈ p.vertices, y = a)
:
p.length = 0
A path all of whose vertices coincide is trivial (the star has no loops).
theorem
MultiplicativeBasisDeformations.StarTrace.phiD_mem_span
{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 ⋯)
(v : (starTree L).Dbl)
(h : ℤ)
(hh : ↑h = (starTree L).par v)
(p : Quiver.Path ((starTree L).toDbl v) (((starTree L).dAct σ hσ).obj ((starTree L).toDbl v)))
(hp : p.length = m + 1)
:
Lemma A.4, first part: the lifted row class of a path from v to σ v
is a word trace at the centre, or zero.
theorem
MultiplicativeBasisDeformations.StarTrace.rowClass_mem_span
{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 ⋯)
(hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x)
(hfib : ∀ (X E : (starTree L).ZVert), π.obj E = π.obj X → E.t = X.t + s → E = ((starTree L).zAct σ hσ s hσp).obj X)
(x : ↑Q.nonprojective)
(w : Quiver.Path ↑(Q.tau x) ↑x)
(hw : w.length = m + 1)
:
ScalarMeshCategory.rowClass c m x w ∈ Submodule.span k (Set.range (wordTr hQ π c σ hσ m hσo))
Lemma A.2, surjectivity: every row class of degree m + 1 = 2 + s is a
combination of word traces at the centre.