The universal realization of a free linear path category

A reversed quiver representation in a linear category assigns an object to every vertex and a morphism F j ⟶ F i to every quiver arrow i ⟶ j. Concatenating those representatives and extending linearly gives the expected linear functor from the free linear path category.

This is the representation-independent path-realization kernel migrated from the Cartan formalization. It carries no determinant-specific dependencies.

@[irreducible]

def MagnitudeConjecture.LinearPathCategory.pathMap {Q : Type v} [Quiver Q] {C : Type z} [CategoryTheory.Category.{u_1, z} C] (F₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) {i j : Q} : Quiver.Path i j → (F₀ j ⟶ F₀ i)

Evaluate a path under a reversed assignment of quiver arrows.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.pathMap_nil {Q : Type v} [Quiver Q] {C : Type z} [CategoryTheory.Category.{u_1, z} C] (F₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) (i : Q) : pathMap F₀ (fun {i j : Q} => F₁) Quiver.Path.nil = CategoryTheory.CategoryStruct.id (F₀ i)

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.pathMap_cons {Q : Type v} [Quiver Q] {C : Type z} [CategoryTheory.Category.{u_1, z} C] (F₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) {i j l : Q} (p : Quiver.Path i j) (a : j ⟶ l) : pathMap F₀ (fun {i j : Q} => F₁) (p.cons a) = CategoryTheory.CategoryStruct.comp (F₁ a) (pathMap F₀ (fun {i j : Q} => F₁) p)

theorem MagnitudeConjecture.LinearPathCategory.pathMap_comp {Q : Type v} [Quiver Q] {C : Type z} [CategoryTheory.Category.{u_1, z} C] (F₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) {i j l : Q} (p : Quiver.Path i j) (q : Quiver.Path j l) : pathMap F₀ (fun {i j : Q} => F₁) (p.comp q) = CategoryTheory.CategoryStruct.comp (pathMap F₀ (fun {i j : Q} => F₁) q) (pathMap F₀ (fun {i j : Q} => F₁) p)

Reversed path evaluation turns concatenation into categorical composition.

noncomputable def MagnitudeConjecture.LinearPathCategory.homMap {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) : (x ⟶ y) →ₗ[k] F₀ (vertex x) ⟶ F₀ (vertex y)

Linear extension of reversed path evaluation to a Hom space of the free linear path category.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.homMap_pathHom {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} (p : Quiver.Path (vertex y) (vertex x)) : (homMap F₀ (fun {i j : Q} => F₁) x y) (pathHom p) = pathMap F₀ (fun {i j : Q} => F₁) p

theorem MagnitudeConjecture.LinearPathCategory.homPathLinearEquiv_symm_single {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y : Category k Q} (p : Quiver.Path (vertex y) (vertex x)) (r : k) : (homPathLinearEquiv x y).symm (Finsupp.single p r) = r • pathHom p

A scalar multiple of one path basis vector, transported back from the Finsupp coordinates.

noncomputable def MagnitudeConjecture.LinearPathCategory.lift {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)) : CategoryTheory.Functor (Category k Q) C

The linear realization functor determined by a reversed assignment of quiver arrows.

instance MagnitudeConjecture.LinearPathCategory.lift_additive {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)) : (lift F₀ fun {i j : Q} => F₁).Additive

instance MagnitudeConjecture.LinearPathCategory.lift_linear {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)) : CategoryTheory.Functor.Linear k (lift F₀ fun {i j : Q} => F₁)

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.lift_obj {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 : Category k Q) : (lift F₀ fun {i j : Q} => F₁).obj x = F₀ (vertex x)

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.lift_map_pathHom {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} (p : Quiver.Path (vertex y) (vertex x)) : (lift F₀ fun {i j : Q} => F₁).map (pathHom p) = pathMap F₀ (fun {i j : Q} => F₁) p

theorem MagnitudeConjecture.LinearPathCategory.pathMap_naturality {Q : Type v} [Quiver Q] {C : Type z} [CategoryTheory.Category.{u_1, z} C] (F₀ G₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) (G₁ : {i j : Q} → (i ⟶ j) → (G₀ j ⟶ G₀ i)) (α : (i : Q) → F₀ i ⟶ G₀ i) (hα : ∀ {i j : Q} (a : i ⟶ j), CategoryTheory.CategoryStruct.comp (F₁ a) (α i) = CategoryTheory.CategoryStruct.comp (α j) (G₁ a)) {i j : Q} (p : Quiver.Path i j) : CategoryTheory.CategoryStruct.comp (pathMap F₀ (fun {i j : Q} => F₁) p) (α i) = CategoryTheory.CategoryStruct.comp (α j) (pathMap G₀ (fun {i j : Q} => G₁) p)

Unary-arrow naturality for reversed assignments propagates along every path.

def MagnitudeConjecture.LinearPathCategory.liftNatTrans {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₀ G₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) (G₁ : {i j : Q} → (i ⟶ j) → (G₀ j ⟶ G₀ i)) (α : (i : Q) → F₀ i ⟶ G₀ i) (hα : ∀ {i j : Q} (a : i ⟶ j), CategoryTheory.CategoryStruct.comp (F₁ a) (α i) = CategoryTheory.CategoryStruct.comp (α j) (G₁ a)) : (lift F₀ fun {i j : Q} => F₁) ⟶ lift G₀ fun {i j : Q} => G₁

A natural transformation between free linear path realizations is determined by its vertex components and unary-arrow naturality squares.

noncomputable def MagnitudeConjecture.LinearPathCategory.liftNatIso {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₀ G₀ : Q → C) (F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i)) (G₁ : {i j : Q} → (i ⟶ j) → (G₀ j ⟶ G₀ i)) (α : (i : Q) → F₀ i ≅ G₀ i) (hα : ∀ {i j : Q} (a : i ⟶ j), CategoryTheory.CategoryStruct.comp (F₁ a) (α i).hom = CategoryTheory.CategoryStruct.comp (α j).hom (G₁ a)) : (lift F₀ fun {i j : Q} => F₁) ≅ lift G₀ fun {i j : Q} => G₁

An isomorphism between free linear path realizations is determined by vertex isomorphisms and unary-arrow naturality squares.