Top-torsionfree vertices in a Riedtmann mesh

Condition (b) prevents the simple at a nonprojective vertex from occurring as a submodule of a contravariant representable. This is the top-torsionfree step in the Bongartz--Gabriel injective-resolution argument.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.oppositeVertexObject {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (p : Q) : T.VertexCategoryᵒᵖ

A mesh vertex as an object of the opposite strict vertex category.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.eq_of_nonzero_map_simple_to_dualCorepresentable {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) {z p : Q} (hI : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.dualLinearYonedaLinearModule (T.oppositeVertexObject p))) (f : T.simpleFiniteModule z ⟶ CoveringHom.finiteDimensionalDualLinearYoneda (T.oppositeVertexObject p) hI) (hf : f ≠ 0) : z = p

A nonzero map from a mesh simple into D Hom(p,-) forces the simple to be supported at p.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.mem_projective_of_nonzero_map_simple_to_contravariantRepresentable {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (hB : T.RiedtmannConditionB) {z y : Q} (f : T.simpleFiniteModule z ⟶ T.contravariantRepresentableFiniteModule hP y) (hf : f ≠ 0) : z ∈ T.projective

If a nonzero map sends the mesh simple at z into a contravariant representable, then z is projective.