Graded decomposition (Lemma 6.3(1))

positive-deformations.tex: "Every finite graded A₀-module is a sum of shifts of the M_i. […] Decompose its underlying ungraded module into normalized modules M_i. Write the projections and inclusions as p_a and j_a, so 1_X = Σ_a p_a j_a. Taking homogeneous degree-zero parts gives 1_X = Σ_{a,r} (p_a)_r (j_a)_{-r}."

Deviation in the proof: instead of the locality of End_gr(X) for a graded indecomposable X, we split off one shifted M_W at a time from a graded idempotent e (exists_summand). Some composite (p_a)_r (j_b)_{-r} of equal level is nonzero, hence invertible by eq:normalized-hom-degrees (exists_inv); otherwise the level sums E_r satisfy E_r E_s = 0 for r ≤ s and force e = 0. The result (exists_gdecomp) is a finite family of graded inclusions and projections with Σ inc_a pr_a = 1, which is the input of extVanish_of_decomp.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_inv {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} (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)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), u (((evAct D Y) m) a) = ((evAct D Z) (u m)) a) (hdeg : ∀ (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c Y)), (zgrEv D hfin Y).IsHom p m → (zgrEv D hfin Z).IsHom (p + 0) (u m)) (hne : u ≠ 0) : ∃ (v : CatAlg.Rep D.F0 (meshFam Q c Z) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)), (∀ (m : CatAlg.Rep D.F0 (meshFam Q c Z)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), v (((evAct D Z) m) a) = ((evAct D Y) (v m)) a) ∧ (∀ (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c Z)), (zgrEv D hfin Z).IsHom p m → (zgrEv D hfin Y).IsHom (p + 0) (v m)) ∧ u ∘ₗ v = LinearMap.id

A nonzero degree-zero map between evaluated modules is invertible.

structure MultiplicativeBasisDeformations.MeshWalk.IsGE {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 : Type u_1} [AddCommGroup X] [Module k X] (XX : GExt.GMod (galgA0 D hfin) X) (f : X →ₗ[k] X) : Prop

A graded A₀-linear endomorphism of degree zero.

• act (m : X) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : f ((XX.act m) a) = (XX.act (f m)) a
• deg (p : ℤ) (m : X) : XX.gr.IsHom p m → XX.gr.IsHom (p + 0) (f m)

theorem MultiplicativeBasisDeformations.MeshWalk.IsGE.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)] {X : Type u_1} [AddCommGroup X] [Module k X] [FiniteDimensional k X] {XX : GExt.GMod (galgA0 D hfin) X} {f : X →ₗ[k] X} (hf : IsGE D hfin XX f) (p : ℤ) (m : X) (hm : XX.gr.IsHom p m) : XX.gr.IsHom p (f m)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_summand {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_1} [AddCommGroup X] [Module k X] [FiniteDimensional k X] (XX : GExt.GMod (galgA0 D hfin) X) (J : D.InjData) {e : X →ₗ[k] X} (he : IsGE D hfin XX e) (hee : e ∘ₗ e = e) (hne : e ≠ 0) : ∃ (W : V) (r : ℤ) (α : CatAlg.Rep D.F0 (meshFam Q c W) →ₗ[k] X) (β : X →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c W)), (∀ (m : CatAlg.Rep D.F0 (meshFam Q c W)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), α (((evAct D W) m) a) = (XX.act (α m)) a) ∧ (∀ (m : X) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), β ((XX.act m) a) = ((evAct D W) (β m)) a) ∧ (∀ (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c W)), (zgrEv D hfin W).IsHom p m → XX.gr.IsHom (p + r) (α m)) ∧ (∀ (p : ℤ) (m : X), XX.gr.IsHom p m → (zgrEv D hfin W).IsHom (p + -r) (β m)) ∧ β ∘ₗ α = LinearMap.id ∧ e ∘ₗ α = α ∧ β ∘ₗ e = β ∧ ∃ (m : CatAlg.Rep D.F0 (meshFam Q c W)), α m ≠ 0

One shifted M_W splits off a nonzero graded idempotent.

structure MultiplicativeBasisDeformations.MeshWalk.GDecomp {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 : Type u_1} [AddCommGroup X] [Module k X] (XX : GExt.GMod (galgA0 D hfin) X) (e : X →ₗ[k] X) : Type (max (max 1 u) u_1)

A graded decomposition of a graded idempotent e into shifted evaluated modules: e = Σ_a inc_a pr_a with inc_a : M_{W a}⟨s_a⟩ → X and pr_a : X → M_{W a}⟨s_a⟩ graded A₀-linear of degree zero.

• μ : Type
• fin : Fintype self.μ
• W : self.μ → V
• s : self.μ → ℤ
• inc (a : self.μ) : CatAlg.Rep D.F0 (meshFam Q c (self.W a)) →ₗ[k] X
• pr (a : self.μ) : X →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c (self.W a))
• inc_act (a : self.μ) (m : CatAlg.Rep D.F0 (meshFam Q c (self.W a))) (x : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (self.inc a) (((evAct D (self.W a)) m) x) = (XX.act ((self.inc a) m)) x
• pr_act (a : self.μ) (m : X) (x : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (self.pr a) ((XX.act m) x) = ((evAct D (self.W a)) ((self.pr a) m)) x
• inc_deg (a : self.μ) (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c (self.W a))) : (zgrEv D hfin (self.W a)).IsHom p m → XX.gr.IsHom (p + self.s a) ((self.inc a) m)
• pr_deg (a : self.μ) (p : ℤ) (m : X) : XX.gr.IsHom p m → (zgrEv D hfin (self.W a)).IsHom (p + -self.s a) ((self.pr a) m)
• sum : ∑ a : self.μ, self.inc a ∘ₗ self.pr a = e
• pr_inc (a : self.μ) : self.pr a ∘ₗ self.inc a = LinearMap.id

theorem MultiplicativeBasisDeformations.MeshWalk.exists_gdecomp_of_idem {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_1} [AddCommGroup X] [Module k X] [FiniteDimensional k X] (XX : GExt.GMod (galgA0 D hfin) X) (J : D.InjData) (e : X →ₗ[k] X) (he : IsGE D hfin XX e) (hee : e ∘ₗ e = e) : Nonempty (GDecomp D hfin XX e)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_gdecomp {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_1} [AddCommGroup X] [Module k X] [FiniteDimensional k X] (XX : GExt.GMod (galgA0 D hfin) X) (J : D.InjData) : Nonempty (GDecomp D hfin XX LinearMap.id)

Lemma 6.3(1): every finite graded A₀-module is a finite sum of shifts of evaluated modules.