Weights of mesh corrections (Proposition 7.6, weights)

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".

mfProj χ, afProj χ are the relative weight-χ projections of mesh and arrow families; D_m commutes with them (meshDerivative_afProj), so they descend to the cokernel (cokerProj). Consequently, when the rows of S span the cokernels, a family of relative weight χ lies in the span of the rows of S of relative weight χ (mem_rowSpan_char), and so does the class Ψ[μ] of a cocycle of character χ (Ψc_mem_rowSpan_char).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.mfProj {k : Type u} [Field k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (χ : M) : ScalarMeshCategory.MeshFamily c →ₗ[k] ScalarMeshCategory.MeshFamily c

The relative weight-χ projection of mesh families.

theorem MultiplicativeBasisDeformations.MeshWalk.mfProj_apply {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (χ : M) (z : ScalarMeshCategory.MeshFamily c) (x : ↑Q.nonprojective) : (mfProj W χ) z x = (wπ c W (W.ν x + χ) ↑(Q.tau x) ↑x) (z x)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.afProj {k : Type u} [Field k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (χ : M) : ScalarMeshCategory.ArrowFamily c →ₗ[k] ScalarMeshCategory.ArrowFamily c

The relative weight-χ projection of arrow families.

theorem MultiplicativeBasisDeformations.MeshWalk.afProj_apply {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (χ : M) (f : ScalarMeshCategory.ArrowFamily c) (a : (x : V) × (y : V) × (x ⟶ y)) : (afProj W χ) f a = (wπ c W (W.w a.snd.snd + χ) a.fst a.snd.fst) (f a)

theorem MultiplicativeBasisDeformations.MeshWalk.meshDerivative_afProj {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (χ : M) (f : ScalarMeshCategory.ArrowFamily c) : ScalarMeshCategory.meshDerivative c ((afProj W χ) f) = (mfProj W χ) (ScalarMeshCategory.meshDerivative c f)

D_m preserves the relative weights.

theorem MultiplicativeBasisDeformations.MeshWalk.afProj_mem {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (χ : M) {m : ℕ} {f : ScalarMeshCategory.ArrowFamily c} (hf : f ∈ ScalarMeshCategory.familiesDeg c m) : (afProj W χ) f ∈ ScalarMeshCategory.familiesDeg c m

theorem MultiplicativeBasisDeformations.MeshWalk.mfProj_imageD {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (χ : M) (m : ℕ) : ScalarMeshCategory.imageD c m ≤ Submodule.comap (mfProj W χ) (ScalarMeshCategory.imageD c m)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.cokerProj {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (χ : M) (m : ℕ) : ScalarMeshCategory.Coker c m →ₗ[k] ScalarMeshCategory.Coker c m

The relative weight-χ projection of the cokernel.

theorem MultiplicativeBasisDeformations.MeshWalk.mfProj_row {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (χ : M) (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x) : (mfProj W χ) (ScalarMeshCategory.row c x w) = if W.pw w = W.ν x + χ then ScalarMeshCategory.row c x w else 0

def MultiplicativeBasisDeformations.MeshWalk.rowsOf {V : Type} [Quiver V] {Q : TranslationQuiver V} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (χ : M) (S : ScalarMeshCategory.RowSet Q) : ScalarMeshCategory.RowSet Q

The rows of S of relative weight χ.

theorem MultiplicativeBasisDeformations.MeshWalk.cokerProj_rowSpan {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (χ : M) (m : ℕ) (S : ScalarMeshCategory.RowSet Q) : Submodule.map (cokerProj W hfin χ m) (ScalarMeshCategory.rowSpan c m S) ≤ ScalarMeshCategory.rowSpan c m (rowsOf W χ S)

theorem MultiplicativeBasisDeformations.MeshWalk.mk_mem_rowSpan {k : Type u} [Field k] {V : Type} [Quiver V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} [Fintype ↑Q.nonprojective] {S : ScalarMeshCategory.RowSet Q} (hS : ScalarMeshCategory.CokerSpan c S) {m : ℕ} (hm : 2 ≤ m) (z : ScalarMeshCategory.MeshFamily c) (hz : ∀ (x : ↑Q.nonprojective), z x ∈ ScalarMeshCategory.degreePart c (m + 1) ↑(Q.tau x) ↑x) : Submodule.Quotient.mk z ∈ ScalarMeshCategory.rowSpan c m S

theorem MultiplicativeBasisDeformations.MeshWalk.mem_rowSpan_char {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (χ : M) [Fintype ↑Q.nonprojective] {S : ScalarMeshCategory.RowSet Q} (hS : ScalarMeshCategory.CokerSpan c S) {m : ℕ} (hm : 2 ≤ m) (z : ScalarMeshCategory.MeshFamily c) (hz : ∀ (x : ↑Q.nonprojective), z x ∈ ScalarMeshCategory.degreePart c (m + 1) ↑(Q.tau x) ↑x) (hzw : ∀ (x : ↑Q.nonprojective), z x ∈ wP c W (W.ν x + χ) ↑(Q.tau x) ↑x) : Submodule.Quotient.mk z ∈ ScalarMeshCategory.rowSpan c m (rowsOf W χ S)

A family of relative weight χ lies in the span of the rows of weight χ.

The class Ψ of a cocycle of character χ

theorem MultiplicativeBasisDeformations.MeshWalk.Ψc_mem_rowSpan_char {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (χ : M) [Fintype ↑Q.nonprojective] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (J : D.InjData) (h1 : DegOne D) (hμχ : HasChar W hfin D χ μ) {S : ScalarMeshCategory.RowSet Q} (hS : ScalarMeshCategory.CokerSpan c S) (hq : 1 ≤ q) (Ld : LiftData D hfin q μ) : Ψc Ld ∈ ScalarMeshCategory.rowSpan c (q + 1) (rowsOf W χ S)

Proposition 7.6, weights (weights-and-parameters.tex): the class Ψ[μ] of a cocycle of character χ lies in the span of the spanning rows of relative weight χ.