Proposition 6.1 with dual mesh weights (for Proposition 7.5)

residual_dual: in characteristic two, under the hypotheses of Proposition 6.1, there is a set S of spanning rows, at most one in each periodic component, together with integer mesh weights W_R (R ∈ S) such that the weight of the row R' minus ν of its vertex is 1 if R' = R and 0 otherwise. This is the input of Proposition 7.5: by Lemma 7.4 these give integer ray weights dual to the residual characters.

theorem MultiplicativeBasisDeformations.residual_dual {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] (c : MeshCoefficients k Q) (hQ : HasAtMostOneArrow V) (hchar : 2 = 0) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (hbrick : ScalarMeshCategory.BrickHypothesis c) : ∃ (S : ScalarMeshCategory.RowSet Q), (∀ R ∈ S, ↑R.fst ∈ Q.periodic) ∧ (∀ R ∈ S, ∀ R' ∈ S, ↑R'.fst ∈ Q.component ↑R.fst → R = R') ∧ ScalarMeshCategory.CokerSpan c S ∧ ∀ R ∈ S, ∃ (W : MeshWalk.MeshWt Q ℤ), ∀ R' ∈ S, W.pw R'.snd - W.ν R'.fst = if R' = R then 1 else 0

Proposition 6.1 with dual mesh weights.