The path-length grading of a free linear category

The Hom space of the free linear category has its path basis. This file groups that basis by path length, proves that the resulting submodules form an internal direct sum, and proves that composition adds degrees.

def MagnitudeConjecture.GradedFinsupp.degreeComponent {k : Type u} [Field k] {P : Type z} (degree : P → ℕ) (n : ℕ) : Submodule k (P →₀ k)

The submodule of finitely supported functions supported in one fiber of a degree function.

theorem MagnitudeConjecture.GradedFinsupp.degreeComponent_iSupIndep {k : Type u} [Field k] {P : Type z} (degree : P → ℕ) : iSupIndep (degreeComponent degree)

theorem MagnitudeConjecture.GradedFinsupp.iSup_degreeComponent_eq_top {k : Type u} [Field k] {P : Type z} (degree : P → ℕ) : ⨆ (n : ℕ), degreeComponent degree n = ⊤

theorem MagnitudeConjecture.GradedFinsupp.degreeComponent_isInternal {k : Type u} [Field k] {P : Type z} (degree : P → ℕ) : DirectSum.IsInternal (degreeComponent degree)

Finitely supported functions decompose internally according to any natural-number-valued degree on their basis indices.

theorem MagnitudeConjecture.CategoricalGrading.comp_comp_mem {k : Type u} [Field k] {C : Type z} [CategoryTheory.Category.{w, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (A : (X Y : C) → ℕ → Submodule k (X ⟶ Y)) (hcomp : ∀ {W X Y : C} {i j : ℕ} {a : W ⟶ X} {b : X ⟶ Y}, a ∈ A W X i → b ∈ A X Y j → CategoryTheory.CategoryStruct.comp a b ∈ A W Y (i + j)) {W X Y Z : C} {i j l : ℕ} {a : W ⟶ X} {b : X ⟶ Y} {c : Y ⟶ Z} (ha : a ∈ A W X i) (hb : b ∈ A X Y j) (hc : c ∈ A Y Z l) : CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp b c) ∈ A W Z (i + j + l)

Binary degree compatibility implies the corresponding three-factor compatibility. This is kept generic so no concrete category implementation is unfolded while checking the associativity step.

noncomputable def MagnitudeConjecture.LinearPathCategory.lengthComponent {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (n : ℕ) : Submodule k (x ⟶ y)

The degree-n submodule of a Hom space in the free linear path category.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.mem_lengthComponent_iff {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (n : ℕ) (f : x ⟶ y) : f ∈ lengthComponent x y n ↔ ↑((homPathLinearEquiv x y) f).support ⊆ {p : Quiver.Path (vertex y) (vertex x) | p.length = n}

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.pathHom_mem_lengthComponent_iff {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y : Category k Q} (p : Quiver.Path (vertex y) (vertex x)) (n : ℕ) : pathHom p ∈ lengthComponent x y n ↔ p.length = n

theorem MagnitudeConjecture.LinearPathCategory.lengthComponent_eq_map {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (n : ℕ) : lengthComponent x y n = Submodule.map (↑(homPathLinearEquiv x y).symm) (GradedFinsupp.degreeComponent (fun (p : Quiver.Path (vertex y) (vertex x)) => p.length) n)

theorem MagnitudeConjecture.LinearPathCategory.lengthComponent_isInternal {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) : DirectSum.IsInternal (lengthComponent x y)

The path-length pieces form an internal direct-sum decomposition of every Hom space.

def MagnitudeConjecture.LinearPathCategory.lengthBasisSet {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (n : ℕ) : Set (x ⟶ y)

The path-basis elements of one fixed length.

theorem MagnitudeConjecture.LinearPathCategory.lengthComponent_eq_span {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (n : ℕ) : lengthComponent x y n = Submodule.span k (lengthBasisSet x y n)

theorem MagnitudeConjecture.LinearPathCategory.comp_mem_lengthComponent {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y z : Category k Q} {i j : ℕ} {f : x ⟶ y} {g : y ⟶ z} (hf : f ∈ lengthComponent x y i) (hg : g ∈ lengthComponent y z j) : CategoryTheory.CategoryStruct.comp f g ∈ lengthComponent x z (i + j)

Composition in the free linear path category adds path length.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.id_mem_lengthComponent_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x : Category k Q) : CategoryTheory.CategoryStruct.id x ∈ lengthComponent x x 0

theorem MagnitudeConjecture.LinearPathCategory.lengthComponent_zero_eq_bot_of_vertex_ne {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y : Category k Q} (hxy : vertex y ≠ vertex x) : lengthComponent x y 0 = ⊥

Between distinct vertices there is no degree-zero morphism.

theorem MagnitudeConjecture.LinearPathCategory.lengthComponent_zero_self {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x : Category k Q) : lengthComponent x x 0 = k ∙ CategoryTheory.CategoryStruct.id x

At one vertex the degree-zero endomorphisms are exactly the scalar multiples of the identity.

noncomputable def MagnitudeConjecture.LinearPathCategory.lengthTail {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (n : ℕ) : Submodule k (x ⟶ y)

The submodule spanned by paths of length at least n. This is the decreasing path-length filtration on the free linear category.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.mem_lengthTail_iff {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (n : ℕ) (f : x ⟶ y) : f ∈ lengthTail x y n ↔ ↑((homPathLinearEquiv x y) f).support ⊆ {p : Quiver.Path (vertex y) (vertex x) | n ≤ p.length}

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.pathHom_mem_lengthTail_iff {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y : Category k Q} (p : Quiver.Path (vertex y) (vertex x)) (n : ℕ) : pathHom p ∈ lengthTail x y n ↔ n ≤ p.length

theorem MagnitudeConjecture.LinearPathCategory.lengthTail_eq_span {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (n : ℕ) : lengthTail x y n = Submodule.span k (pathHom '' {p : Quiver.Path (vertex y) (vertex x) | n ≤ p.length})

The path-length tail is the span of the corresponding path-basis elements.

theorem MagnitudeConjecture.LinearPathCategory.lengthTail_antitone {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) {m n : ℕ} (hmn : m ≤ n) : lengthTail x y n ≤ lengthTail x y m

Raising the cutoff shrinks the free path-length tail.

theorem MagnitudeConjecture.LinearPathCategory.comp_mem_lengthTail {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y z : Category k Q} {i j : ℕ} {f : x ⟶ y} {g : y ⟶ z} (hf : f ∈ lengthTail x y i) (hg : g ∈ lengthTail y z j) : CategoryTheory.CategoryStruct.comp f g ∈ lengthTail x z (i + j)

Composition adds lower bounds on path length.

noncomputable def MagnitudeConjecture.LinearPathCategory.positivePathSubmodule {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) : Submodule k (x ⟶ y)

The submodule spanned by nontrivial paths. Unlike a single homogeneous length component, this collects all strictly positive path lengths.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.mem_positivePathSubmodule_iff {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (f : x ⟶ y) : f ∈ positivePathSubmodule x y ↔ ↑((homPathLinearEquiv x y) f).support ⊆ {p : Quiver.Path (vertex y) (vertex x) | p.length ≠ 0}

theorem MagnitudeConjecture.LinearPathCategory.positivePathSubmodule_eq_span {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) : positivePathSubmodule x y = Submodule.span k (pathHom '' {p : Quiver.Path (vertex y) (vertex x) | p.length ≠ 0})

The positive-path submodule is the span of its path-basis elements.

theorem MagnitudeConjecture.LinearPathCategory.positivePathSubmodule_eq_top_of_vertex_ne {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y : Category k Q} (hxy : vertex y ≠ vertex x) : positivePathSubmodule x y = ⊤

Between distinct vertices every free linear morphism is a combination of positive-length paths.

noncomputable def MagnitudeConjecture.LinearPathCategory.nilPathCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x : Category k Q) : (x ⟶ x) →ₗ[k] k

The coefficient of the trivial path in a free linear endomorphism.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.nilPathCoefficient_id {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x : Category k Q) : (nilPathCoefficient x) (CategoryTheory.CategoryStruct.id x) = 1

theorem MagnitudeConjecture.LinearPathCategory.mem_positivePathSubmodule_self_iff {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x : Category k Q) (f : x ⟶ x) : f ∈ positivePathSubmodule x x ↔ (nilPathCoefficient x) f = 0

For endomorphisms, having no trivial-path coefficient is exactly being a linear combination of positive-length paths.

theorem MagnitudeConjecture.LinearPathCategory.nilPathCoefficient_eq_zero_of_mem_lengthComponent {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x : Category k Q) {n : ℕ} (hn : n ≠ 0) {f : x ⟶ x} (hf : f ∈ lengthComponent x x n) : (nilPathCoefficient x) f = 0

A positive-length homogeneous endomorphism has zero trivial-path coefficient.