Projective detection in a finite Riedtmann mesh

Riedtmann condition (b) lets a nonzero morphism be pulled backwards through an incoming arrow as long as its source vertex is nonprojective. Finite- dimensionality of the graded mesh Hom spaces makes their path-length filtration terminate. Consequently this backwards process reaches a projective vertex, which is precisely the faithfulness input for restricted Yoneda on the projective full subcategory.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.exists_uniform_source_lengthTail_eq_bot {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hfinite : ∀ (x y : Q), FiniteDimensional k (obj T x ⟶ obj T y)) (x : Q) : ∃ (N : ℕ), ∀ (z : Q), lengthTail T z x N = ⊥

For a fixed target vertex, finite-dimensionality gives a common cutoff at which every source-to-target path-length tail vanishes.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.exists_lengthTail_precomposition_ne_zero {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hB : T.RiedtmannConditionB) {x y : Q} (f : obj T x ⟶ obj T y) (hf : f ≠ 0) (hprojective : ∀ p ∈ T.projective, ∀ (g : obj T p ⟶ obj T x), CategoryTheory.CategoryStruct.comp g f = 0) (n : ℕ) : ∃ (z : Q), ∃ g ∈ lengthTail T z x n, CategoryTheory.CategoryStruct.comp g f ≠ 0

If no projective vertex detects a nonzero morphism, condition (b) can construct arbitrarily long nonvanishing precompositions.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.exists_projective_precomposition_ne_zero {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hfinite : ∀ (x y : Q), FiniteDimensional k (obj T x ⟶ obj T y)) (hB : T.RiedtmannConditionB) {x y : Q} (f : obj T x ⟶ obj T y) (hf : f ≠ 0) : ∃ (p : Q) (_ : p ∈ T.projective) (g : obj T p ⟶ obj T x), CategoryTheory.CategoryStruct.comp g f ≠ 0

Riedtmann condition (b) and Hom-finiteness make the projective vertices a detecting family for all morphisms in the raw mesh category.