Classification of simple finite mesh modules

For a finite mesh category with local vertex endomorphism rings, the categorical radical of each finite representable is its unique maximal submodule. Its cokernel is the mesh simple at that vertex, and these exhaust the simple objects of the finite-dimensional module category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleStandardRadicalCokernelIso {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (hlocal : ∀ (X : T.VertexCategoryᵒᵖ), IsLocalRing (CategoryTheory.End X)) (z : Q) : CategoryTheory.Limits.cokernel (CoveringHom.finiteDimensionalLinearCoyonedaRadicalInclusion (have this := Opposite.op z; this) ⋯) ≅ T.simpleFiniteModule z

The radical cokernel of the representable at a vertex is the explicitly constructed mesh simple at that vertex.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.exists_iso_simpleFiniteModule_of_simple {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (hlocal : ∀ (X : T.VertexCategoryᵒᵖ), IsLocalRing (CategoryTheory.End X)) (M : CoveringHom.FiniteDimensionalModuleCategory k) [CategoryTheory.Simple M] : ∃ (z : Q), Nonempty (M ≅ T.simpleFiniteModule z)

Every simple finite-dimensional module on a finite mesh category is the mesh simple supported at one of its vertices.