The category of lifted modules (toward Corollary 12.1)

The filtered lifts M_X^B of the evaluated modules as right B-modules (FB), with B-linear maps identified with filtered maps of the underlying graded spaces (toLin, ofLin). The maps of filtration order at least one form the radical of a local family (Proposition 6.5(3): "the map-degree filtration has nilpotent positive part, and its degree-zero part is a product of copies of k").

def MultiplicativeBasisDeformations.MeshWalk.LMod {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)} {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (_Ls : Lifts D hfin P) (X : V) : Type u

The underlying space of the lifted module M_X^B.

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.MeshWalk.instAddCommGroupLMod {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)} {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (X : V) : AddCommGroup (LMod Ls X)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.MeshWalk.instModuleMulOppositeLMod {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)} {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (X : V) : Module Bᵐᵒᵖ (LMod Ls X)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.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)} {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (X : V) : RightModuleCat B

The lifted module M_X^B as a right B-module.

theorem MultiplicativeBasisDeformations.MeshWalk.smul_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) (X : V) (t : k) (m : CatAlg.Rep D.F0 (meshFam Q c X)) : t • m = ((Ls.L X).act m) ((algebraMap k B) t)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.toLin {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} (f : FB Ls X ⟶ FB Ls Y) : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)

A B-linear map of lifts, as a k-linear map of the graded spaces.

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_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} {X Y : V} (f : FB Ls X ⟶ FB Ls Y) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (b : B) : (toLin f) (((Ls.L X).act m) b) = ((Ls.L Y).act ((toLin f) m)) b

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ofLin {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)} {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) {X Y : V} (g : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)) (hg : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c X)) (b : B), g (((Ls.L X).act m) b) = ((Ls.L Y).act (g m)) b) : FB Ls X ⟶ FB Ls Y

A B-linear k-linear map of the graded spaces, as a map of lifts.

@[simp]

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_ofLin {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} (g : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)) (hg : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c X)) (b : B), g (((Ls.L X).act m) b) = ((Ls.L Y).act (g m)) b) : toLin (ofLin Ls g hg) = g

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_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} {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} : Function.Injective toLin

@[simp]

theorem MultiplicativeBasisDeformations.MeshWalk.ofLin_toLin {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} (f : FB Ls X ⟶ FB Ls Y) : ofLin Ls (toLin f) ⋯ = f

@[simp]

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_comp {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 Z : V} (f : FB Ls X ⟶ FB Ls Y) (g : FB Ls Y ⟶ FB Ls Z) : toLin (CategoryTheory.CategoryStruct.comp f g) = toLin g ∘ₗ toLin f

@[simp]

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_id {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 : V) : toLin (CategoryTheory.CategoryStruct.id (FB Ls X)) = LinearMap.id

@[simp]

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_add {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} (f f' : FB Ls X ⟶ FB Ls Y) : toLin (f + f') = toLin f + toLin f'

@[simp]

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_zero {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} : toLin 0 = 0

@[simp]

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} {Ls : Lifts D hfin P} {X Y : V} (f : FB Ls X ⟶ FB Ls Y) : toLin (-f) = -toLin f

@[simp]

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_sub {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} (f f' : FB Ls X ⟶ FB Ls Y) : toLin (f - f') = toLin f - toLin f'

@[simp]

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_smul {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} (t : k) (f : FB Ls X ⟶ FB Ls Y) : toLin (t • f) = t • toLin f

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_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} {X Y : V} {ι : Type u_1} (s : Finset ι) (f : ι → (FB Ls X ⟶ FB Ls Y)) : toLin (∑ i ∈ s, f i) = ∑ i ∈ s, toLin (f i)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.toLinL {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) : (FB Ls X ⟶ FB Ls Y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)

toLin as a k-linear map.

instance MultiplicativeBasisDeformations.MeshWalk.finiteDimensional_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} (X Y : V) : FiniteDimensional k (FB Ls X ⟶ FB Ls Y)

The radical of the lifted category

theorem MultiplicativeBasisDeformations.MeshWalk.hneg {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) (r : ℤ) : r < 0 → ∀ (f : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)), (∀ (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), f (((gmodEv D hfin X).act m) a) = ((gmodEv D hfin Y).act (f m)) a) → (∀ (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c X)), (gmodEv D hfin X).gr.IsHom p m → (gmodEv D hfin Y).gr.IsHom (p + r) (f m)) → f = 0

Hom_{A₀}(M_X, M_Y)_r = 0 for r < 0, in the form used by Proposition 6.5(3).

theorem MultiplicativeBasisDeformations.MeshWalk.order0 {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} (f : FB Ls X ⟶ FB Ls Y) : GExt.OrderGe (gmodEv D hfin X) (gmodEv D hfin Y) 0 (toLin f)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_lead0 {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} (f : FB Ls X ⟶ FB Ls Y) : ∃ φ ∈ ScalarMeshCategory.degreePart c 0 X Y, (gmodEv D hfin X).gr.comp (gmodEv D hfin Y).gr 0 (toLin f) = rs D φ

The leading term of a map of lifts is a morphism of C of degree zero.

theorem MultiplicativeBasisDeformations.MeshWalk.rs_id {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) : rs D (CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c X)) = LinearMap.id

theorem MultiplicativeBasisDeformations.MeshWalk.comp_id0 {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) : (gmodEv D hfin X).gr.comp (gmodEv D hfin X).gr 0 LinearMap.id = LinearMap.id

def MultiplicativeBasisDeformations.MeshWalk.radB {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) : Submodule k (FB Ls X ⟶ FB Ls Y)

The radical of the lifted category: maps of filtration order at least one.

theorem MultiplicativeBasisDeformations.MeshWalk.toLin_pow {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 : V} (f : CategoryTheory.End (FB Ls X)) (n : ℕ) : toLin (f ^ n) = toLin f ^ n

theorem MultiplicativeBasisDeformations.MeshWalk.nontrivial_rep {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) : Nontrivial (CatAlg.Rep D.F0 (meshFam Q c x))

theorem MultiplicativeBasisDeformations.MeshWalk.prod_order {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) (l : List (CatAlg.Alg (FB Ls))) (hl : ∀ a ∈ l, ∀ (y z : V), a y z ∈ radB Ls y z) (y z : V) : GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin z) (↑l.length) (toLin (l.prod y z))

def MultiplicativeBasisDeformations.MeshWalk.localB {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) : CatAlg.LocalFamily (FB Ls)

The local family of the lifted modules (Proposition 6.5(3)).