Kernels and the path-length filtration

A linear realization of a free path category has no kernel terms below a cutoff when the short realized paths remain linearly independent modulo a target submodule containing every long realized path. The cutoff-two case is the generic linear-algebra step in ordinary-quiver admissibility.

theorem MagnitudeConjecture.LinearPathCategory.exists_eq_toPath_of_length_one {Q : Type v} [Quiver Q] {x y : Q} (p : Quiver.Path x y) (hp : p.length = 1) : ∃ (a : x ⟶ y), p = a.toPath

noncomputable def MagnitudeConjecture.LinearPathCategory.arrowOfLengthOne {Q : Type v} [Quiver Q] {x y : Q} (p : { p : Quiver.Path x y // p.length = 1 }) : x ⟶ y

Recover the unique arrow represented by a path of length one.

theorem MagnitudeConjecture.LinearPathCategory.lengthOnePath_eq_toPath {Q : Type v} [Quiver Q] {x y : Q} (p : { p : Quiver.Path x y // p.length = 1 }) : ↑p = (arrowOfLengthOne p).toPath

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.arrowOfLengthOne_toPath {Q : Type v} [Quiver Q] {x y : Q} (a : x ⟶ y) : arrowOfLengthOne ⟨a.toPath, ⋯⟩ = a

theorem MagnitudeConjecture.LinearPathCategory.arrowOfLengthOne_injective {Q : Type v} [Quiver Q] {x y : Q} : Function.Injective arrowOfLengthOne

noncomputable def MagnitudeConjecture.LinearPathCategory.arrowEquivLengthOnePath {Q : Type v} [Quiver Q] (x y : Q) : (x ⟶ y) ≃ { p : Quiver.Path x y // p.length = 1 }

Arrows are equivalent to paths of length one.

def MagnitudeConjecture.LinearPathCategory.lowPathEquivLengthOnePath {Q : Type v} [Quiver Q] {x y : Q} (hxy : x ≠ y) : { p : Quiver.Path x y // p.length < 2 } ≃ { p : Quiver.Path x y // p.length = 1 }

Between distinct vertices, paths of length below two are exactly arrows.

noncomputable def MagnitudeConjecture.LinearPathCategory.optionArrowEquivLowPath {Q : Type v} [Quiver Q] (x : Q) : Option (x ⟶ x) ≃ { p : Quiver.Path x x // p.length < 2 }

At one vertex, paths of length below two are the trivial path or one loop.

theorem MagnitudeConjecture.LinearPathCategory.mem_lengthTail_of_map_eq_zero_of_low_independent {k : Type u} [Field k] {Q : Type v} [Quiver Q] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) {X Y : Category k Q} (W : Submodule k (F₀ (vertex X) ⟶ F₀ (vertex Y))) (n : ℕ) (hlong : ∀ (p : Quiver.Path (vertex Y) (vertex X)), n ≤ p.length → pathMap F₀ (fun {i j : Q} => F₁) p ∈ W) (hlow : LinearIndependent k fun (p : { p : Quiver.Path (vertex Y) (vertex X) // p.length < n }) => W.mkQ (pathMap F₀ (fun {i j : Q} => F₁) ↑p)) (f : X ⟶ Y) (hf : (homMap F₀ (fun {i j : Q} => F₁) X Y) f = 0) : f ∈ lengthTail X Y n

If all paths at or above n map into W and the shorter paths remain linearly independent modulo W, then every element of the realization kernel is supported in path lengths at least n.