Paired arrows and the ordinary mesh relation

The polarization pairs every arrow ending at a nonprojective vertex with an arrow out of its translate. Summing the resulting length-two composites is exactly the defining mesh relation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.free_paired_incomingSum_eq_comp_meshRelation {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) {y : Q} (q : LinearPathCategory.obj k Q y ⟶ LinearPathCategory.obj k Q (T.tau x)) : (LinearPathCategory.incomingSum fun (a : LinearPathCategory.IncomingArrow ↑x) => CategoryTheory.CategoryStruct.comp q (LinearPathCategory.pathHom ((T.arrowEquiv x a.fst) a.snd).toPath)) = CategoryTheory.CategoryStruct.comp q (T.meshRelation x)

Before quotienting, the sum of the paired translate-arrow/incoming-arrow composites is exactly a left multiple of the defining mesh relation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.pairedArrow_comp_incomingArrowHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) (a : T.MeshArrow x) : CategoryTheory.CategoryStruct.comp (T.incomingArrowHom ⟨T.tau x, (T.arrowEquiv x a.fst) a.snd⟩) (T.incomingArrowHom ⟨a.fst, a.snd⟩) = (quotientFunctor T).map (LinearPathCategory.pathHom (T.meshPath x a))

One paired translate-arrow/incoming-arrow composite is the corresponding term of the ordinary mesh relation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.paired_incomingSum_eq_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) {y : Q} (q : obj T y ⟶ obj T (T.tau x)) : (T.incomingSum fun (a : IncomingArrow ↑x) => CategoryTheory.CategoryStruct.comp q (T.incomingArrowHom ⟨T.tau x, (T.arrowEquiv x a.fst) a.snd⟩)) = 0

Precomposing all paired translate arrows with one morphism gives zero after summing against the incoming arrows, because the sum is the defining mesh relation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.raw_paired_incomingSum_eq_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) (X : RawCategory T) (q : X ⟶ obj T (T.tau x)) : ∑ a : IncomingArrow ↑x, CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp q (T.incomingArrowHom ⟨T.tau x, (T.arrowEquiv x a.fst) a.snd⟩)) (T.incomingArrowHom a) = 0

The paired incoming sum also vanishes when its source is an arbitrary raw mesh-category object rather than a displayed vertex object.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.paired_incomingSum_comp_eq_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) (X : RawCategory T) (q : obj T ↑x ⟶ X) : ∑ a : IncomingArrow ↑x, CategoryTheory.CategoryStruct.comp (T.incomingArrowHom ⟨T.tau x, (T.arrowEquiv x a.fst) a.snd⟩) (CategoryTheory.CategoryStruct.comp (T.incomingArrowHom a) q) = 0

Postcomposing the defining mesh relation by an arbitrary raw mesh-category morphism still gives zero.