The spanning row of a connected periodic quiver winds once #
Strengthening of connected_cokerSpan for Proposition 7.5: the spanning row (if any) of
a finite connected stable translation quiver in characteristic two has a winding mesh
weight in which the weight of the row minus ν of its vertex is one
(connected_cokerSpan_wt; the weight is floorWt).
theorem
MultiplicativeBasisDeformations.StarTrace.connected_cokerSpan_wt
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
(hQ : Q.IsStable)
[DecidablePred fun (x : V) => x ∈ Q.nonprojective]
[Fintype ↑Q.nonprojective]
{k : Type u}
[Field k]
(c : MeshCoefficients k Q)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
(hchar : 2 = 0)
(hbrick : ScalarMeshCategory.BrickHypothesis c)
(x₀ : V)
(hconn : ∀ (v : V), Relation.EqvGen (TranslationQuiver.SecPath.ConnAdj hQ) x₀ v)
:
∃ (S : ScalarMeshCategory.RowSet Q),
Set.Subsingleton S ∧ ScalarMeshCategory.CokerSpan c S ∧ ∀ R ∈ S, ∃ (W : MeshWalk.MeshWt Q ℤ), W.pw R.snd - W.ν R.fst = 1
The spanning row winds once.