Homogeneous components of composites in kQ #
Composition with a homogeneous morphism of degree m shifts homogeneous
components by m. Together with the finiteness of the decomposition into
components, this reduces statements about the mesh sequences of C(Q, c) to
homogeneous families (graded-category.tex).
theorem
MultiplicativeBasisDeformations.LinearPaths.proj_comp_of_mem
{k : Type u}
[Field k]
{V : Type v}
[Quiver V]
{m d : ℕ}
{x y z : V}
(F : obj x ⟶ obj y)
{G : obj y ⟶ obj z}
(hG : G ∈ degreePart m y z)
:
theorem
MultiplicativeBasisDeformations.LinearPaths.proj_comp_of_mem_lt
{k : Type u}
[Field k]
{V : Type v}
[Quiver V]
{m e : ℕ}
{x y z : V}
(F : obj x ⟶ obj y)
{G : obj y ⟶ obj z}
(hG : G ∈ degreePart m y z)
(he : e < m)
:
(proj e x z) (CategoryTheory.CategoryStruct.comp F G) = 0
theorem
MultiplicativeBasisDeformations.LinearPaths.proj_of_mem_comp
{k : Type u}
[Field k]
{V : Type v}
[Quiver V]
{m d : ℕ}
{x y z : V}
{G : obj x ⟶ obj y}
(hG : G ∈ degreePart m x y)
(F : obj y ⟶ obj z)
:
theorem
MultiplicativeBasisDeformations.LinearPaths.proj_of_mem_comp_lt
{k : Type u}
[Field k]
{V : Type v}
[Quiver V]
{m e : ℕ}
{x y z : V}
{G : obj x ⟶ obj y}
(hG : G ∈ degreePart m x y)
(F : obj y ⟶ obj z)
(he : e < m)
:
(proj e x z) (CategoryTheory.CategoryStruct.comp G F) = 0
theorem
MultiplicativeBasisDeformations.LinearPaths.eq_sum_proj_of_le
{k : Type u}
[Field k]
{V : Type v}
[Quiver V]
{x y : V}
(f : obj x ⟶ obj y)
:
∃ (N : ℕ), ∀ (M : ℕ), N ≤ M → f = ∑ d ∈ Finset.range M, (proj d x y) f
The decomposition into homogeneous components may use any long enough range of degrees.
theorem
MultiplicativeBasisDeformations.LinearPaths.exists_sum_proj_family
{k : Type u}
[Field k]
{V : Type v}
[Quiver V]
{α : Type u_1}
[Fintype α]
{x y : α → V}
(f : (a : α) → obj (x a) ⟶ obj (y a))
:
∃ (N : ℕ), ∀ (a : α), f a = ∑ d ∈ Finset.range N, (proj d (x a) (y a)) (f a)
A uniform range of degrees for a finite family.