A₀ and its evaluated modules as graded objects

Section 6 (positive-deformations.tex): "Let M_1, …, M_h be the degree-normalized graded indecomposable A₀-modules obtained by evaluating the objects of C: the degree-d part at x is C_d(P_x, X_i)." Here A₀ = (Alg F₀)ᵒᵖ is ℤ-graded through lenA0 (galgA0), and the evaluation M_X = Rep F₀ X of an object X of the mesh category is a graded right A₀-module (gmodEv), with m·a = a.unop • m.

def MultiplicativeBasisDeformations.GExt.ZGr.ofLen {k : Type u_1} [Field k] {B : Type u_2} [Ring B] [Algebra k B] (G : LenGrading k B) : ZGr B

A length grading as a ℤ-grading.

theorem MultiplicativeBasisDeformations.GExt.ZGr.ofLen_isHom {k : Type u_1} [Field k] {B : Type u_2} [Ring B] [Algebra k B] (G : LenGrading k B) (d : ℕ) (b : B) : (ofLen G).IsHom (↑d) b ↔ G.IsHom d b

theorem MultiplicativeBasisDeformations.GExt.ZGr.ofLen_isHom_neg {k : Type u_1} [Field k] {B : Type u_2} [Ring B] [Algebra k B] (G : LenGrading k B) {p : ℤ} (hp : p < 0) (b : B) : (ofLen G).IsHom p b ↔ b = 0

def MultiplicativeBasisDeformations.GExt.GAlg.ofLen {k : Type u_1} [Field k] {B : Type u_2} [Ring B] [Algebra k B] (G : LenGrading k B) (h1 : G.IsHom 0 1) : GAlg B

A length-graded algebra (with 1 in degree 0) as a graded algebra.

theorem MultiplicativeBasisDeformations.MeshWalk.one_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)) : (lenA0 D hfin).IsHom 0 1

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.galgA0 {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)) : GExt.GAlg (CatAlg.Alg D.F0)ᵐᵒᵖ

A₀ as a graded algebra.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.Nb {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) : ℕ

The degree bound of the mesh category.

theorem MultiplicativeBasisDeformations.MeshWalk.Nb_spec {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} (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (d : ℕ) (x y : V) : Nb hfin ≤ d → ScalarMeshCategory.degreePart c d x y = ⊥

noncomputable def MultiplicativeBasisDeformations.MeshWalk.repProj {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) (d : ℕ) (X : V) : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

Degree projection on an evaluated module.

theorem MultiplicativeBasisDeformations.MeshWalk.repProj_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) (d : ℕ) (X : V) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (y : D.PV) : (repProj D d X) m y = (ScalarMeshCategory.degProj c d (↑y) X) (m y)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.zgrEv {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.ZGr (CatAlg.Rep D.F0 (meshFam Q c X))

The grading of the evaluated module M_X.

theorem MultiplicativeBasisDeformations.MeshWalk.zgrEv_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)) (X : V) (d : ℕ) (m : CatAlg.Rep D.F0 (meshFam Q c X)) : (zgrEv D hfin X).IsHom (↑d) m ↔ ∀ (y : D.PV), m y ∈ ScalarMeshCategory.degreePart c d (↑y) X

theorem MultiplicativeBasisDeformations.MeshWalk.zgrEv_isHom_neg {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) {p : ℤ} (hp : p < 0) (m : CatAlg.Rep D.F0 (meshFam Q c X)) : (zgrEv D hfin X).IsHom p m ↔ m = 0

theorem MultiplicativeBasisDeformations.MeshWalk.galgA0_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)) (d : ℕ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (galgA0 D hfin).gr.IsHom (↑d) a ↔ ∀ (y z : D.PV), MulOpposite.unop a y z ∈ ScalarMeshCategory.degreePart c d ↑y ↑z

theorem MultiplicativeBasisDeformations.MeshWalk.galgA0_isHom_neg {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)) {p : ℤ} (hp : p < 0) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (galgA0 D hfin).gr.IsHom p a ↔ a = 0

noncomputable def MultiplicativeBasisDeformations.MeshWalk.evAct {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) : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The right A₀-action m·a = a.unop • m.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.gmodEv {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) (CatAlg.Rep D.F0 (meshFam Q c X))

The evaluated module M_X as a graded right A₀-module.

Graded maps between evaluated modules

theorem MultiplicativeBasisDeformations.MeshWalk.degreePart_zero_ne {k : Type u} [Field k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {x y : V} (hxy : x ≠ y) {f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y} (hf : f ∈ ScalarMeshCategory.degreePart c 0 x y) : f = 0

theorem MultiplicativeBasisDeformations.MeshWalk.degProj_comp_left {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} (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {p r : ℕ} {y x z : V} {g : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c x} (hg : g ∈ ScalarMeshCategory.degreePart c p y x) (f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c z) : (ScalarMeshCategory.degProj c (p + r) y z) (CategoryTheory.CategoryStruct.comp g f) = CategoryTheory.CategoryStruct.comp g ((ScalarMeshCategory.degProj c r x z) f)

theorem MultiplicativeBasisDeformations.MeshWalk.comp_repMap_nat {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 Y : V) (r : ℕ) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : (zgrEv D hfin X).comp (zgrEv D hfin Y) (↑r) (↑k (CatAlg.repMap f)) = ↑k (CatAlg.repMap ((ScalarMeshCategory.degProj c r X Y) f))

The degree-r component of an evaluated morphism.

theorem MultiplicativeBasisDeformations.MeshWalk.comp_repMap_neg {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 Y : V) {r : ℤ} (hr : r < 0) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : (zgrEv D hfin X).comp (zgrEv D hfin Y) r (↑k (CatAlg.repMap f)) = 0

noncomputable def MultiplicativeBasisDeformations.MeshWalk.toAlgLin {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 Y : V} (u : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)) (hu : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), u (((evAct D X) m) a) = ((evAct D Y) (u m)) a) : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[CatAlg.Alg D.F0] CatAlg.Rep D.F0 (meshFam Q c Y)

An A₀-linear map between evaluated modules, as an Alg F₀-linear map.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_repMap {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 Y : V} (u : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)) (hu : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), u (((evAct D X) m) a) = ((evAct D Y) (u m)) a) : ∃ (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y), u = ↑k (CatAlg.repMap f)

theorem MultiplicativeBasisDeformations.MeshWalk.hom_comp_neg {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} (u : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)) (hu : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), u (((evAct D X) m) a) = ((evAct D Y) (u m)) a) {r : ℤ} (hr : r < 0) : (zgrEv D hfin X).comp (zgrEv D hfin Y) r u = 0

Hom_{A₀}(M_X, M_Y)_r = 0 for r < 0 (eq:normalized-hom-degrees).

theorem MultiplicativeBasisDeformations.MeshWalk.hom_comp_zero_ne {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} (hXY : X ≠ Y) (u : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)) (hu : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), u (((evAct D X) m) a) = ((evAct D Y) (u m)) a) : (zgrEv D hfin X).comp (zgrEv D hfin Y) 0 u = 0

Hom_{A₀}(M_X, M_Y)_0 = 0 for X ≠ Y.

theorem MultiplicativeBasisDeformations.MeshWalk.hom_comp_zero_self {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 : V} (u : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)) (hu : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), u (((evAct D X) m) a) = ((evAct D X) (u m)) a) : ∃ (t : k), (zgrEv D hfin X).comp (zgrEv D hfin X) 0 u = t • LinearMap.id

Hom_{A₀}(M_X, M_X)_0 = k.