Finite mesh categories and their path-length grading

This file packages the right-translation data needed for ordinary mesh relations. The quiver is written in the orientation used by the free linear path category: an arrow x ⟶ y represents an irreducible morphism from y to x. Thus the translation pairing at a nonprojective x sends

x ⟶ y to y ⟶ τx.

When the arrow star at each vertex is finite, the mesh relation is the sum of the corresponding length-two paths. The vertex type itself may be infinite, as it is for a universal Auslander--Reiten cover. The general homogeneous- relation quotient construction then gives an internally graded mesh category.

structure MagnitudeConjecture.MeshCategory.RightMeshData (Q : Type v) [Quiver Q] : Type (max v w)

The minimal right-translation-quiver data needed to form ordinary mesh relations. Full Auslander--Reiten data will provide this by restricting the translation to nonprojective vertices and pairing the two sides of each mesh.

• projective : Set Q
• tau : { x : Q // x ∉ self.projective } → Q
• arrowEquiv (x : { x : Q // x ∉ self.projective }) (y : Q) : (↑x ⟶ y) ≃ (y ⟶ self.tau x)

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.MeshArrow {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) : Type (max v w)

A reversed incoming arrow at the endpoint of a mesh.

def MagnitudeConjecture.MeshCategory.RightMeshData.meshPath {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) (a : T.MeshArrow x) : Quiver.Path (↑x) (T.tau x)

The length-two reversed-quiver path associated to one paired mesh arrow.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.meshPath_length {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) (a : T.MeshArrow x) : (T.meshPath x a).length = 2

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

The ordinary mesh relation at a nonprojective vertex.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.meshRelation_mem_lengthComponent_two {k : Type u} [Field k] {Q : Type v} [Quiver Q] (T : RightMeshData Q) [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (x : { x : Q // x ∉ T.projective }) : T.meshRelation x ∈ LinearPathCategory.lengthComponent (LinearPathCategory.obj k Q (T.tau x)) (LinearPathCategory.obj k Q ↑x) 2

Every ordinary mesh relation has path degree two.

def MagnitudeConjecture.MeshCategory.RightMeshData.meshGeneratorSet {k : Type u} [Field k] {Q : Type v} [Quiver Q] (T : RightMeshData Q) [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (X Y : LinearPathCategory.Category k Q) : Set (X ⟶ Y)

The family of all mesh-relation generators, indexed by their categorical endpoints. Equality transports only place a relation in the requested Hom type; after substituting the endpoint equalities they are identities.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.meshRelation_mem_meshGeneratorSet {k : Type u} [Field k] {Q : Type v} [Quiver Q] (T : RightMeshData Q) [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (x : { x : Q // x ∉ T.projective }) : T.meshRelation x ∈ T.meshGeneratorSet (LinearPathCategory.obj k Q (T.tau x)) (LinearPathCategory.obj k Q ↑x)

The defining mesh relation occurs in the generator family at its literal endpoints.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.meshGeneratorSet_mem_lengthComponent_two {k : Type u} [Field k] {Q : Type v} [Quiver Q] (T : RightMeshData Q) [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (X Y : LinearPathCategory.Category k Q) (f : X ⟶ Y) (hf : f ∈ T.meshGeneratorSet X Y) : f ∈ LinearPathCategory.lengthComponent X Y 2

Every generator in the endpoint-indexed family has degree two.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.meshGeneratorSet_isHomogeneous {k : Type u} [Field k] {Q : Type v} [Quiver Q] (T : RightMeshData Q) [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (X Y : LinearPathCategory.Category k Q) (f : X ⟶ Y) (hf : f ∈ T.meshGeneratorSet X Y) : ∃ (n : ℕ), f ∈ LinearPathCategory.lengthComponent X Y n

In particular, every mesh generator is homogeneous.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.basisCompositeSet_mem_positive {k : Type u} [Field k] {Q : Type v} [Quiver Q] (T : RightMeshData Q) [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (X Y : LinearPathCategory.Category k Q) (f : X ⟶ Y) (hf : f ∈ LinearPathCategory.basisCompositeSet T.meshGeneratorSet X Y) : ∃ (n : ℕ), n ≠ 0 ∧ f ∈ LinearPathCategory.lengthComponent X Y n

Every path-basis two-sided composite of a mesh generator has strictly positive path length.

@[reducible, inline]

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

The raw categorical quotient by the ordinary mesh relations.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.MeshCategory.quotientFunctor {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) : CategoryTheory.Functor (LinearPathCategory.Category k Q) (CategoryTheory.Quotient (LinearPathCategory.HomogeneousQuotient.relationIdeal T.meshGeneratorSet).rel)

The functor from the free linear path category to the raw mesh category.

@[reducible, inline]

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

A quiver vertex as an object of the raw mesh category.

noncomputable def MagnitudeConjecture.MeshCategory.lengthComponent {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x y : Q) (n : ℕ) : Submodule k (obj T x ⟶ obj T y)

The degree-n part of a mesh-category Hom space.

theorem MagnitudeConjecture.MeshCategory.lengthComponent_isInternal {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x y : Q) : DirectSum.IsInternal (lengthComponent T x y)

The path-length pieces form an internal decomposition of every mesh-category Hom space.

theorem MagnitudeConjecture.MeshCategory.comp_mem_lengthComponent {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x y z : Q} {i j : ℕ} {f : obj T x ⟶ obj T y} {g : obj T y ⟶ obj T z} (hf : f ∈ lengthComponent T x y i) (hg : g ∈ lengthComponent T y z j) : CategoryTheory.CategoryStruct.comp f g ∈ lengthComponent T x z (i + j)

Composition in the mesh category adds degrees.

@[simp]

theorem MagnitudeConjecture.MeshCategory.id_mem_lengthComponent_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : CategoryTheory.CategoryStruct.id (obj T x) ∈ lengthComponent T x x 0

Every mesh-category vertex identity has path degree zero.

theorem MagnitudeConjecture.MeshCategory.lengthComponent_zero_self {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : lengthComponent T x x 0 = k ∙ CategoryTheory.CategoryStruct.id (obj T x)

Degree zero at a mesh-category vertex is the scalar span of its identity.

theorem MagnitudeConjecture.MeshCategory.lengthComponent_zero_eq_bot_of_ne {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x y : Q} (hxy : y ≠ x) : lengthComponent T x y 0 = ⊥

Degree zero between distinct mesh-category vertices vanishes.

theorem MagnitudeConjecture.MeshCategory.quotient_map_meshRelation_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 }) : (quotientFunctor T).map (T.meshRelation x) = 0

Every defining mesh relation vanishes in the raw mesh category.

theorem MagnitudeConjecture.MeshCategory.id_ne_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : CategoryTheory.CategoryStruct.id (obj T x) ≠ 0

Mesh relations cannot kill a vertex identity: every two-sided path-basis composite of a mesh relation has positive length, while the identity has nonzero trivial-path coefficient.