Uniqueness of the graded Ext of Lemma 6.3

The formalization works with Ext^{n+1}(M, N)_t = 0 in the bar form (GExt.ExtVanish); its agreement with the manuscript's Ext (from graded projective resolutions) is GRes.extVanish_iff in ExtResolutions.lean. This file shows in addition that the definition is forced: any notion of graded Ext vanishing with the standard properties gives the same answer for all the groups Ext^{n+1}_{A₀}(M_i, M_j)_t of Lemma 6.3 (extVanish_unique). The properties are:

• Ext¹(M, N)_t = 0 exactly when every graded extension 0 → N⟨−t⟩ → E → M → 0 splits;
• higher Ext of a projective M_p vanishes;
• dimension shifting along the graded projective cover 0 → K_i → P_i → M_i → 0: Ext^{n+2}(M_i, N)_t = 0 ↔ Ext^{n+1}(K_i, N)_t = 0;
• additivity over a graded decomposition of K_i into shifted M_j. The bar Ext has them all: extensions (extVanish_zero_iff), projectives (extVanish_proj), dimension shifting in both directions (extVanish_shift, extVanish_unshift), additivity in both directions (extVanish_of_decomp, extVanish_of_retract).

theorem MultiplicativeBasisDeformations.GExt.extVanish_unshift {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} {K : Type u_5} {P : Type u_6} [AddCommGroup K] [Module R K] [AddCommGroup P] [Module R P] {KK : GMod GΛ K} {PP : GMod GΛ P} (ι : K →ₗ[R] P) (π : P →ₗ[R] M) (s : M →ₗ[R] P) (ρ : P →ₗ[R] K) (hι : ∀ (m : K) (a : Λ), ι ((KK.act m) a) = (PP.act (ι m)) a) (hπ : ∀ (m : P) (a : Λ), π ((PP.act m) a) = (MM.act (π m)) a) (hι_deg : ∀ (p : ℤ) (m : K), KK.gr.IsHom p m → PP.gr.IsHom (p + 0) (ι m)) (hπ_deg : ∀ (p : ℤ) (m : P), PP.gr.IsHom p m → MM.gr.IsHom (p + 0) (π m)) (hs_deg : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → PP.gr.IsHom (p + 0) (s m)) (hρ_deg : ∀ (p : ℤ) (m : P), PP.gr.IsHom p m → KK.gr.IsHom (p + 0) (ρ m)) (hπs : π ∘ₗ s = LinearMap.id) (hρι : ρ ∘ₗ ι = LinearMap.id) (hsplit : ι ∘ₗ ρ + s ∘ₗ π = LinearMap.id) (hπι : π ∘ₗ ι = 0) {n : ℕ} {t : ℤ} (hP : ExtVanish PP NN n t) (hM : ExtVanish MM NN (n + 1) t) : ExtVanish KK NN n t

Dimension shifting, converse: along an R-split exact sequence 0 → K → P → M → 0 of graded modules with Ext^{n+1}(P, N)_t = 0, Ext^{n+2}(M, N)_t = 0 gives Ext^{n+1}(K, N)_t = 0.

theorem MultiplicativeBasisDeformations.GExt.extVanish_of_retract {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} {M' : Type u_5} [AddCommGroup M'] [Module R M'] {MM' : GMod GΛ M'} (inc : M' →ₗ[R] M) (pr : M →ₗ[R] M') (s : ℤ) (hinc : ∀ (m : M') (x : Λ), inc ((MM'.act m) x) = (MM.act (inc m)) x) (hpr : ∀ (m : M) (x : Λ), pr ((MM.act m) x) = (MM'.act (pr m)) x) (hinc_deg : ∀ (p : ℤ) (m : M'), MM'.gr.IsHom p m → MM.gr.IsHom (p + s) (inc m)) (hpr_deg : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → MM'.gr.IsHom (p + -s) (pr m)) (hpi : pr ∘ₗ inc = LinearMap.id) {n : ℕ} {t : ℤ} (h : ExtVanish MM NN n t) : ExtVanish MM' NN n (t + s)

A graded direct summand inherits Ext vanishing.

theorem MultiplicativeBasisDeformations.MeshWalk.extVanish_cover_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 : V) {N : Type u_1} [AddCommGroup N] [Module k N] (NN : GExt.GMod (galgA0 D hfin) N) (n : ℕ) (t : ℤ) : GExt.ExtVanish (gmodEv D hfin i) NN (n + 1) t ↔ GExt.ExtVanish (KK D hfin i) NN n t

Dimension shifting along the cover of M_i, both directions.

theorem MultiplicativeBasisDeformations.MeshWalk.extVanish_decomp_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)] {X : Type u} [AddCommGroup X] [Module k X] {XX : GExt.GMod (galgA0 D hfin) X} (d : GDecomp D hfin XX LinearMap.id) {N : Type u_1} [AddCommGroup N] [Module k N] (NN : GExt.GMod (galgA0 D hfin) N) (n : ℕ) (t : ℤ) : GExt.ExtVanish XX NN n t ↔ ∀ (a : d.μ), d.inc a ≠ 0 → GExt.ExtVanish (gmodEv D hfin (d.W a)) NN n (t + d.s a)

Additivity over a graded decomposition, both directions.

theorem MultiplicativeBasisDeformations.MeshWalk.extVanish_unique {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) (j : V) (E : {X : Type u} → [inst : AddCommGroup X] → [inst_1 : Module k X] → GExt.GMod (galgA0 D hfin) X → ℕ → ℤ → Prop) (hE0 : ∀ (i : V) (t : ℤ), E (gmodEv D hfin i) 0 t ↔ ∀ (X : GExt.GExtn (gmodEv D hfin i) (gmodEv D hfin j) t (CatAlg.Rep D.F0 (meshFam Q c j) × CatAlg.Rep D.F0 (meshFam Q c i))), X.Splits) (hEproj : ∀ (p : D.PV) (n : ℕ) (t : ℤ), E (gmodEv D hfin ↑p) n t) (hEshift : ∀ (i : V), ¬D.proj i → ∀ (n : ℕ) (t : ℤ), E (gmodEv D hfin i) (n + 1) t ↔ E (KK D hfin i) n t) (hEdecomp : ∀ (i : V) (d : GDecomp D hfin (KK D hfin i) LinearMap.id) (n : ℕ) (t : ℤ), E (KK D hfin i) n t ↔ ∀ (a : d.μ), d.inc a ≠ 0 → E (gmodEv D hfin (d.W a)) n (t + d.s a)) (n : ℕ) (i : V) (t : ℤ) : E (gmodEv D hfin i) n t ↔ GExt.ExtVanish (gmodEv D hfin i) (gmodEv D hfin j) n t

Uniqueness of the graded Ext of Lemma 6.3: any notion E of graded Ext^{n+1}(−, M_j)_t vanishing on graded A₀-modules such that

• E(M_i, 0, t) holds exactly when every graded extension of M_i by M_j⟨−t⟩ splits,
• E(M_p, n, t) holds at projective labels,
• E(M_i, n+1, t) ↔ E(K_i, n, t) along the graded projective cover K_i ↪ P_i ↠ M_i,
• E(K, n, t) ↔ ∀ a, E(M_{W a}, n, t + s_a) for a graded decomposition K ≅ ⊕_a M_{W a}⟨s_a⟩, agrees with the bar-complex Ext on every Ext^{n+1}_{A₀}(M_i, M_j)_t.