Multiplicative bases

MultiplicativeBasisDeformations.Foundations.ConnectedWt

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.