The path-length grading of a linear path category #
The linear path category kQ = Free k (Paths Q) is graded by path length:
every morphism is the finite sum of its homogeneous components, and
composition adds degrees (graded-category.tex: "The quotient is
graded by path length").
@[simp]
theorem
MultiplicativeBasisDeformations.LinearPaths.toFinsupp_zero
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{x y : V}
:
toFinsupp 0 = 0
theorem
MultiplicativeBasisDeformations.LinearPaths.path_mem_degreePart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{x y : V}
(p : Quiver.Path x y)
:
path p ∈ degreePart p.length x y
theorem
MultiplicativeBasisDeformations.LinearPaths.induction_on
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{x y : V}
{P : (obj x ⟶ obj y) → Prop}
(f : obj x ⟶ obj y)
(h0 : P 0)
(hadd : ∀ (f g : obj x ⟶ obj y), P f → P g → P (f + g))
(hsingle : ∀ (p : Quiver.Path x y) (c : k), P (c • path p))
:
P f
Every morphism of kQ is a finite linear combination of paths.
theorem
MultiplicativeBasisDeformations.LinearPaths.mem_degreePart_iff
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{d : ℕ}
{x y : V}
(f : obj x ⟶ obj y)
:
f ∈ degreePart d x y ↔ (proj d x y) f = f
theorem
MultiplicativeBasisDeformations.LinearPaths.proj_mem
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{d : ℕ}
{x y : V}
(f : obj x ⟶ obj y)
:
(proj d x y) f ∈ degreePart d x y
theorem
MultiplicativeBasisDeformations.LinearPaths.proj_of_mem
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{d e : ℕ}
{x y : V}
{f : obj x ⟶ obj y}
(hf : f ∈ degreePart e x y)
:
(proj d x y) f = if e = d then f else 0
theorem
MultiplicativeBasisDeformations.LinearPaths.comp_mem_degreePart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{d e : ℕ}
{x y z : V}
{f : obj x ⟶ obj y}
{g : obj y ⟶ obj z}
(hf : f ∈ degreePart d x y)
(hg : g ∈ degreePart e y z)
:
CategoryTheory.CategoryStruct.comp f g ∈ degreePart (d + e) x z
theorem
MultiplicativeBasisDeformations.LinearPaths.proj_mem_linearSpan
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
(R : (X Y : LinearPaths k V) → Set (X ⟶ Y))
(hR : ∀ (X Y : V), ∀ r ∈ R X Y, ∃ (e : ℕ), r ∈ degreePart e X Y)
(d : ℕ)
{X Y : V}
{f : obj X ⟶ obj Y}
(hf : f ∈ (CategoricalIdeal.HomIdeal.linearSpan k R).hom (obj X) (obj Y))
:
(proj d X Y) f ∈ (CategoricalIdeal.HomIdeal.linearSpan k R).hom (obj X) (obj Y)
An ideal generated by homogeneous relations is graded: it is stable under the homogeneous projections.
theorem
MultiplicativeBasisDeformations.LinearPaths.exists_lastArrow_decomposition
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
[DecidableEq V]
[(x y : V) → DecidableEq (x ⟶ y)]
{N : ℕ}
{W Y : V}
[Fintype ((X : V) × (X ⟶ Y))]
{F : obj W ⟶ obj Y}
(hF : F ∈ degreePart (N + 1) W Y)
:
∃ (G : (a : (X : V) × (X ⟶ Y)) → obj W ⟶ obj a.fst),
(∀ (a : (X : V) × (X ⟶ Y)), G a ∈ degreePart N W a.fst) ∧ F = ∑ a : (X : V) × (X ⟶ Y), CategoryTheory.CategoryStruct.comp (G a) (arrow a.snd)
A homogeneous morphism of positive degree is a sum over the arrows ending
at its target: F = ∑_a G_a a with G_a homogeneous of one degree less.
theorem
MultiplicativeBasisDeformations.LinearPaths.degreePart_zero_of_ne
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{x y : V}
(hxy : x ≠ y)
{F : obj x ⟶ obj y}
(hF : F ∈ degreePart 0 x y)
:
F = 0
A homogeneous morphism of degree zero between distinct vertices vanishes.
theorem
MultiplicativeBasisDeformations.LinearPaths.degreePart_zero_self
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{x : V}
{F : obj x ⟶ obj x}
(hF : F ∈ degreePart 0 x x)
:
A homogeneous endomorphism of degree zero is a multiple of the trivial path.
theorem
MultiplicativeBasisDeformations.LinearPaths.arrow_mem_degreePart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{x y : V}
(a : x ⟶ y)
:
arrow a ∈ degreePart 1 x y
theorem
MultiplicativeBasisDeformations.LinearPaths.comp_arrow_mem_degreePart
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{m : ℕ}
{x y z : V}
{H : obj x ⟶ obj y}
(hH : H ∈ degreePart m x y)
(a : y ⟶ z)
:
CategoryTheory.CategoryStruct.comp H (arrow a) ∈ degreePart (m + 1) x z
theorem
MultiplicativeBasisDeformations.meshRelation_mem_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 : ↑Q.nonprojective)
:
meshRelation c x ∈ LinearPaths.degreePart 2 ↑(Q.tau x) ↑x
The mesh relations are homogeneous of degree two.
theorem
MultiplicativeBasisDeformations.meshRelations_homogeneous
{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)
(r : LinearPaths.obj X ⟶ LinearPaths.obj Y)
(hr : r ∈ meshRelations c (LinearPaths.obj X) (LinearPaths.obj Y))
:
∃ (e : ℕ), r ∈ LinearPaths.degreePart e X Y