Mesh data of the lifted modules (toward Corollary 12.1)

The lifted mesh sequences 0 → M_{τx}^B → ⊕_a M_{y_a}^B → M_x^B → 0 are exact sequences of right B-modules (LiftedMesh.lean); applying Hom_B(M_w^B, −) and Hom_B(−, M_w^B) gives the exactness required of a MeshData on the lifted modules (meshB), with the radical of localB (filtration order at least one).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.kd {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (hx : ¬D.proj x) : KerData Ls J h1 Vx x hx

The chosen lifted kernel at a nonprojective label.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.pB {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (a : D.Mid x) : FB Ls (D.mid x a) ⟶ FB Ls x

The lifted arrow map as a morphism of right B-modules.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.qB {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (hx : ¬D.proj x) (a : D.Mid x) : FB Ls (D.tau x hx) ⟶ FB Ls (D.mid x a)

The components of the lifted kernel as morphisms.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.joinIn {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) {w x : V} (g : (a : D.Mid x) → FB Ls w ⟶ FB Ls (D.mid x a)) : CatAlg.Rep D.F0 (meshFam Q c w) →ₗ[k] Emid D x

The components of a family of maps into the middle term, as one map.

theorem MultiplicativeBasisDeformations.MeshWalk.πB_joinIn {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) {w x : V} (g : (a : D.Mid x) → FB Ls w ⟶ FB Ls (D.mid x a)) : πB Ls J h1 Vx x ∘ₗ joinIn Ls g = toLin (∑ a : D.Mid x, CategoryTheory.CategoryStruct.comp (g a) (pB Ls J h1 Vx x a))

theorem MultiplicativeBasisDeformations.MeshWalk.joinIn_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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) {w x : V} (g : (a : D.Mid x) → FB Ls w ⟶ FB Ls (D.mid x a)) (m : CatAlg.Rep D.F0 (meshFam Q c w)) (b : B) : (joinIn Ls g) (((Ls.L w).act m) b) = ((LE Ls x).act ((joinIn Ls g) m)) b

noncomputable def MultiplicativeBasisDeformations.MeshWalk.joinOut {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) {w x : V} (v : (a : D.Mid x) → FB Ls (D.mid x a) ⟶ FB Ls w) : Emid D x →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c w)

A family of maps out of the middle term, as one map.

theorem MultiplicativeBasisDeformations.MeshWalk.joinOut_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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) {w x : V} (v : (a : D.Mid x) → FB Ls (D.mid x a) ⟶ FB Ls w) (e : Emid D x) (b : B) : (joinOut Ls v) (((LE Ls x).act e) b) = ((Ls.L w).act ((joinOut Ls v) e)) b

noncomputable def MultiplicativeBasisDeformations.MeshWalk.meshB {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (hrad : ∀ (x y : V) (d : ℕ), 1 ≤ d → ∀ f ∈ ScalarMeshCategory.degreePart c d x y, f ∈ L.rad x y) : CatAlg.MeshData (FB Ls) (localB Ls Vx)

The mesh data of the lifted modules.

Dimensions of the lifted Hom spaces

theorem MultiplicativeBasisDeformations.MeshWalk.exists_lead {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) {X Y : V} (r : ℕ) (f : FB Ls X ⟶ FB Ls Y) (hf : GExt.OrderGe (gmodEv D hfin X) (gmodEv D hfin Y) (↑r) (toLin f)) : ∃ φ ∈ ScalarMeshCategory.degreePart c r X Y, (gmodEv D hfin X).gr.comp (gmodEv D hfin Y).gr (↑r) (toLin f) = rs D φ

The leading term of a map of order r is a morphism of C of degree r.

def MultiplicativeBasisDeformations.MeshWalk.filB {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (X Y : V) (r : ℕ) : Submodule k (FB Ls X ⟶ FB Ls Y)

The filtration of the lifted Hom space by order.

theorem MultiplicativeBasisDeformations.MeshWalk.finrank_filB_step {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (X Y : V) (r : ℕ) : Module.finrank k ↥(filB Ls X Y r) = Module.finrank k ↥(filB Ls X Y (r + 1)) + Module.finrank k ↥(ScalarMeshCategory.degreePart c r X Y)

theorem MultiplicativeBasisDeformations.MeshWalk.finrank_FB_eq_sum {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (X Y : V) (R : ℕ) (hR : ↑(GExt.degBound (gmodEv D hfin X).gr) + ↑(GExt.degBound (gmodEv D hfin Y).gr) < ↑R) : Module.finrank k (FB Ls X ⟶ FB Ls Y) = ∑ r ∈ Finset.range R, Module.finrank k ↥(ScalarMeshCategory.degreePart c r X Y)

theorem MultiplicativeBasisDeformations.MeshWalk.finrank_C_eq_sum {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (X Y : V) (R : ℕ) (hR : Nb hfin ≤ R) : Module.finrank k (ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) = ∑ r ∈ Finset.range R, Module.finrank k ↥(ScalarMeshCategory.degreePart c r X Y)

theorem MultiplicativeBasisDeformations.MeshWalk.finrank_FB {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (X Y : V) : Module.finrank k (FB Ls X ⟶ FB Ls Y) = Module.finrank k (meshFam Q c X ⟶ meshFam Q c Y)

The lifted Hom spaces have the dimensions of C.