Proposition 6.1: residual correction spaces (spanning form)

prop:residual-correction-spaces (positive-deformations.tex) and Appendix B: in characteristic two, under the brick hypothesis, "each periodic component contributes at most one correction line, represented by a single path". We record: there is a set S of rows at periodic vertices, at most one in each periodic component, whose classes span all derivative cokernels in degrees at least three (residual_cokerSpan).

Deviation from the source: the source takes I to be exactly the components with a nonzero class; we keep all components with a candidate row (a superset), which is what the spanning statement needs. The component models and degrees of the rows are recorded by connected_cokerSpan and the files StarDSpan, StarESpan.

theorem MultiplicativeBasisDeformations.TranslationQuiver.component_eq_of_mem {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x y : V} (hy : y ∈ Q.component x) : Q.component y = Q.component x

noncomputable def MultiplicativeBasisDeformations.repr {V : Type v} [Quiver V] [Fintype V] {Q : TranslationQuiver V} (T : Set V) (d : V) : V

A canonical vertex of a set of vertices.

theorem MultiplicativeBasisDeformations.repr_congr {V : Type v} [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] {T T' : Set V} (h : T = T') (hT : ∃ y ∈ Q.periodic, y ∈ T) (d d' : V) : repr T d = repr T' d'

theorem MultiplicativeBasisDeformations.repr_mem {V : Type v} [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] {x : V} (hx : x ∈ Q.periodic) : repr (Q.component x) x ∈ Q.component x

theorem MultiplicativeBasisDeformations.repr_component {V : Type v} [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] {x : V} (hx : x ∈ Q.periodic) : Q.component (repr (Q.component x) x) = Q.component x

theorem MultiplicativeBasisDeformations.residual_cokerSpan_model {k : Type u} [Field k] {V : Type v} [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 ∧ ScalarMeshCategory.TwoRows Q S ∧ ∀ R ∈ S, ∃ x ∈ Q.periodic, ↑R.fst ∈ Q.component x ∧ ∃ (R₀ : (y : ↑(TranslationQuiver.restrict ⋯).nonprojective) × Quiver.Path ↑((TranslationQuiver.restrict ⋯).tau y) ↑y), StarTrace.DEModel ⋯ R₀ ∧ R₀.snd.length = R.snd.length

Proposition 6.1, spanning form with the model data: as residual_cokerSpan, and each spanning row comes from a row of its periodic component of type D or E and degree 2s + 2 (StarTrace.DEModel).

theorem MultiplicativeBasisDeformations.residual_cokerSpan {k : Type u} [Field k] {V : Type v} [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 ∧ ScalarMeshCategory.TwoRows Q S

Proposition 6.1, spanning form (prop:residual-correction-spaces). In characteristic two, for a finite-dimensional scalar mesh category on a finite translation quiver with at most one arrow between ordered vertices, satisfying the brick hypothesis, there is a set of rows at periodic vertices, at most one in each periodic component, whose classes span the cokernels of all D_m, m ≥ 2.