The translation map in a mesh-simple presentation

At a nonprojective vertex, the polarization sends every incoming arrow to the paired arrow out of the translate. Precomposition with these paired arrows defines the map preceding the incoming-arrow map in the standard projective presentation of the vertex simple.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.freePairedCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) {x : Q} (q : LinearPathCategory.obj k Q x ⟶ LinearPathCategory.obj k Q (T.tau z)) : LinearPathCategory.IncomingCoefficient x ↑z

The free-category paired coefficient family before imposing the mesh relations.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.quotient_map_free_incomingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x z : Q} (c : LinearPathCategory.IncomingCoefficient x z) : (quotientFunctor T).map (LinearPathCategory.incomingSum c) = T.incomingSum fun (a : IncomingArrow z) => (quotientFunctor T).map (c a)

Quotienting a free incoming sum gives the corresponding incoming sum in the mesh category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.pairedCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) {x : Q} (q : obj T x ⟶ obj T (T.tau z)) : T.IncomingCoefficient x ↑z

Coefficients obtained by following a morphism to the translate by every paired arrow.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.quotient_map_freePairedCoefficient_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) {x : Q} (q : LinearPathCategory.obj k Q x ⟶ LinearPathCategory.obj k Q (T.tau z)) (a : LinearPathCategory.IncomingArrow ↑z) : (quotientFunctor T).map (T.freePairedCoefficient z q a) = T.pairedCoefficient z ((quotientFunctor T).map q) a

Quotienting one free paired coefficient gives the corresponding paired coefficient in the mesh category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.pairedCoefficientLinearMap {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) (x : Q) : (obj T x ⟶ obj T (T.tau z)) →ₗ[k] T.IncomingCoefficient x ↑z

The paired-coefficient construction as a linear map.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.pairedCoefficientLinearMap_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) (x : Q) (q : obj T x ⟶ obj T (T.tau z)) : (T.pairedCoefficientLinearMap z x) q = T.pairedCoefficient z q

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSumLinearMap_comp_pairedCoefficientLinearMap_eq_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) (x : Q) : T.incomingSumLinearMap x ↑z ∘ₗ T.pairedCoefficientLinearMap z x = 0

The paired translation map followed by incoming summation is the mesh relation and hence vanishes.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.range_pairedCoefficientLinearMap_eq_ker_incomingSumLinearMap {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) (x : Q) : (T.pairedCoefficientLinearMap z x).range = (T.incomingSumLinearMap x ↑z).ker

Exactness at the incoming-coefficient term of the mesh-simple presentation. No injectivity assertion is made about the translation map.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSumLinearMap_injective_of_projective {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) (hz : z ∈ T.projective) (x : Q) : Function.Injective ⇑(T.incomingSumLinearMap x z)

At a projective target there is no endpoint mesh relation, so the incoming-arrow map is injective.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.translationMap {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) : (CategoryTheory.linearYoneda k T.VertexCategory).obj (T.tau z) ⟶ T.incomingCoefficientFunctor ↑z

The natural map from the representable at the translate to the incoming coefficient functor.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.translationMap_comp_incomingMap {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) : CategoryTheory.CategoryStruct.comp (T.translationMap z) (T.incomingMap ↑z) = 0

The translation map and the incoming-arrow map form a complex.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.range_translationMap_app_eq_ker_incomingMap_app {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) (X : T.VertexCategoryᵒᵖ) : (ModuleCat.Hom.hom ((T.translationMap z).app X)).range = (ModuleCat.Hom.hom ((T.incomingMap ↑z).app X)).ker

Objectwise exactness at the incoming-coefficient functor in the nonprojective mesh-simple presentation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingMap_app_injective_of_projective {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) (hz : z ∈ T.projective) (X : T.VertexCategoryᵒᵖ) : Function.Injective ⇑(ModuleCat.Hom.hom ((T.incomingMap z).app X))

At a projective vertex, every evaluated incoming map is injective.