Ringel's directed faithfulness induction

This file develops the representation-independent part of the standardness argument. A strict order on arrows rules out backward paths. The ordinary mesh relation then records, in the quotient, the composite of the paired source and sink arrow families.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.path_lt_of_length_ne_zero {Q : Type} [Quiver Q] [LinearOrder Q] (harrow : ∀ {a b : Q} (a_1 : a ⟶ b), b < a) {a b : Q} (p : Quiver.Path a b) (hp : p.length ≠ 0) : b < a

If every arrow strictly lowers a chosen order, every nonempty path also strictly lowers that order.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.hom_eq_zero_of_lt {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {T : RightMeshData Q} [LinearOrder Q] (harrow : ∀ {a b : Q} (a_1 : a ⟶ b), b < a) {x y : Q} (hyx : y < x) (f : obj T x ⟶ obj T y) : f = 0

There are no mesh-category morphisms strictly backwards in an order lowered by every quiver arrow.

@[simp]

theorem MagnitudeConjecture.MeshCategory.Realization.functor_map_incomingArrowHom {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) {z : Q} (a : RightMeshData.IncomingArrow z) : R.functor.map (T.incomingArrowHom a) = R.arrowMap a.snd

The realization of a length-one mesh morphism is its selected arrow representative.

theorem MagnitudeConjecture.MeshCategory.Realization.functor_map_incomingSum {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) {x z : Q} (h : T.IncomingCoefficient x z) : R.functor.map (T.incomingSum h) = ∑ a : RightMeshData.IncomingArrow z, CategoryTheory.CategoryStruct.comp (R.functor.map (h a)) (R.arrowMap a.snd)

Realization carries the incoming-arrow decomposition to the corresponding sum of composites in the target category.

structure MagnitudeConjecture.MeshCategory.Realization.DirectedExactData {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) : Type

The local exactness input in Ringel's proof. At a projective target the incoming arrow family is jointly monic. At a nonprojective target its kernel is generated by the paired outgoing arrow family from the translate.

• order : LinearOrder Q
• arrow_lt {a b : Q} (_e : a ⟶ b) : b < a
• target_id_ne_zero (x : Q) : CategoryTheory.CategoryStruct.id (R.functor.obj (obj T x)) ≠ 0
• projective_exact (z : Q) : z ∈ T.projective → ∀ (x : Q) (h : T.IncomingCoefficient x z), ∑ a : RightMeshData.IncomingArrow z, CategoryTheory.CategoryStruct.comp (R.functor.map (h a)) (R.functor.map (T.incomingArrowHom a)) = 0 → ∀ (a : RightMeshData.IncomingArrow z), R.functor.map (h a) = 0
• nonprojective_exact (z : { z : Q // z ∉ T.projective }) (x : Q) (h : T.IncomingCoefficient x ↑z) : ∑ a : RightMeshData.IncomingArrow ↑z, CategoryTheory.CategoryStruct.comp (R.functor.map (h a)) (R.functor.map (T.incomingArrowHom a)) = 0 → ∃ (t : R.functor.obj (obj T x) ⟶ R.functor.obj (obj T (T.tau z))), ∀ (a : RightMeshData.IncomingArrow ↑z), R.functor.map (h a) = CategoryTheory.CategoryStruct.comp t (R.functor.map (T.incomingArrowHom ⟨T.tau z, (T.arrowEquiv z a.fst) a.snd⟩))

theorem MagnitudeConjecture.MeshCategory.Realization.DirectedExactData.map_eq_zero {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) (D : R.DirectedExactData) [R.functor.Full] {x z : Q} (f : obj T x ⟶ obj T z) (hf : R.functor.map f = 0) : f = 0

Ringel's induction on the target vertex: local mesh exactness and directedness force every morphism killed by the realization to vanish.

theorem MagnitudeConjecture.MeshCategory.Realization.DirectedExactData.map_injective {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) (D : R.DirectedExactData) [R.functor.Full] (x z : Q) : Function.Injective fun (f : obj T x ⟶ obj T z) => R.functor.map f

On every displayed pair of mesh vertices, the directed exact realization is injective. This vertexwise form is exactly what the strict standard mesh presentation consumes.