Functionals on Π(Δ) modulo deleted vertices

Tools for the nonvanishing statements of Appendix A (periodic-mesh-calculations.tex: "Assigning these values in k gives a nonzero functional annihilating all the relations"). A function g on vertex lists gives a functional on paths (vfun); it annihilates the ideal of Π(Δ) modulo the deleted vertices when its values on the terms of each contextual relation cancel and it vanishes on lists through deleted vertices (vfun_eq_zero_of_mem). The constant term (len0) shows that the vertex idempotents of retained vertices are nonzero.

theorem Quiver.Path.vertices_eq_cons {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) : p.vertices = a :: p.vertices.tail

noncomputable def MultiplicativeBasisDeformations.OrientedTree.vfun {D : Type v} (T : OrientedTree D) {k : Type u} [Field k] {x y : T.Dbl} (g : List T.Dbl → k) : (LinearPaths.obj x ⟶ LinearPaths.obj y) →ₗ[k] k

The functional of a function on vertex lists.

theorem MultiplicativeBasisDeformations.OrientedTree.vfun_path {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] {k : Type u} [Field k] {x y : T.Dbl} (g : List T.Dbl → k) (q : Quiver.Path x y) : (T.vfun g) (LinearPaths.path q) = g q.vertices

theorem MultiplicativeBasisDeformations.OrientedTree.vfun_rel {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] {k : Type u} [Field k] (g : List T.Dbl → k) {x y u : T.Dbl} (p : Quiver.Path x u) (p' : Quiver.Path u y) : (T.vfun g) (CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.CategoryStruct.comp (T.preprojRel k u) (LinearPaths.path p'))) = ∑ e : (w : T.Dbl) × (u ⟶ w), ↑(T.sgn k u e.fst) * g (p.vertices.dropLast ++ u :: e.fst :: u :: p'.vertices.tail)

The value on a contextual relation.

theorem MultiplicativeBasisDeformations.OrientedTree.vfun_eq_zero_of_mem {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] {k : Type u} [Field k] (Del : Set T.Dbl) (g : List T.Dbl → k) (hrel : ∀ (u : T.Dbl) (l₀ l₂ : List T.Dbl), ∑ e : (w : T.Dbl) × (u ⟶ w), ↑(T.sgn k u e.fst) * g (l₀ ++ u :: e.fst :: u :: l₂) = 0) (hdel : ∀ (l : List T.Dbl), (∃ d ∈ l, d ∈ Del) → g l = 0) {x y : T.Dbl} {f : LinearPaths.obj x ⟶ LinearPaths.obj y} (hf : f ∈ ((T.preproj k).del Del).ideal (LinearPaths.obj x) (LinearPaths.obj y)) : (T.vfun g) f = 0

A vertex-list functional annihilating the relations.

noncomputable def MultiplicativeBasisDeformations.OrientedTree.len0 {D : Type v} (T : OrientedTree D) {k : Type u} [Field k] {x y : T.Dbl} : (LinearPaths.obj x ⟶ LinearPaths.obj y) →ₗ[k] k

The coefficient of the paths of length zero.

theorem MultiplicativeBasisDeformations.OrientedTree.nil_not_mem_del {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] {k : Type u} [Field k] (Del : Set T.Dbl) {x : T.Dbl} (hx : x ∉ Del) : LinearPaths.path Quiver.Path.nil ∉ ((T.preproj k).del Del).ideal (LinearPaths.obj x) (LinearPaths.obj x)

Retained vertex idempotents are nonzero in Π(Δ) modulo deleted vertices.