Riedtmann's incoming-detection condition

Condition (b) in the Bongartz--Gabriel--Riedtmann mesh-Auslander criterion says that every nonzero morphism out of a nonprojective mesh vertex remains nonzero after precomposition with at least one arrow entering that vertex. In the finite additive hull this is exactly epimorphy of the matrix of all incoming arrows.

This file records that equivalence. It does not assume or assert that an arbitrary finite translation quiver satisfies the condition.

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

Riedtmann condition (b) at one vertex: every nonzero morphism out of the vertex is detected after precomposition with one represented incoming arrow.

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

The global condition restricts incoming detection to the nonprojective vertices, exactly as in Riedtmann's criterion.

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

Incoming detection at z is equivalent to epimorphy of the complete incoming-arrow matrix in the finite additive hull.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.riedtmannConditionB_iff_epi_additiveIncomingMap {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) : T.RiedtmannConditionB ↔ ∀ (z : { z : Q // z ∉ T.projective }), CategoryTheory.Epi (T.additiveIncomingMap ↑z)

Riedtmann condition (b) is equivalently epimorphy of every nonprojective incoming-arrow matrix.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.compositionDualityLinearMap {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (p x j : Q) (epsilon : (obj T p ⟶ obj T j) →ₗ[k] k) : (obj T p ⟶ obj T x) →ₗ[k] Module.Dual k (obj T x ⟶ obj T j)

Composition followed by a linear form, regarded as the linear map from the left Hom space to the coefficient dual of the right Hom space.

structure MagnitudeConjecture.MeshCategory.RightMeshData.RiedtmannProjectiveDualityData {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (p : Q) : Type (max u u_1)

The perfect-composition-pairing data in Riedtmann condition (c) for one projective vertex.

• dualVertex : Q
• epsilon : (obj T p ⟶ obj T self.dualVertex) →ₗ[k] k
• pairing_bijective (x : Q) : Function.Bijective ⇑(T.compositionDualityLinearMap p x self.dualVertex self.epsilon)

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

Riedtmann condition (c): every projective vertex admits a vertex and a linear form whose composition pairing is a vector-space duality at every vertex.