Gradings of mesh categories by path weights #
For the covering formula eq:walk-hom-sum (scalar-normalization.tex):
"Paths lift uniquely from a chosen starting vertex. Contextual mesh relations
lift uniquely as well: all terms of a mesh have the same lifted endpoints […]
The relation ideal therefore decomposes by lifted endpoints, just as the path
spaces do."
A path weight assigns to each path an element of a monoid, multiplicatively.
When all terms of each mesh relation have the same weight, the mesh ideal is
homogeneous and the Hom spaces of C(Q, c) are the internal direct sums of
their weight parts (iSupIndep_wPart, iSup_wPart), compatibly with
composition (comp_mem_wPart). For the walk-class weight of the cover
(DeckGrading.lean) the weight part of degree g is the space
C̃(X̃, gỸ).
structure
MultiplicativeBasisDeformations.PathWeight
(V : Type v)
[Quiver V]
(G : Type u')
[Monoid G]
:
Type (max (max u' v) w)
A multiplicative weight on the paths of a quiver.
- deg {x y : V} : Quiver.Path x y → G
- deg_nil (x : V) : self.deg Quiver.Path.nil = 1
Instances For
noncomputable def
MultiplicativeBasisDeformations.LinearPaths.wpart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{G : Type u'}
[Monoid G]
(wt : PathWeight V G)
(g : G)
(x y : V)
:
The weight-g part of kQ(x, y).
Instances For
def
MultiplicativeBasisDeformations.LinearPaths.wproj
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{G : Type u'}
[Monoid G]
[DecidableEq G]
(wt : PathWeight V G)
(g : G)
(x y : V)
:
The projection onto the weight-g part.
Instances For
theorem
MultiplicativeBasisDeformations.LinearPaths.path_mem_wpart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
{x y : V}
(p : Quiver.Path x y)
:
theorem
MultiplicativeBasisDeformations.LinearPaths.wproj_path
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
{x y : V}
(g : G)
(p : Quiver.Path x y)
:
theorem
MultiplicativeBasisDeformations.LinearPaths.wproj_of_mem
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
{g h : G}
{x y : V}
{f : obj x ⟶ obj y}
(hf : f ∈ wpart wt h x y)
:
(wproj wt g x y) f = if h = g then f else 0
theorem
MultiplicativeBasisDeformations.LinearPaths.wproj_mem
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
{g : G}
{x y : V}
(f : obj x ⟶ obj y)
:
theorem
MultiplicativeBasisDeformations.LinearPaths.eq_sum_wproj
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
{x y : V}
(f : obj x ⟶ obj y)
:
∃ (s : Finset G), f = ∑ g ∈ s, (wproj wt g x y) f
A morphism of kQ is the sum of its weight components, over a finite set of
weights.
theorem
MultiplicativeBasisDeformations.LinearPaths.comp_mem_wpart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
{g h : G}
{x y z : V}
{f : obj x ⟶ obj y}
{f' : obj y ⟶ obj z}
(hf : f ∈ wpart wt g x y)
(hf' : f' ∈ wpart wt h y z)
:
CategoryTheory.CategoryStruct.comp f f' ∈ wpart wt (g * h) x z
theorem
MultiplicativeBasisDeformations.LinearPaths.wproj_mem_linearSpan
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(R : (X Y : LinearPaths k V) → Set (X ⟶ Y))
(hR : ∀ (X Y : V), ∀ r ∈ R X Y, ∃ (e : G), r ∈ wpart wt e X Y)
(g : G)
{X Y : V}
{f : obj X ⟶ obj Y}
(hf : f ∈ (CategoricalIdeal.HomIdeal.linearSpan k R).hom (obj X) (obj Y))
:
(wproj wt g X Y) f ∈ (CategoricalIdeal.HomIdeal.linearSpan k R).hom (obj X) (obj Y)
An ideal generated by weight-homogeneous relations is stable under the weight projections.
def
MultiplicativeBasisDeformations.ScalarMeshCategory.MeshHomogeneous
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
{G : Type u'}
[Monoid G]
(wt : PathWeight V G)
:
All terms of every mesh have the same weight.
Instances For
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.meshRelation_mem_wpart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(hw : MeshHomogeneous wt)
(x : ↑Q.nonprojective)
:
∃ (e : G), meshRelation c x ∈ LinearPaths.wpart wt e ↑(Q.tau x) ↑x
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.meshRelations_wHomogeneous
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(hw : MeshHomogeneous wt)
(X Y : V)
(r : LinearPaths.obj X ⟶ LinearPaths.obj Y)
(hr : r ∈ meshRelations c (LinearPaths.obj X) (LinearPaths.obj Y))
:
∃ (e : G), r ∈ LinearPaths.wpart wt e X Y
noncomputable def
MultiplicativeBasisDeformations.ScalarMeshCategory.wPart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
{G : Type u'}
[Monoid G]
(wt : PathWeight V G)
(g : G)
(x y : V)
:
The weight-g part of C(x, y).
Instances For
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.pathMor_mem_wPart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
{x y : V}
(p : Quiver.Path x y)
:
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.ker_quotL_le_w
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(hw : MeshHomogeneous wt)
(g : G)
(x y : V)
:
(quotL c x y).ker ≤ (quotL c x y ∘ₗ LinearPaths.wproj wt g x y).ker
noncomputable def
MultiplicativeBasisDeformations.ScalarMeshCategory.wProj
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
{G : Type u'}
[Monoid G]
[DecidableEq G]
(wt : PathWeight V G)
(hw : MeshHomogeneous wt)
(g : G)
(x y : V)
:
The weight-g projection on the Hom spaces of C(Q, c).
Instances For
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.wProj_apply
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(hw : MeshHomogeneous wt)
(g : G)
{x y : V}
(F : LinearPaths.obj x ⟶ LinearPaths.obj y)
:
(wProj c wt hw g x y) ((RelationCategory.functor k (meshRelations c)).map F) = (RelationCategory.functor k (meshRelations c)).map ((LinearPaths.wproj wt g x y) F)
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.wProj_of_mem
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(hw : MeshHomogeneous wt)
{g h : G}
{x y : V}
{f : obj c x ⟶ obj c y}
(hf : f ∈ wPart c wt h x y)
:
(wProj c wt hw g x y) f = if h = g then f else 0
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.wProj_mem
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(hw : MeshHomogeneous wt)
(g : G)
{x y : V}
(f : obj c x ⟶ obj c y)
:
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.iSupIndep_wPart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(hw : MeshHomogeneous wt)
(x y : V)
:
iSupIndep fun (g : G) => wPart c wt g x y
The covering formula, independence: the weight parts are independent.
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.eq_sum_wProj
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(hw : MeshHomogeneous wt)
{x y : V}
(f : obj c x ⟶ obj c y)
:
∃ (s : Finset G), f = ∑ g ∈ s, (wProj c wt hw g x y) f
A morphism is the sum of its weight components, over a finite set of weights.
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.iSup_wPart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
(hw : MeshHomogeneous wt)
(x y : V)
:
⨆ (g : G), wPart c wt g x y = ⊤
The covering formula, spanning.
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.comp_mem_wPart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{G : Type u'}
[Monoid G]
[DecidableEq G]
{wt : PathWeight V G}
{g h : G}
{x y z : V}
{f : obj c x ⟶ obj c y}
{f' : obj c y ⟶ obj c z}
(hf : f ∈ wPart c wt g x y)
(hf' : f' ∈ wPart c wt h y z)
:
CategoryTheory.CategoryStruct.comp f f' ∈ wPart c wt (g * h) x z