Ext¹ between normalized modules (Lemma 6.3, n = 1)

positive-deformations.tex: "At a nonprojective label i, Lemma 2.9 and Proposition 2.6 give an exact sequence of representable functors […] We obtain a short exact sequence with terms M_{τi}, the middle mesh summands, and M_i, and both maps have degree one. […] It is right almost split […] Shifting its terms to make its maps degree zero gives 0 → M_{τi}⟨2⟩ → ⊕_{Y→i} M_Y⟨1⟩ → M_i → 0. Suppose that 0 → M_j⟨-t⟩ → X → M_i → 0 is a nonsplit graded extension with t > -2. It remains nonsplit after forgetting the grading […] Thus v factors through the right almost split map. Taking the degree-zero part makes this factorization graded. The induced map on kernels from M_j⟨-t⟩ to M_{τi}⟨2⟩ has underlying degree -t-2, so it is zero […] The factorization therefore descends to a section of the right almost split map, a contradiction."

Here: the evaluated mesh maps πE, ιτ (exact_E, ιτ_injective), the right almost split property (exists_factor, not_retraction), and the vanishing (extOne_vanish).

@[reducible, inline]

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

The middle term ⊕_a M_{mid a} of the mesh at x.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.πE {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) (x : V) : Emid D x →ₗ[CatAlg.Alg D.F0] CatAlg.Rep D.F0 (meshFam Q c x)

The evaluated right mesh map ⊕_a M_{mid a} → M_x.

theorem MultiplicativeBasisDeformations.MeshWalk.πE_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) (x : V) (m : Emid D x) (y : D.PV) : (πE D x) m y = ∑ a : D.Mid x, CategoryTheory.CategoryStruct.comp (m a y) (D.p x a)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ιτ {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) (x : V) (hx : ¬D.proj x) : CatAlg.Rep D.F0 (meshFam Q c (D.tau x hx)) →ₗ[CatAlg.Alg D.F0] Emid D x

The evaluated left mesh map M_{τx} → ⊕_a M_{mid a}.

theorem MultiplicativeBasisDeformations.MeshWalk.ιτ_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) (x : V) (hx : ¬D.proj x) (m : CatAlg.Rep D.F0 (meshFam Q c (D.tau x hx))) (a : D.Mid x) (y : D.PV) : (ιτ D x hx) m a y = CategoryTheory.CategoryStruct.comp (m y) (D.q x hx a)

theorem MultiplicativeBasisDeformations.MeshWalk.ιτ_injective {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) (x : V) (hx : ¬D.proj x) : Function.Injective ⇑(ιτ D x hx)

theorem MultiplicativeBasisDeformations.MeshWalk.πE_ιτ {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) (x : V) (hx : ¬D.proj x) (m : CatAlg.Rep D.F0 (meshFam Q c (D.tau x hx))) : (πE D x) ((ιτ D x hx) m) = 0

theorem MultiplicativeBasisDeformations.MeshWalk.exact_E {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) (x : V) (hx : ¬D.proj x) {m : Emid D x} (hm : (πE D x) m = 0) : ∃ (r : CatAlg.Rep D.F0 (meshFam Q c (D.tau x hx))), (ιτ D x hx) r = m

Exactness at the middle term.

theorem MultiplicativeBasisDeformations.MeshWalk.not_retraction {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)] (x : V) (w : CatAlg.Rep D.F0 (meshFam Q c x) →ₗ[CatAlg.Alg D.F0] Emid D x) (hw : πE D x ∘ₗ w = LinearMap.id) : False

πE is not a retraction: its components are radical.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_factor {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)] (J : D.InjData) {X : Type u_1} [AddCommGroup X] [Module k X] [Module (CatAlg.Alg D.F0) X] [IsScalarTower k (CatAlg.Alg D.F0) X] [FiniteDimensional k X] (x : V) (g : X →ₗ[CatAlg.Alg D.F0] CatAlg.Rep D.F0 (meshFam Q c x)) (hg : ¬∃ (s : CatAlg.Rep D.F0 (meshFam Q c x) →ₗ[CatAlg.Alg D.F0] X), g ∘ₗ s = LinearMap.id) : ∃ (u : X →ₗ[CatAlg.Alg D.F0] Emid D x), πE D x ∘ₗ u = g

πE is right almost split: a non-retraction into M_x factors through it.

theorem MultiplicativeBasisDeformations.MeshWalk.πE_injective {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)] (x : V) (hx : D.proj x) : Function.Injective ⇑(πE D x)

Degrees of the mesh maps

theorem MultiplicativeBasisDeformations.MeshWalk.repMap_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)] {X Y : V} {s : ℕ} {f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y} (hf : f ∈ ScalarMeshCategory.degreePart c s X Y) {p : ℤ} {m : CatAlg.Rep D.F0 (meshFam Q c X)} (hm : (zgrEv D hfin X).IsHom p m) : (zgrEv D hfin Y).IsHom (p + ↑s) ((CatAlg.repMap f) m)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.gE {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)) (x : V) : GExt.GMod (galgA0 D hfin) (Emid D x)

The middle term ⊕_a M_{mid a}⟨1⟩ as a graded module.

structure MultiplicativeBasisDeformations.MeshWalk.DegOne {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) : Prop

The mesh maps have degree one.

• p (x : V) (a : D.Mid x) : D.p x a ∈ ScalarMeshCategory.degreePart c 1 (D.mid x a) x
• q (x : V) (hx : ¬D.proj x) (a : D.Mid x) : D.q x hx a ∈ ScalarMeshCategory.degreePart c 1 (D.tau x hx) (D.mid x a)

theorem MultiplicativeBasisDeformations.MeshWalk.πE_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)] (h1 : DegOne D) (x : V) (p : ℤ) (m : Emid D x) (hm : (gE D hfin x).gr.IsHom p m) : (zgrEv D hfin x).IsHom (p + 0) ((πE D x) m)

theorem MultiplicativeBasisDeformations.MeshWalk.ιτ_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)] (h1 : DegOne D) (x : V) (hx : ¬D.proj x) (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c (D.tau x hx))) (hm : (zgrEv D hfin (D.tau x hx)).IsHom p m) : (gE D hfin x).gr.IsHom (p + 2) ((ιτ D x hx) m)

The vanishing

theorem MultiplicativeBasisDeformations.MeshWalk.extOne_vanish {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) (i j : V) {t : ℤ} (ht : -2 < t) : GExt.ExtVanish (gmodEv D hfin i) (gmodEv D hfin j) 0 t

Lemma 6.3(2), n = 1: Ext¹_{A₀}(M_i, M_j)_t = 0 for t > -2.