Higher Ext between normalized modules (Lemma 6.3(2))

positive-deformations.tex: "In a minimal graded projective cover of a nonprojective M_i, every summand P⟨a⟩ has a ≥ 1 […] A nonzero component of a kernel inclusion Z⟨b⟩ → P⟨a⟩ is also radical. […] Hence b − a ≥ 1 and b ≥ 2. […] Dimension shifting gives Ext^n(M_i, M_j)_t = Ext^1(Ω^{n−1}M_i, M_j)_t = 0 (t > −2n) […] Projective summands contribute zero."

Here the cover is P = ⊕_ℓ M_{x_ℓ}⟨d_ℓ⟩ → M_i, ℓ running over homogeneous bases of the spaces C_d(P_x, X_i) (cπ, with graded k-section cs).

Deviation: this cover need not be minimal. Minimality is used in the paper only to see that kernel summands Z⟨b⟩ have b ≥ 2. Here the bound is proved for the nonprojective summands directly (two_le_shift): every component Z → M_{x_ℓ} has degree b − d_ℓ, and it vanishes when b − d_ℓ ≤ 0, by eq:normalized-hom-degrees, since Z ≠ P_{x_ℓ}. Projective summands contribute zero whatever their shift.

The cover

noncomputable def MultiplicativeBasisDeformations.MeshWalk.cbasis {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)) (i : V) (x : D.PV) (d : ℕ) : Module.Basis (Fin (Module.finrank k ↥(ScalarMeshCategory.degreePart c d (↑x) i))) k ↥(ScalarMeshCategory.degreePart c d (↑x) i)

A homogeneous basis of C_d(P_x, X_i).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.CIdx {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)) (i : V) : Type

The index set of the cover: (x, d, basis index).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ch {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)) (i : V) (ℓ : CIdx D hfin i) : ScalarMeshCategory.obj c ↑ℓ.fst ⟶ ScalarMeshCategory.obj c i

The basis morphism h_ℓ : P_x → X_i of degree d.

theorem MultiplicativeBasisDeformations.MeshWalk.ch_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} {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) (ℓ : CIdx D hfin i) : ch D hfin i ℓ ∈ ScalarMeshCategory.degreePart c (↑ℓ.snd.fst) (↑ℓ.fst) i

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.CP {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)) (i : V) : Type u

The cover P = ⊕_ℓ M_{x_ℓ}.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.gCP {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)) (i : V) : GExt.GMod (galgA0 D hfin) (CP D hfin i)

P = ⊕_ℓ M_{x_ℓ}⟨d_ℓ⟩ as a graded module.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.cπ {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)) (i : V) : CP D hfin i →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c i)

The cover map Σ_ℓ h_ℓ.

theorem MultiplicativeBasisDeformations.MeshWalk.cπ_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} {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) (y : CP D hfin i) : (cπ D hfin i) y = ∑ ℓ : CIdx D hfin i, (CatAlg.repMap (ch D hfin i ℓ)) (y ℓ)

theorem MultiplicativeBasisDeformations.MeshWalk.cπ_act {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) (y : CP D hfin i) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (cπ D hfin i) (((gCP D hfin i).act y) a) = ((evAct D i) ((cπ D hfin i) y)) a

theorem MultiplicativeBasisDeformations.MeshWalk.cπ_deg {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) (p : ℤ) (y : CP D hfin i) (hy : (gCP D hfin i).gr.IsHom p y) : (zgrEv D hfin i).IsHom (p + 0) ((cπ D hfin i) y)

def MultiplicativeBasisDeformations.MeshWalk.evalAt {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) (i : V) (y : D.PV) : CatAlg.Rep D.F0 (meshFam Q c i) →ₗ[k] ScalarMeshCategory.obj c ↑y ⟶ ScalarMeshCategory.obj c i

Evaluation at a projective label.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ccoef {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)) (i : V) (ℓ : CIdx D hfin i) : CatAlg.Rep D.F0 (meshFam Q c i) →ₗ[k] k

The coefficient of h_ℓ in the degree-d_ℓ part of m_{x_ℓ}.

