Lemma 6.3(2) with Ext from graded projective resolutions

positive-deformations.tex: internal degree t in Ext means degree-t maps from a graded projective resolution, and Ext^n_{A₀}(M_i, M_j)_t = 0 for n ≥ 1, t > −2n. Every M_i has a graded projective resolution (exists_gres_ev), and for every one of them the Ext computed from it vanishes in the stated range (extVanish_ev_res), by the comparison with the bar Ext (GExt.GRes.extVanish_iff) and the bar form of the lemma (extVanish_ev).

theorem MultiplicativeBasisDeformations.MeshWalk.finite_A0op {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) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] : Module.Finite k (CatAlg.Alg D.F0)ᵐᵒᵖ

A₀ is finite-dimensional.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_gres_ev {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)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (i : V) : Nonempty (GExt.GRes (gmodEv D hfin i))

Every M_i has a graded projective resolution (by finite free graded A₀-modules).

theorem MultiplicativeBasisDeformations.MeshWalk.gres_extVanish_iff {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)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (i j : V) (Rs : GExt.GRes (gmodEv D hfin i)) (n : ℕ) (t : ℤ) : Rs.ExtVanish (gmodEv D hfin j) n t ↔ GExt.ExtVanish (gmodEv D hfin i) (gmodEv D hfin j) n t

The Ext of any graded projective resolution of M_i is the bar Ext.

theorem MultiplicativeBasisDeformations.MeshWalk.extVanish_ev_res {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)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (J : D.InjData) (h1 : DegOne D) (n : ℕ) (i j : V) (t : ℤ) (ht : D.proj i ∨ -2 * (↑n + 1) < t) (Rs : GExt.GRes (gmodEv D hfin i)) : Rs.ExtVanish (gmodEv D hfin j) n t

Lemma 6.3(2) (lem:positive-ext-vanishing), with Ext as in the manuscript: for every graded projective resolution of M_i, the Ext^{n+1}_{A₀}(M_i, M_j)_t computed from it vanishes for t > −2(n+1), and for all t when M_i is projective.