Rows and columns of the mesh derivative

Subsection 5.1 of the manuscript (mesh-deformations.tex).

For a scalar mesh category C = C(Q, c) the derivative D_m of eq:mesh-derivative is linear. Its target V_{m+1} is spanned by the rows (x, w): a nonprojective vertex x and a path w : τ x → x of length m + 1, placed in the x-th component. A correction column is an arrow b together with a parallel path p; by eq:mesh-derivative its image has at most two entries (column_eq). This file sets up these objects:

• meshDerivativeₗ, the derivative as a linear map;
• imageD c m, the image of the degree-m families;
• row c x w, the row of a path, and surjective_iff_rows: D_m is surjective exactly when every row of length m + 1 lies in the image;
• column_eq, the two entries of a correction column.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.pathMor {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} (p : Quiver.Path x y) : obj c x ⟶ obj c y

The image of a path in the scalar mesh category.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.pathMor_comp {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 z : V} (p : Quiver.Path x y) (q : Quiver.Path y z) : pathMor c (p.comp q) = CategoryTheory.CategoryStruct.comp (pathMor c p) (pathMor c q)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.pathMor_toPath {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} (a : x ⟶ y) : pathMor c a.toPath = arrowMor c a

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.pathMor_cons {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 z : V} (p : Quiver.Path x y) (a : y ⟶ z) : pathMor c (p.cons a) = CategoryTheory.CategoryStruct.comp (pathMor c p) (arrowMor c a)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.pathMor_mem_degreePart {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} (p : Quiver.Path x y) : pathMor c p ∈ degreePart c p.length x y

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.degreePart_eq_span {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (n : ℕ) (x y : V) : degreePart c n x y = Submodule.span k {f : obj c x ⟶ obj c y | ∃ (p : Quiver.Path x y), p.length = n ∧ f = pathMor c p}

The degree-n part is spanned by the images of the paths of length n.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.meshDerivativeₗ {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) : ArrowFamily c →ₗ[k] MeshFamily c

The mesh derivative is linear.

@[simp]

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.meshDerivativeₗ_apply {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (f : ArrowFamily c) : (meshDerivativeₗ c) f = meshDerivative c f

def MultiplicativeBasisDeformations.ScalarMeshCategory.familiesDeg {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (m : ℕ) : Submodule k (ArrowFamily c)

The families of path degree m.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.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) (m : ℕ) : Submodule k (MeshFamily c)

The image of D_m.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.row {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x) : MeshFamily c

The row of a path w : τ x → x: the family with w at x and zero elsewhere.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.surjective_iff_rows {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [Fintype ↑Q.nonprojective] (m : ℕ) : MeshDerivativeSurjective c m ↔ ∀ (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x), w.length = m + 1 → row c x w ∈ imageD c m

D_m is surjective exactly when every row of length m + 1 lies in its image.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.meshDerivative_apply_eq {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (f : ArrowFamily c) (x : ↑Q.nonprojective) : meshDerivative c f x = ∑ b : (y : V) × (y ⟶ ↑x), ↑(c x b.fst b.snd) • CategoryTheory.CategoryStruct.comp (f ⟨↑(Q.tau x), ⟨b.fst, (Q.mate x b.fst) b.snd⟩⟩) (arrowMor c b.snd) + ∑ b : (y : V) × (y ⟶ ↑x), ↑(c x b.fst b.snd) • CategoryTheory.CategoryStruct.comp (arrowMor c ((Q.mate x b.fst) b.snd)) (f ⟨b.fst, ⟨↑x, b.snd⟩⟩)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.sigma3_eq_iff {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {u v u' v' : V} (a : u ⟶ v) (a' : u' ⟶ v') : ⟨u, ⟨v, a⟩⟩ = ⟨u', ⟨v', a'⟩⟩ ↔ u = u' ∧ v = v' ∧ a ≍ a'

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.column_eq {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (x : ↑Q.nonprojective) {y : V} (a : y ⟶ ↑x) (p : Quiver.Path (↑(Q.tau x)) y) : meshDerivative c (Pi.single ⟨↑(Q.tau x), ⟨y, (Q.mate x y) a⟩⟩ (pathMor c p)) = ↑(c x y a) • row c x (p.cons a) + if hy : y ∈ Q.nonprojective then ↑(c ⟨y, hy⟩ (↑(Q.tau x)) ((Q.mate x y) a)) • row c ⟨y, hy⟩ (((Q.mate ⟨y, hy⟩ ↑(Q.tau x)) ((Q.mate x y) a)).toPath.comp p) else 0

A correction column has at most two entries (proof of prop:periodic-localization). Correcting the arrow σ a : τ x → y (for a : y → x) by a parallel path p contributes c_{x,a} p a to the mesh at x and, if y is nonprojective, c_{y,σ a} (σ σ a) p to the mesh at y.