theorem MultiplicativeBasisDeformations.MeshWalk.ccoef_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} {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) (ℓ : CIdx D hfin i) (m : CatAlg.Rep D.F0 (meshFam Q c i)) : (ccoef D hfin i ℓ) m = ((cbasis D hfin i ℓ.fst ↑ℓ.snd.fst).repr ⟨(ScalarMeshCategory.degProj c (↑ℓ.snd.fst) (↑ℓ.fst) i) (m ℓ.fst), ⋯⟩) ℓ.snd.snd

noncomputable def MultiplicativeBasisDeformations.MeshWalk.cs {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)) (i : V) : CatAlg.Rep D.F0 (meshFam Q c i) →ₗ[k] CP D hfin i

The graded k-section m ↦ Σ_ℓ c_ℓ(m) 1_{x_ℓ}.

theorem MultiplicativeBasisDeformations.MeshWalk.cs_apply_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} {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) (ℓ : CIdx D hfin i) (m : CatAlg.Rep D.F0 (meshFam Q c i)) (y : D.PV) : (CatAlg.repMap (ch D hfin i ℓ)) ((cs D hfin i) m ℓ) y = if ℓ.fst = y then (ccoef D hfin i ℓ) m • CategoryTheory.CategoryStruct.comp (CatAlg.idTo y ℓ.fst) (ch D hfin i ℓ) else 0

theorem MultiplicativeBasisDeformations.MeshWalk.cπ_cs {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) : cπ D hfin i ∘ₗ cs D hfin i = LinearMap.id

theorem MultiplicativeBasisDeformations.MeshWalk.cs_deg {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) (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c i)) (hm : (zgrEv D hfin i).IsHom p m) : (gCP D hfin i).gr.IsHom (p + 0) ((cs D hfin i) m)

The kernel and its summands

noncomputable def MultiplicativeBasisDeformations.MeshWalk.KK {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) : GExt.GMod (galgA0 D hfin) ↥(cπ D hfin i).ker

The kernel Ω M_i of the cover.

theorem MultiplicativeBasisDeformations.MeshWalk.one_le_shift {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) (hi : ¬D.proj i) (ℓ : CIdx D hfin i) : 1 ≤ ↑ℓ.snd.fst

At a nonprojective label every cover summand has positive shift.

theorem MultiplicativeBasisDeformations.MeshWalk.KK_isHom {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) (p : ℤ) (x : ↥(cπ D hfin i).ker) : (KK D hfin i).gr.IsHom p x ↔ (gCP D hfin i).gr.IsHom p ↑x

theorem MultiplicativeBasisDeformations.MeshWalk.eq_zero_of_deg_nonpos {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)] {Y Z : V} (hYZ : Y ≠ Z) {s : ℤ} (hs : s ≤ 0) (u : CatAlg.Rep D.F0 (meshFam Q c Y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Z)) (hu : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c Y)) (x : (CatAlg.Alg D.F0)ᵐᵒᵖ), u (((evAct D Y) m) x) = ((evAct D Z) (u m)) x) (hdeg : ∀ (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c Y)), (zgrEv D hfin Y).IsHom p m → (zgrEv D hfin Z).IsHom (p + s) (u m)) : u = 0

A graded map of degree s ≤ 0 between evaluated modules at distinct labels vanishes.

theorem MultiplicativeBasisDeformations.MeshWalk.two_le_shift {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) (hi : ¬D.proj i) (d : GDecomp D hfin (KK D hfin i) LinearMap.id) (a : d.μ) (ha : d.inc a ≠ 0) (hz : ¬D.proj (d.W a)) : 2 ≤ d.s a

Nonprojective kernel summands have shift at least two.

The vanishing

theorem MultiplicativeBasisDeformations.MeshWalk.extVanish_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)] (J : D.InjData) (h1 : DegOne D) (n : ℕ) (i j : V) (t : ℤ) : D.proj i ∨ -2 * (↑n + 1) < t → GExt.ExtVanish (gmodEv D hfin i) (gmodEv D hfin j) n t

Lemma 6.3(2): Ext^{n+1}_{A₀}(M_i, M_j)_t = 0 for t > -2(n+1), and for all t when M_i is projective.