The positive tail of a mesh representable

For a vertex z, the morphisms into z of positive path length are exactly the sums of morphisms followed by one arrow into z. This is the first exact part of the standard mesh presentation of the simple contravariant functor at z.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingArrowHom_mem_lengthComponent_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {z : Q} (a : IncomingArrow z) : T.incomingArrowHom a ∈ lengthComponent T a.fst z 1

A represented quiver arrow into a vertex has path degree one.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.outgoingArrowHom_mem_lengthComponent_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x : Q} (a : OutgoingArrow x) : T.outgoingArrowHom a ∈ lengthComponent T x a.fst 1

A represented quiver arrow out of a vertex has path degree one.

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

The incoming-arrow sum, regarded as a linear map from its coefficient space to the target Hom space.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSumLinearMap_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x z : Q} (c : T.IncomingCoefficient x z) : (T.incomingSumLinearMap x z) c = T.incomingSum c

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSum_mem_lengthTail_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x z : Q} (c : T.IncomingCoefficient x z) : T.incomingSum c ∈ lengthTail T x z 1

Every sum through the incoming arrows has positive path length.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.smul_id_mem_lengthTail_one_iff {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) (c : k) : c • CategoryTheory.CategoryStruct.id (obj T x) ∈ lengthTail T x x 1 ↔ c = 0

A scalar multiple of a vertex identity can have positive path length only when its scalar is zero.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.diagonalScalar_eq_zero_of_mem_lengthTail_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x z : Q} (c : k) (hc : T.diagonalScalar x z c ∈ lengthTail T x z 1) : T.diagonalScalar x z c = 0

A diagonal scalar term lying in the positive tail vanishes. For unequal vertices it is zero by definition; at one vertex this is degree separation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.range_incomingSumLinearMap_eq_lengthTail_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x z : Q) : (T.incomingSumLinearMap x z).range = lengthTail T x z 1

The image of the incoming-arrow map is exactly the positive-length tail of the contravariant representable at its target.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.simpleValue {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x z : Q) : Type (max (max u v) w)

The value at x of the simple contravariant mesh functor supported at z: the representable Hom space modulo all positive-length morphisms.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleValueProjection {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x z : Q) : (obj T x ⟶ obj T z) →ₗ[k] T.simpleValue x z

The canonical projection from the representable Hom space to the simple value.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simpleValueProjection_surjective {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x z : Q) : Function.Surjective ⇑(T.simpleValueProjection x z)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.ker_simpleValueProjection_eq_range_incomingSumLinearMap {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x z : Q) : (T.simpleValueProjection x z).ker = (T.incomingSumLinearMap x z).range

Objectwise exactness at the representable: the kernel of projection to the simple value is exactly the image of all incoming arrows.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simpleValue_subsingleton_of_ne {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x z : Q} (hxz : x ≠ z) : Subsingleton (T.simpleValue x z)

Away from its supporting vertex, the simple mesh value is zero.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleValueSelfScalarLinearMap {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : k →ₗ[k] T.simpleValue z z

Scalar multiples of the identity map into the value of the simple mesh functor at its supporting vertex.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simpleValueSelfScalarLinearMap_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) (c : k) : (T.simpleValueSelfScalarLinearMap z) c = (T.simpleValueProjection z z) (c • CategoryTheory.CategoryStruct.id (obj T z))

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simpleValueSelfScalarLinearMap_bijective {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : Function.Bijective ⇑(T.simpleValueSelfScalarLinearMap z)

At its supporting vertex, the simple mesh value is one-dimensional, with the identity class as its canonical basis vector.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleValueSelfLinearEquiv {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : k ≃ₗ[k] T.simpleValue z z

The canonical identification of the supporting value of a mesh simple with the coefficient field.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.precomp_mem_lengthTail_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x y z : Q} (f : obj T y ⟶ obj T x) {q : obj T x ⟶ obj T z} (hq : q ∈ lengthTail T x z 1) : CategoryTheory.CategoryStruct.comp f q ∈ lengthTail T y z 1

Precomposition preserves the positive tail in the contravariant representable.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.VertexCategory {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) : Type v

The strict vertex model of the raw mesh category. Its objects are the quiver vertices themselves and its Hom spaces are the corresponding raw mesh Hom spaces.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleFunctor {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : CategoryTheory.Functor T.VertexCategoryᵒᵖ (ModuleCat k)

The simple contravariant mesh functor supported at z.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleProjection {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : (CategoryTheory.linearYoneda k T.VertexCategory).obj z ⟶ T.simpleFunctor z

The representable presheaf projects naturally onto the mesh simple.

instance MagnitudeConjecture.MeshCategory.RightMeshData.simpleProjection_epi {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : CategoryTheory.Epi (T.simpleProjection z)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingCoefficientFunctor {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : CategoryTheory.Functor T.VertexCategoryᵒᵖ (ModuleCat k)

The finite family of contravariant representables indexed by the arrows into z, presented objectwise as its coefficient product.

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

Summing after the incoming arrows is a natural map from the incoming coefficient functor to the representable at z.

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

The incoming-arrow map followed by projection to the mesh simple is zero.

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

Exactness of the incoming-arrow presentation at every object of the raw mesh category.