The free degree-one path space counts arrows #
noncomputable def
MagnitudeConjecture.LinearPathCategory.lengthComponentPathEquiv
{k : Type u}
[Field k]
{Q : Type v}
[Quiver Q]
(X Y : Category k Q)
(n : ℕ)
:
↥(lengthComponent X Y n) ≃ₗ[k] { p : Quiver.Path (vertex Y) (vertex X) // p.length = n } →₀ k
Restrict path coordinates to one fixed path length.
Instances For
noncomputable def
MagnitudeConjecture.LinearPathCategory.lengthOneArrowEquiv
{k : Type u}
[Field k]
{Q : Type v}
[Quiver Q]
(X Y : Category k Q)
:
↥(lengthComponent X Y 1) ≃ₗ[k] (vertex Y ⟶ vertex X) →₀ k
Degree-one path coefficients are precisely coefficients indexed by arrows.
Instances For
theorem
MagnitudeConjecture.LinearPathCategory.lengthComponent_one_finrank
{k : Type u}
[Field k]
{Q : Type v}
[Quiver Q]
(X Y : Category k Q)
[Fintype (vertex Y ⟶ vertex X)]
:
Module.finrank k ↥(lengthComponent X Y 1) = Fintype.card (vertex Y ⟶ vertex X)
Variance is reversed: maps X to Y have the arrows from vertex Y to vertex X.