Weak mesh exactness in the finite additive hull

The finite matrix category is the additive hull of the strict raw mesh category. The objectwise exactness of the contravariant mesh representables therefore upgrades to a genuine weak-kernel statement for each nonprojective mesh. This is the additive categorical form used in the Bongartz--Gabriel Auslander-category argument.

Only the middle exactness of the mesh is asserted. In particular, the map from the translate need not be monic.

@[reducible, inline]

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

The finite additive hull of the strict vertex model of the raw mesh category.

@[reducible, inline]

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

A mesh vertex as a singleton object of the finite additive hull.

def MagnitudeConjecture.MeshCategory.RightMeshData.additiveIncomingObj {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : T.AdditiveHull

The additive-hull object indexed by the arrows entering z.

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

The matrix of paired arrows from the translate into the incoming middle term of a nonprojective mesh.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.additiveIncomingMap {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : T.additiveIncomingObj z ⟶ T.additiveVertexObj z

The matrix of incoming arrows from the middle term to its endpoint.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.additiveIncomingMap_not_splitEpi {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) : ¬CategoryTheory.IsSplitEpi (T.additiveIncomingMap z)

The complete incoming-arrow matrix never has a section: every entry of a hypothetical section--matrix composite has positive path length, whereas the identity of the endpoint vertex has degree zero.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.additiveRightMesh {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) : CategoryTheory.ShortComplex T.AdditiveHull

The right mesh ending at a nonprojective vertex, inside the finite additive hull.

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

Evaluation of a one-row matrix, reindexed by the actual incoming arrows and stripped of the induced-category wrapper.

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

Evaluation identifies a one-by-one matrix with the underlying raw mesh Hom space.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.additiveIncomingHomLinearEquiv_comp_translationMap {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) (z : { z : Q // z ∉ T.projective }) (f : T.additiveVertexObj x ⟶ T.additiveVertexObj (T.tau z)) : (T.additiveIncomingHomLinearEquiv x ↑z) (CategoryTheory.CategoryStruct.comp f (T.additiveTranslationMap z)) = T.pairedCoefficient z ((T.additiveVertexHomLinearEquiv x (T.tau z)) f)

Evaluating postcomposition by the matrix of paired arrows gives the paired-coefficient map of the representable mesh presentation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.additiveVertexHomLinearEquiv_comp_incomingMap {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x z : Q) (f : T.additiveVertexObj x ⟶ T.additiveIncomingObj z) : (T.additiveVertexHomLinearEquiv x z) (CategoryTheory.CategoryStruct.comp f (T.additiveIncomingMap z)) = T.incomingSum ((T.additiveIncomingHomLinearEquiv x z) f)

Evaluating postcomposition by the incoming-arrow matrix gives literal incoming summation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.additiveRightMesh_exact_from_vertex {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) (z : { z : Q // z ∉ T.projective }) : Function.Exact (fun (l : T.additiveVertexObj x ⟶ (T.additiveRightMesh z).X₁) => CategoryTheory.CategoryStruct.comp l (T.additiveRightMesh z).f) fun (q : T.additiveVertexObj x ⟶ (T.additiveRightMesh z).X₂) => CategoryTheory.CategoryStruct.comp q (T.additiveRightMesh z).g

The additive-hull mesh is exact against every singleton source.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.additiveRightMesh_isWeakKernel {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) : QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel (T.additiveRightMesh z)

The right mesh ending at a nonprojective vertex is a weak-kernel pair in the finite additive hull. No monicity of its first map is used or claimed.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.additiveIncomingMap_mono_of_projective {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) (hz : z ∈ T.projective) : CategoryTheory.Mono (T.additiveIncomingMap z)

At a projective vertex, the incoming-arrow matrix is monic in the finite additive hull. This is the projective boundary case complementary to the nonprojective weak mesh above.