Proposition 6.1: residual correction spaces

positive-deformations.tex (prop:residual-correction-spaces). In characteristic two, under the brick hypothesis, call a periodic component residual if ⊕_m coker D_m(C) has a nonzero class supported on it. Then each residual component is ℤΔ/⟨τ^{s_i}ρ⟩ with Δ of type D or E, there is a path p_i : τ v_i → v_i of degree d_i = 2s_i + 2, and ⊕_{m≥2} coker D_m(C) = ⊕_{i∈I} k[p_i].

The spanning by at most one row per periodic component is residual_cokerSpan. Here:

• the mesh derivative commutes with the projection to a union of components of a quiver (D_projA), so the image of D is stable under it (projM_mem_imageD);
• after the localization of Proposition 5.1 to the periodic vertices (where periodic components are unions of connected components), a family supported on one periodic component lies in the image of D as soon as it does modulo families supported elsewhere (mem_imageD_of_supported);
• hence rows in distinct periodic components with nonzero classes are linearly independent (rows_independent).

Projection to a union of components

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.projA {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (P : V → Prop) [DecidablePred P] (f : ArrowFamily c) : ArrowFamily c

The arrow family kept on the arrows with target in P.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.projM {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (P : V → Prop) [DecidablePred P] (g : MeshFamily c) : MeshFamily c

The mesh family kept on the vertices in P.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.D_projA {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {P : V → Prop} [DecidablePred P] (hP : ∀ (x y : V) (x_1 : x ⟶ y), P x ↔ P y) (f : ArrowFamily c) : meshDerivative c (projA c P f) = projM c P (meshDerivative c f)

The mesh derivative commutes with the projection to a union of components.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.projM_mem_imageD {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {P : V → Prop} [DecidablePred P] (hP : ∀ (x y : V) (x_1 : x ⟶ y), P x ↔ P y) {m : ℕ} {g : MeshFamily c} (hg : g ∈ imageD c m) : projM c P g ∈ imageD c m

Families supported on one periodic component

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.mem_component_iff {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {r x : V} (hx : x ∈ Q.periodic) : x ∈ Q.component r ↔ Q.component x = Q.component r

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.component_eq' {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {u v : V} (h : Relation.EqvGen Q.PeriodicAdj u v) : Q.component u = Q.component v

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.comp_iff_of_arrow {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] (r : V) (a b : FullSub Q.periodic) (e : a ⟶ b) : a.val ∈ Q.component r ↔ b.val ∈ Q.component r

Membership in a periodic component is preserved along arrows between periodic vertices.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.mem_imageD_of_supported {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {m : ℕ} (r : V) {g h : MeshFamily c} (hg : g ∈ famDeg c (m + 1)) (hgs : ∀ (x : ↑Q.nonprojective), ↑x ∉ Q.component r → g x = 0) (hhs : ∀ (x : ↑Q.nonprojective), ↑x ∈ Q.component r → h x = 0) (hgh : g + h ∈ imageD c m) : g ∈ imageD c m

A family supported on one periodic component lies in the image of D_m as soon as it does modulo a family supported off that component.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.row_mem_famDeg {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {m : ℕ} (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x) (hw : w.length = m + 1) (t : k) : t • row c x w ∈ famDeg c (m + 1)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rows_independent {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {m : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : ι → ↑Q.nonprojective) (w : (i : ι) → Quiver.Path ↑(Q.tau (x i)) ↑(x i)) (hw : ∀ (i : ι), (w i).length = m + 1) (hper : ∀ (i : ι), ↑(x i) ∈ Q.periodic) (hcomp : ∀ (i j : ι), ↑(x j) ∈ Q.component ↑(x i) → i = j) (hne : ∀ (i : ι), row c (x i) (w i) ∉ imageD c m) (l : ι → k) (h : ∑ i : ι, l i • row c (x i) (w i) ∈ imageD c m) (i : ι) : l i = 0

Rows in distinct periodic components with nonzero classes are linearly independent.

Rows and the cokernel

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.famDeg_le_rows {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] (m : ℕ) : famDeg c (m + 1) ≤ Submodule.span k {f : MeshFamily c | ∃ (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x), w.length = m + 1 ∧ f = row c x w}

The families of degree m + 1 are spanned by the rows.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.rowSpanF {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (m : ℕ) (S : RowSet Q) : Submodule k (MeshFamily c)

The span of the rows of S of degree m + 1, in the families.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowSpan_eq_map {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] (m : ℕ) (S : RowSet Q) : rowSpan c m S = Submodule.map (imageD c m).mkQ (rowSpanF c m S)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.exists_rowSpanF {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {S : RowSet Q} (hS : CokerSpan c S) {m : ℕ} (hm : 2 ≤ m) {g : MeshFamily c} (hg : g ∈ famDeg c (m + 1)) : ∃ n ∈ rowSpanF c m S, g - n ∈ imageD c m

A family of degree m + 1 is a combination of the rows of a spanning set, modulo the image of D_m.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowSpanF_supported {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {m : ℕ} {S : RowSet Q} {r : V} (hS : ∀ R ∈ S, ↑R.fst ∉ Q.component r) {n : MeshFamily c} (hn : n ∈ rowSpanF c m S) (x : ↑Q.nonprojective) : ↑x ∈ Q.component r → n x = 0

def MultiplicativeBasisDeformations.ScalarMeshCategory.Residual {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (r : V) : Prop

A periodic component is residual if ⊕_{m≥2} coker D_m(C) has a nonzero class supported on it.

Proposition 6.1

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.residualCorrectionSpaces {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] [(x y : V) → Fintype (x ⟶ y)] (hQ : HasAtMostOneArrow V) (hchar : 2 = 0) (hfin : ∀ (x y : V), FiniteDimensional k (obj c x ⟶ obj c y)) (hbrick : BrickHypothesis c) : ∃ (S : RowSet Q), (∀ R ∈ S, ↑R.fst ∈ Q.periodic) ∧ (∀ R ∈ S, ∀ R' ∈ S, ↑R'.fst ∈ Q.component ↑R.fst → R = R') ∧ CokerSpan c S ∧ (∀ R ∈ S, row c R.fst R.snd ∉ imageD c (R.snd.length - 1)) ∧ (∀ (m : ℕ) (F : Finset ((x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)), ↑F ⊆ S → (∀ R ∈ F, R.snd.length = m + 1) → ∀ (l : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x → k), ∑ R ∈ F, l R • row c R.fst R.snd ∈ imageD c m → ∀ R ∈ F, l R = 0) ∧ (∀ r ∈ Q.periodic, Residual c r ↔ ∃ R ∈ S, ↑R.fst ∈ Q.component r) ∧ (∀ 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) ∧ TwoRows Q S

Proposition 6.1 (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 S of rows p_i at periodic vertices, at most one in each periodic component, such that:

• the classes [p_i] span ⊕_{m≥2} coker D_m(C), are nonzero, and are linearly independent (so ⊕_{m≥2} coker D_m(C) = ⊕_i k[p_i]);
• a periodic component is residual exactly when it carries a row of S (so S is indexed by the residual components I);
• the component of each p_i is ℤΔ/⟨τ^{s_i}ρ⟩ with Δ of type D or E, ρ fixing the centre, and p_i has degree d_i = 2s_i + 2 (StarTrace.DEModel; in particular d_i is the only degree of a nonzero class on the component);
• the rows are killed by two over every coefficient ring (used for Lemma B.2).