The path-length grading of a scalar mesh category

graded-category.tex: "The quotient is graded by path length." The mesh relations are homogeneous, so the degree projections of kQ descend to C(Q, c) and its degree parts are independent (iSupIndep_degreePart). If C(Q, c) is finite-dimensional, only finitely many degree parts are nonzero, so all sufficiently long paths vanish (exists_pathMor_eq_zero); this is the first step of the proof of Proposition 4.1 (periodic-mesh-calculations.tex).

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.quotL {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x y : V) : (LinearPaths.obj x ⟶ LinearPaths.obj y) →ₗ[k] (RelationCategory.functor k (meshRelations c)).obj (LinearPaths.obj x) ⟶ (RelationCategory.functor k (meshRelations c)).obj (LinearPaths.obj y)

The quotient map kQ(x, y) → C(x, y).

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.quotL_surjective {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x y : V) : Function.Surjective ⇑(quotL c x y)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.ker_quotL_le {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (d : ℕ) (x y : V) : (quotL c x y).ker ≤ (quotL c x y ∘ₗ LinearPaths.proj d x y).ker

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.degProj {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (d : ℕ) (x y : V) : (obj c x ⟶ obj c y) →ₗ[k] obj c x ⟶ obj c y

The degree-d projection on the Hom spaces of C(Q, c).

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.degProj_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) (d : ℕ) {x y : V} (F : LinearPaths.obj x ⟶ LinearPaths.obj y) : (degProj c d x y) ((RelationCategory.functor k (meshRelations c)).map F) = (RelationCategory.functor k (meshRelations c)).map ((LinearPaths.proj d x y) F)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.iSupIndep_degreePart {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x y : V) : iSupIndep fun (d : ℕ) => degreePart c d x y

The degree parts of the Hom spaces of C(Q, c) are independent.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.exists_pathMor_eq_zero {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Finite V] (hfin : ∀ (x y : V), FiniteDimensional k (obj c x ⟶ obj c y)) : ∃ (N : ℕ), ∀ (x y : V) (p : Quiver.Path x y), N ≤ p.length → pathMor c p = 0

In a finite-dimensional scalar mesh category on a finite quiver, all sufficiently long paths vanish.