The degree-two part of the mesh ideal

Lemma 4.13 (scalar-normalization.tex): "Since Φ preserves the mesh ideal, whose degree-two part from τX to X is spanned by the mesh relation at X, it multiplies that relation by some ν_X ∈ k*. Comparing coefficients gives w(σa) w(a) = ν_X for every mate pair at that mesh."

The mesh ideal is spanned by composites u r_Y v; their degree-two parts from τX to X are those with u, v of degree zero, hence Y = X and u, v scalars (proj_two_mem_span). A linear relation among the composites (σa) a in C(Q, c) is therefore proportional to the mesh coefficients (mesh_coeffs).

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.mesh_sum_zero {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x : ↑Q.nonprojective) : ∑ a : (y : V) × (y ⟶ ↑x), ↑(c x a.fst a.snd) • CategoryTheory.CategoryStruct.comp (arrowMor c ((Q.mate x a.fst) a.snd)) (arrowMor c a.snd) = 0

The mesh relation vanishes in C(Q, c).

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.proj_two_comp {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x z : ↑Q.nonprojective) (u : LinearPaths.obj ↑(Q.tau x) ⟶ LinearPaths.obj ↑(Q.tau z)) (w' : LinearPaths.obj ↑z ⟶ LinearPaths.obj ↑x) : (LinearPaths.proj 2 ↑(Q.tau x) ↑x) (CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (meshRelation c z) w')) = CategoryTheory.CategoryStruct.comp ((LinearPaths.proj 0 ↑(Q.tau x) ↑(Q.tau z)) u) (CategoryTheory.CategoryStruct.comp (meshRelation c z) ((LinearPaths.proj 0 ↑z ↑x) w'))

The degree-two part of a two-sided composite through a mesh relation.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.proj_two_mem_span {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x : ↑Q.nonprojective) {f : LinearPaths.obj ↑(Q.tau x) ⟶ LinearPaths.obj ↑x} (hf : f ∈ CategoricalIdeal.HomIdeal.generatedHomSubmodule k (meshRelations c) (LinearPaths.obj ↑(Q.tau x)) (LinearPaths.obj ↑x)) : (LinearPaths.proj 2 ↑(Q.tau x) ↑x) f ∈ k ∙ meshRelation c x

The degree-two part of the mesh ideal from τX to X is spanned by the mesh relation at X.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.meshPath {V : Type v} [Quiver V] {Q : TranslationQuiver V} (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) : Quiver.Path ↑(Q.tau x) ↑x

The two-arrow path (σ a) a of a mesh.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.meshPath_injective {V : Type v} [Quiver V] {Q : TranslationQuiver V} (x : ↑Q.nonprojective) : Function.Injective (meshPath x)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.coeff_meshPath {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} (x : ↑Q.nonprojective) [Fintype ((y : V) × (y ⟶ ↑x))] (μ : (y : V) × (y ⟶ ↑x) → k) (a : (y : V) × (y ⟶ ↑x)) : (LinearPaths.toFinsupp (∑ e : (y : V) × (y ⟶ ↑x), μ e • LinearPaths.path (meshPath x e))) (meshPath x a) = μ a

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.mesh_coeffs {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x : ↑Q.nonprojective) (lam : (y : V) × (y ⟶ ↑x) → k) (h : ∑ a : (y : V) × (y ⟶ ↑x), lam a • CategoryTheory.CategoryStruct.comp (arrowMor c ((Q.mate x a.fst) a.snd)) (arrowMor c a.snd) = 0) : ∃ (ν : k), ∀ (a : (y : V) × (y ⟶ ↑x)), lam a = ν * ↑(c x a.fst a.snd)

Comparing coefficients: a linear relation among the composites (σ a) a is proportional to the mesh relation.