Evaluated projectives (Lemma 6.3)

positive-deformations.tex: "The projectives are included with their regular gradings. […] Projective summands contribute zero." At a projective label p, the evaluated module M_p = R⁰_{F p} is the cyclic graded projective e_p A₀ generated in degree 0 by 1_p (Yoneda: colAlg, colAlg_smul_unit), so all its higher Ext groups vanish (extVanish_proj).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.cycProj {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} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (p : D.PV) : GExt.CycProj (gmodEv D hfin ↑p)

M_p is cyclic projective, generated by 1_p in degree 0.

theorem MultiplicativeBasisDeformations.MeshWalk.extVanish_proj {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} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (p : D.PV) {N : Type u_1} [AddCommGroup N] [Module k N] (NN : GExt.GMod (galgA0 D hfin) N) (n : ℕ) (t : ℤ) : GExt.ExtVanish (gmodEv D hfin ↑p) NN n t

Ext out of an evaluated projective vanishes.