Mesh-weight gradings of A₀ and of its evaluated modules #
weights-and-parameters.tex: "a mesh weight w grades V_{m+1}(C) by giving a
path at row v the weight w(path) − ν_v, and grades U_m(C) …", and
weights-and-parameters.tex: "Lift a basis of the integer ray weights to mesh
weights using Lemma 7.4. These give simultaneous gradings on the lifted modules."
A mesh weight W with values in an abelian group M is a path weight for which all
meshes are homogeneous (MeshWt.homog), so it grades every Hom space of C (wπ),
compatibly with composition and with the length grading (wπ_degProj). It grades A₀
(grA0, latA0) and each evaluated module M_X (grEv); the action of a homogeneous
element of A₀, the arrow maps and all evaluated morphisms shift weights
(act_shift, fA_shift, rs_shift), and an evaluated morphism shifting by γ comes
from the weight-γ part of C (mem_wP_of_shift).
theorem
MultiplicativeBasisDeformations.MeshWalk.MeshWt.pw_comp
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{x y : V}
(p : Quiver.Path x y)
{z : V}
(q : Quiver.Path y z)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.MeshWt.pw_toPath
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{x y : V}
(a : x ⟶ y)
:
def
MultiplicativeBasisDeformations.MeshWalk.MeshWt.toPW
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
:
PathWeight V (Multiplicative M)
The path weight of a mesh weight, with values in Multiplicative M.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.MeshWt.toPW_deg
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{x y : V}
(p : Quiver.Path x y)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.MeshWt.homog
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
{M : Type}
[AddCommGroup M]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(W : MeshWt Q M)
:
Meshes are homogeneous for a mesh weight.
Weight parts of the Hom spaces of C #
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.MeshWalk.wP
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(g : M)
(x y : V)
:
Submodule k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)
The weight-g part of C(x, y).
Instances For
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.MeshWalk.wπ
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(g : M)
(x y : V)
:
(ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y) →ₗ[k] ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y
The weight-g projection of C(x, y).
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.wπ_mem
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(g : M)
{x y : V}
(f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.wπ_of_mem
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{g h : M}
{x y : V}
{f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hf : f ∈ wP c W h x y)
:
(wπ c W g x y) f = if h = g then f else 0
theorem
MultiplicativeBasisDeformations.MeshWalk.comp_mem_wP
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{g h : M}
{x y z : V}
{f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
{f' : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c z}
(hf : f ∈ wP c W g x y)
(hf' : f' ∈ wP c W h y z)
:
CategoryTheory.CategoryStruct.comp f f' ∈ wP c W (g + h) x z
theorem
MultiplicativeBasisDeformations.MeshWalk.pathMor_mem_wP
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{x y : V}
(p : Quiver.Path x y)
:
ScalarMeshCategory.pathMor c p ∈ wP c W (W.pw p) x y
theorem
MultiplicativeBasisDeformations.MeshWalk.arrowMor_mem_wP
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{x y : V}
(a : x ⟶ y)
:
ScalarMeshCategory.arrowMor c a ∈ wP c W (W.w a) x y
theorem
MultiplicativeBasisDeformations.MeshWalk.wπ_degProj
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(g : M)
(d : ℕ)
{x y : V}
(f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)
:
(wπ c W g x y) ((ScalarMeshCategory.degProj c d x y) f) = (ScalarMeshCategory.degProj c d x y) ((wπ c W g x y) f)
The weight and length projections commute.
theorem
MultiplicativeBasisDeformations.MeshWalk.wπ_mem_degreePart
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(g : M)
{d : ℕ}
{x y : V}
{f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hf : f ∈ ScalarMeshCategory.degreePart c d x y)
:
(wπ c W g x y) f ∈ ScalarMeshCategory.degreePart c d x y
theorem
MultiplicativeBasisDeformations.MeshWalk.finite_wP
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
(x y : V)
:
{g : M | wP c W g x y ≠ ⊥}.Finite
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.wSupp
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
:
Finset M
A finite set of weights containing all weights with nonzero parts.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.wP_eq_bot
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{g : M}
(hg : g ∉ wSupp W hfin)
(x y : V)
:
wP c W g x y = ⊥
theorem
MultiplicativeBasisDeformations.MeshWalk.wπ_out
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{g : M}
(hg : g ∉ wSupp W hfin)
(x y : V)
:
wπ c W g x y = 0
theorem
MultiplicativeBasisDeformations.MeshWalk.eq_sum_wπ
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{x y : V}
(f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.wπ_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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{β : M}
{x y z : V}
{u : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hu : u ∈ wP c W β x y)
(γ : M)
(f : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c z)
:
Composition with a homogeneous morphism on the left.
theorem
MultiplicativeBasisDeformations.MeshWalk.wπ_comp_right
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{β : M}
{x y z : V}
{u : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c z}
(hu : u ∈ wP c W β y z)
(γ : M)
(f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)
:
Composition with a homogeneous morphism on the right.
The grading of the evaluated modules #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.evProj
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
(g : M)
(X : V)
:
CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)
The weight projection of an evaluated module.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.evProj_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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
(g : M)
(X : V)
(m : CatAlg.Rep D.F0 (meshFam Q c X))
(y : D.PV)
:
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.grEv
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
(X : V)
:
MGr k M (CatAlg.Rep D.F0 (meshFam Q c X))
The mesh-weight grading of M_X.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.grEv_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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
{g : M}
{X : V}
{m : CatAlg.Rep D.F0 (meshFam Q c X)}
:
The grading of A₀ #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.a0Proj
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
(g : M)
:
(CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ
The weight projection of A₀.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.a0Proj_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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
(g : M)
(a : (CatAlg.Alg D.F0)ᵐᵒᵖ)
(p q : D.PV)
:
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.grA0
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
:
MGr k M (CatAlg.Alg D.F0)ᵐᵒᵖ
The mesh-weight grading of A₀ as a module grading.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.grA0_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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
{g : M}
{a : (CatAlg.Alg D.F0)ᵐᵒᵖ}
:
theorem
MultiplicativeBasisDeformations.MeshWalk.grA0_mul
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
{g h : M}
{a b : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(ha : (grA0 W hfin D).IsHom g a)
(hb : (grA0 W hfin D).IsHom h b)
:
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.latA0
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
:
LatGrading k (CatAlg.Alg D.F0)ᵐᵒᵖ M
The mesh-weight grading of A₀ as an algebra grading.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.latA0_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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
{g : M}
{a : (CatAlg.Alg D.F0)ᵐᵒᵖ}
:
Shifting maps #
theorem
MultiplicativeBasisDeformations.MeshWalk.act_shift
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
{α : M}
{a : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(ha : (grA0 W hfin D).IsHom α a)
(X : V)
:
The action of a homogeneous element of A₀ shifts weights.
theorem
MultiplicativeBasisDeformations.MeshWalk.rs_shift
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
{γ : M}
{X Y : V}
{f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y}
(hf : f ∈ wP c W γ X Y)
:
An evaluated homogeneous morphism shifts weights.
theorem
MultiplicativeBasisDeformations.MeshWalk.fA_shift
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
{X Y : V}
(a : X ⟶ Y)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.pr_rs
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
(γ : M)
{X Y : V}
(f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)
:
The weight part of an evaluated morphism.
theorem
MultiplicativeBasisDeformations.MeshWalk.mem_wP_of_shift
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{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)]
{γ : M}
{X Y : V}
{f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y}
(h : (grEv W hfin D X).Shift (grEv W hfin D Y) γ (rs D f))
:
f ∈ wP c W γ X Y
An evaluated morphism shifting by γ comes from the weight-γ part.
Compatibility with the length grading #
theorem
MultiplicativeBasisDeformations.MeshWalk.evProj_zgr
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{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)]
{g : M}
{X : V}
{p : ℤ}
{m : CatAlg.Rep D.F0 (meshFam Q c X)}
(hm : (zgrEv D hfin X).IsHom p m)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.a0Proj_zgr
{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}
{M : Type}
[AddCommGroup M]
(W : MeshWt Q M)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{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)]
{g : M}
{p : ℤ}
{a : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(ha : (galgA0 D hfin).gr.IsHom p a)
: