Weight gradings of the mesh derivative cokernels

weights-and-parameters.tex: "a mesh weight w grades V_{m+1}(C) by giving a path at row v the weight w(path) − ν_v, and grades U_m(C) by giving a path parallel to an arrow a the weight w(path) − w(a). The map D_m preserves these gradings, because each term (σa)a of the mesh at v has weight ν_v. Hence coker D_m is graded by L, and the line k[p_i] has degree χ_i."

Over any commutative coefficient ring: for an integer mesh weight W (IntWt), the weight projections of families (projW, projWA) commute with D_m (D_projWA), so the image of D_m is graded (projW_mem_imageD), and a row is homogeneous of degree W(p) − ν_v (projW_row). This gives the labels χ_i of Lemma B.2 (integralMeshCokernels_graded).

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

An integer mesh weight: arrow weights w and row weights ν with w(σa) + w(a) = ν_v.

• w {y x : V} : (y ⟶ x) → ℤ
• ν : ↑Q.nonprojective → ℤ
• mesh (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) : self.w ((Q.mate x a.fst) a.snd) + self.w a.snd = self.ν x

@[irreducible]

def MultiplicativeBasisDeformations.ScalarMeshCategory.IntWt.pw {V : Type v} [Quiver V] {Q : TranslationQuiver V} (W : IntWt Q) {y x : V} : Quiver.Path y x → ℤ

The weight of a path.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.IntWt.pw_comp {V : Type v} [Quiver V] {Q : TranslationQuiver V} (W : IntWt Q) {x y z : V} (p : Quiver.Path x y) (q : Quiver.Path y z) : W.pw (p.comp q) = W.pw p + W.pw q

def MultiplicativeBasisDeformations.ScalarMeshCategory.IntWt.pathWeight {V : Type v} [Quiver V] {Q : TranslationQuiver V} (W : IntWt Q) : PathWeight V (Multiplicative ℤ)

The path weight of W, multiplicatively.

@[simp]

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.IntWt.pathWeight_deg {V : Type v} [Quiver V] {Q : TranslationQuiver V} (W : IntWt Q) {x y : V} (p : Quiver.Path x y) : W.pathWeight.deg p = Multiplicative.ofAdd (W.pw p)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.IntWt.pw_toPath {V : Type v} [Quiver V] {Q : TranslationQuiver V} (W : IntWt Q) {y x : V} (a : y ⟶ x) : W.pw a.toPath = W.w a

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.IntWt.homog {V : Type v} [Quiver V] {Q : TranslationQuiver V} (W : IntWt Q) [(x : V) → Fintype ((y : V) × (y ⟶ x))] : MeshHomogeneous W.pathWeight

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.wP {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) (g : ℤ) (x y : V) : (obj c x ⟶ obj c y) →ₗ[k] obj c x ⟶ obj c y

The weight projection on Hom spaces.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.arrowMor_mem_wPart {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) {y x : V} (a : y ⟶ x) : arrowMor c a ∈ wPart c W.pathWeight (Multiplicative.ofAdd (W.w a)) y x

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.wP_comp_hom {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) {x y z : V} (φ : obj c x ⟶ obj c y) {α : obj c y ⟶ obj c z} {h : ℤ} (hα : α ∈ wPart c W.pathWeight (Multiplicative.ofAdd h) y z) (g : ℤ) : (wP c W g x z) (CategoryTheory.CategoryStruct.comp φ α) = CategoryTheory.CategoryStruct.comp ((wP c W (g - h) x y) φ) α

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.wP_hom_comp {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) {x y z : V} {α : obj c x ⟶ obj c y} (φ : obj c y ⟶ obj c z) {h : ℤ} (hα : α ∈ wPart c W.pathWeight (Multiplicative.ofAdd h) x y) (g : ℤ) : (wP c W g x z) (CategoryTheory.CategoryStruct.comp α φ) = CategoryTheory.CategoryStruct.comp α ((wP c W (g - h) y z) φ)

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.projW {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) (l : ℤ) (g : MeshFamily c) : MeshFamily c

The weight-λ part of a mesh family: degree W(path) − ν_v at the row v.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.projWA {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) (l : ℤ) (f : ArrowFamily c) : ArrowFamily c

The weight-λ part of an arrow family: degree W(path) − W(a) at the arrow a.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.D_projWA {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) (l : ℤ) (f : ArrowFamily c) : meshDerivative c (projWA c W l f) = projW c W l (meshDerivative c f)

D_m preserves the weight gradings.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.wP_degreePart {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) {g : ℤ} {d : ℕ} {x y : V} {φ : obj c x ⟶ obj c y} (hφ : φ ∈ degreePart c d x y) : (wP c W g x y) φ ∈ degreePart c d x y

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.projW_mem_imageD {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) (l : ℤ) {m : ℕ} {g : MeshFamily c} (hg : g ∈ imageD c m) : projW c W l g ∈ imageD c m

The image of D_m is graded by W.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.projW_row {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) [DecidableEq V] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (l : ℤ) (x : ↑Q.nonprojective) (p : Quiver.Path ↑(Q.tau x) ↑x) : projW c W l (row c x p) = if W.pw p - W.ν x = l then row c x p else 0

A row is homogeneous of degree W(p) − ν_v.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.integralMeshCokernels_weights {V : Type v} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (W : IntWt Q) [DecidableEq V] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] {m : ℕ} (l : ℤ) : (∀ g ∈ imageD c m, projW c W l g ∈ imageD c m) ∧ ∀ (x : ↑Q.nonprojective) (p : Quiver.Path ↑(Q.tau x) ↑x), projW c W l (row c x p) = if W.pw p - W.ν x = l then row c x p else 0

The weight labels of Lemma B.2: over 𝒪 = ℤ/4 (or any coefficient ring), for every integer mesh weight W the cokernel of D_m is W-graded (the image of D_m is graded), and the class of a row p_i at v_i is homogeneous of degree χ_i(W) = W(p_i) − ν_{v_i} (eq:parameter-character). With integralMeshCokernels this is ⊕_{m≥2} coker D_m(E₄) ≅ ⊕_{i∈I} (𝒪/(2))_{χ_i}.