Mesh corrections on a connected periodic quiver in characteristic two

characteristic-two-mesh-calculations.tex: "We will show that each periodic component contributes at most one correction line, represented by a single path." On a finite connected stable translation quiver with a finite-dimensional scalar mesh category satisfying the brick hypothesis, in characteristic two, the cokernels of the mesh derivatives are spanned by the class of at most one row (connected_cokerSpan): by Proposition 4.1 the quiver is covered by a star model; the types A give zero cokernels, and the types D, E one row of degree 2s + 2 at the centre.

def MultiplicativeBasisDeformations.StarTrace.DEModel {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : Prop

The model of a row of type D or E (Proposition 6.1(1)(2)): the quiver is ℤΔ/⟨g⟩ for a three-arm Dynkin star Δ, with g(v, j) = (ρ v, j + 2s) (that is, τ^{−s} ρ), ρ an automorphism of Δ fixing the centre, s ≥ 1, and the row has degree 2s + 2.

theorem MultiplicativeBasisDeformations.StarTrace.deModel_candRow {V : Type v'} [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] (L : Fin 3 → ℕ) (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsurj : Function.Surjective π.obj) (hsum : ∑ i : Fin 3, (↑(L i) + 1) / (↑(L i) + 2) < 2) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (h0 : ρ none = none) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) (W₀ : List (Fin 3)) (hW₀ : W₀.length = c0 / 2 + 1) (R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : R ∈ candRow hQ π W₀ → DEModel hQ R

The model data of a candidate row of a three-arm star.

theorem MultiplicativeBasisDeformations.StarTrace.connected_cokerSpan_model {V : Type v'} [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 ∧ ScalarMeshCategory.TwoRows Q S ∧ ∀ R ∈ S, DEModel hQ R

Mesh corrections on a connected periodic quiver in characteristic two, with the model data of Proposition 6.1(1)(2): the cokernels are spanned by the class of at most one row, of type D or E and degree 2s + 2.

theorem MultiplicativeBasisDeformations.StarTrace.connected_cokerSpan {V : Type v'} [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 ∧ ScalarMeshCategory.TwoRows Q S

Mesh corrections on a connected periodic quiver in characteristic two: the cokernels are spanned by the class of at most one row.