Cokernels spanned by given rows

In characteristic two the derivative cokernels need not vanish (prop:residual-correction-spaces, positive-deformations.tex): each periodic component contributes at most one line, spanned by a single row. We record "the cokernel classes of all rows of degree at least three lie in the span of the classes of the rows in S" (CokerSpan), and show that it is preserved by rescaling arrows and entire mesh relations (periodic-mesh-calculations.tex: "rescaling arrows and entire relations changes the mesh derivative by invertible diagonal maps, so it changes neither its cokernel …").

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.RowSet {V : Type v} [Quiver V] (Q : TranslationQuiver V) : Type (max v w)

A set of rows: paths τ x → x at nonprojective vertices.

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

The span of the classes of the rows of S of degree m + 1.

def MultiplicativeBasisDeformations.ScalarMeshCategory.CokerSpan {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) (S : RowSet Q) : Prop

The cokernels are spanned by the rows of S.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowClass_mem_rowSpan {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) {m : ℕ} {S : RowSet Q} {R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x} (hR : R ∈ S) (hl : R.snd.length = m + 1) : rowClass c m R.fst R.snd ∈ rowSpan c m S

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowSpan_mono {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) {m : ℕ} {S S' : RowSet Q} (h : S ⊆ S') : rowSpan c m S ≤ rowSpan c m S'

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowSpan_empty {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) (m : ℕ) : rowSpan c m ∅ = ⊥

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.cokerSpan_empty_iff {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) [Fintype ↑Q.nonprojective] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] : CokerSpan c ∅ ↔ ∀ (m : ℕ), 2 ≤ m → MeshDerivativeSurjective c m

Gauge invariance

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeFam {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) : MeshFamily c →ₗ[k] MeshFamily c'

The gauge on mesh families, g ↦ η Φ(g).

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeFam_imageD {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) (m : ℕ) : imageD c m ≤ Submodule.comap (gaugeFam c (fun {x y : V} => μ) η c' h) (imageD c' m)

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeCoker {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) (m : ℕ) : Coker c m →ₗ[k] Coker c' m

The induced map on cokernels.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeCoker_rowClass {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) (m : ℕ) (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x) : (gaugeCoker c (fun {x y : V} => μ) η c' h m) (rowClass c m x w) = (↑(η x) * ↑(pathWt (fun {x y : V} => μ) w)) • rowClass c' m x w

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowClass_mem_rowSpan_gauge {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) {m : ℕ} {S : RowSet Q} {x : ↑Q.nonprojective} {w : Quiver.Path ↑(Q.tau x) ↑x} (hx : rowClass c m x w ∈ rowSpan c m S) : rowClass c' m x w ∈ rowSpan c' m S

Spanning rows transfer along a gauge transformation.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.cokerSpan_gauge {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (c : MeshCoefficients k Q) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) {S : RowSet Q} (hS : CokerSpan c S) : CokerSpan c' S