Decomposition by the first represented arrow

A morphism in the free reversed linear path category between distinct vertices is a finite sum of one represented arrow out of its categorical source followed by a coefficient path. This is the free-category form used by Ringel's recursive fullness construction.

@[reducible, inline]

abbrev MagnitudeConjecture.LinearPathCategory.OutgoingArrow {Q : Type v} [Quiver Q] (x : Q) : Type (max v w)

Reversed quiver arrows whose represented categorical maps start at x.

noncomputable def MagnitudeConjecture.LinearPathCategory.outgoingArrowHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x : Q} (a : OutgoingArrow x) : obj k Q x ⟶ obj k Q a.fst

The free-path morphism represented by one arrow out of x.

@[reducible, inline]

abbrev MagnitudeConjecture.LinearPathCategory.OutgoingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x z : Q) : Type (max (max w v) (max u v) w)

One free-path coefficient after every arrow out of x.

noncomputable def MagnitudeConjecture.LinearPathCategory.outgoingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype (OutgoingArrow x)] {x z : Q} (c : OutgoingCoefficient x z) : obj k Q x ⟶ obj k Q z

Sum of all first-arrow factorizations.

noncomputable def MagnitudeConjecture.LinearPathCategory.singleOutgoingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x z : Q} (a₀ : OutgoingArrow x) (f : obj k Q a₀.fst ⟶ obj k Q z) : OutgoingCoefficient x z

A coefficient family supported after one outgoing arrow.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.outgoingSum_single {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype (OutgoingArrow x)] {x z : Q} (a₀ : OutgoingArrow x) (f : obj k Q a₀.fst ⟶ obj k Q z) : outgoingSum (singleOutgoingCoefficient a₀ f) = CategoryTheory.CategoryStruct.comp (outgoingArrowHom a₀) f

theorem MagnitudeConjecture.LinearPathCategory.exists_eq_outgoingSum_of_ne {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype (OutgoingArrow x)] {x z : Q} (hxz : x ≠ z) (f : obj k Q x ⟶ obj k Q z) : ∃ (h : OutgoingCoefficient x z), f = outgoingSum h

Between distinct vertices, every free-path morphism is a sum grouped by its first represented categorical arrow.

theorem MagnitudeConjecture.LinearPathCategory.exists_eq_smul_id_add_outgoingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype (OutgoingArrow x)] {x : Q} (f : obj k Q x ⟶ obj k Q x) : ∃ (r : k) (h : OutgoingCoefficient x x), f = r • CategoryTheory.CategoryStruct.id (obj k Q x) + outgoingSum h

Every free-path endomorphism is a scalar identity plus a sum grouped by its first represented categorical arrow. This is the diagonal counterpart of exists_eq_outgoingSum_of_ne; the scalar is exactly the coefficient of the trivial path.

theorem MagnitudeConjecture.LinearPathCategory.exists_eq_smul_id_add_incomingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype (IncomingArrow z)] {z : Q} (f : obj k Q z ⟶ obj k Q z) : ∃ (r : k) (h : IncomingCoefficient z z), f = r • CategoryTheory.CategoryStruct.id (obj k Q z) + incomingSum h

Every free-path endomorphism is a scalar identity plus a sum grouped by its last represented categorical arrow.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.pathMap_toPath {Q : Type v} [Quiver Q] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) {i j : Q} (a : i ⟶ j) : pathMap F₀ (fun {i j : Q} => F₁) a.toPath = F₁ a

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.lift_map_outgoingArrowHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) {x : Q} (a : OutgoingArrow x) : (lift F₀ fun {i j : Q} => F₁).map (outgoingArrowHom a) = F₁ a.snd

theorem MagnitudeConjecture.LinearPathCategory.lift_map_outgoingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype (OutgoingArrow x)] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) {x z : Q} (c : OutgoingCoefficient x z) : (lift F₀ fun {i j : Q} => F₁).map (outgoingSum c) = ∑ a : OutgoingArrow x, CategoryTheory.CategoryStruct.comp (F₁ a.snd) ((lift F₀ fun {i j : Q} => F₁).map (c a))

Evaluation of a first-arrow decomposition is the corresponding sum of represented arrows followed by evaluated coefficients.

theorem MagnitudeConjecture.LinearPathCategory.path_target_le_of_arrow_lt {Q : Type v} [Quiver Q] [Preorder Q] (harrow : ∀ {i j : Q} (a : i ⟶ j), j < i) {i j : Q} (p : Quiver.Path i j) : j ≤ i

If every quiver arrow strictly lowers an order, the endpoint of a path is below its starting vertex.

theorem MagnitudeConjecture.LinearPathCategory.pathMap_eq_of_eq_on_source_le {Q : Type v} [Quiver Q] [Preorder Q] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F₀ : Q → C) (F₁ G₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) (harrow : ∀ {i j : Q} (a : i ⟶ j), j < i) {i j : Q} (p : Quiver.Path i j) (h : ∀ {a b : Q} (e : a ⟶ b), a ≤ i → F₁ e = G₁ e) : pathMap F₀ (fun {i j : Q} => F₁) p = pathMap F₀ (fun {i j : Q} => G₁) p

Changing arrow representatives strictly above the start of a path does not change its evaluation.

theorem MagnitudeConjecture.LinearPathCategory.homMap_eq_of_eq_on_source_le {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Preorder Q] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F₀ : Q → C) (F₁ G₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) (harrow : ∀ {i j : Q} (a : i ⟶ j), j < i) {x z : Q} (f : obj k Q x ⟶ obj k Q z) (h : ∀ {a b : Q} (e : a ⟶ b), a ≤ z → F₁ e = G₁ e) : (homMap F₀ (fun {i j : Q} => F₁) (obj k Q x) (obj k Q z)) f = (homMap F₀ (fun {i j : Q} => G₁) (obj k Q x) (obj k Q z)) f

The corresponding stability statement for a linear combination of paths.