Degree-one mesh morphisms count arrows

theorem MagnitudeConjecture.MeshCategory.RightMeshData.basisCompositeSet_degree_ne_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (X Y : LinearPathCategory.Category k Q) (f : X ⟶ Y) (hf : f ∈ LinearPathCategory.basisCompositeSet T.meshGeneratorSet X Y) : ∃ (n : ℕ), n ≠ 1 ∧ f ∈ LinearPathCategory.lengthComponent X Y n

Composing a quadratic mesh relation with paths never produces degree one.

noncomputable def MagnitudeConjecture.MeshCategory.degreeOneFreeEquiv {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x y : Q) : ↥(LinearPathCategory.lengthComponent (LinearPathCategory.obj k Q x) (LinearPathCategory.obj k Q y) 1) ≃ₗ[k] ↥(lengthComponent T x y 1)

The mesh quotient leaves the free degree-one space unchanged.

theorem MagnitudeConjecture.MeshCategory.lengthComponent_one_finrank {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x y : Q) [Fintype (y ⟶ x)] : Module.finrank k ↥(lengthComponent T x y 1) = Fintype.card (y ⟶ x)

Degree-one mesh morphisms from x to y count quiver arrows from y to x.