The vertex simples as a simple family of a path algebra

Let Q be a finite quiver whose path algebra kQ is finite-dimensional, that is, a finite acyclic quiver. Its simple modules are the vertex simples Sᵢ, so the family of vertex simples, viewed as finitely generated kQ-modules, is an exhaustive family of simple modules in the sense of TauCeti.IsExhaustiveSimpleFamily. Their classes therefore span G₀(mod kQ), and any additive identity on that group can be checked on them.

Main results

• TauCeti.vertexSimpleModuleFG: the vertex simple Sᵢ as a finitely generated module.
• TauCeti.isExhaustiveSimpleFamily_vertexSimpleModuleFG: the vertex simples exhaust the simple modules of a finite-dimensional path algebra.

References

• Ibrahim Assem, Daniel Simson, and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 2.

noncomputable def TauCeti.vertexSimpleModuleFG (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) : FGModuleCat (pathAlgebra k Q)

The vertex simple Sᵢ as an object of the category of finitely generated modules.

@[simp]

theorem TauCeti.vertexSimpleModuleFG_obj (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) : (vertexSimpleModuleFG k Q i).obj = vertexSimpleModule k Q i

The underlying module of the finitely generated vertex simple is the vertex simple module.

instance TauCeti.isSimpleModule_vertexSimpleModuleFG (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) : IsSimpleModule (pathAlgebra k Q) ↑(vertexSimpleModuleFG k Q i)

The finitely generated vertex simple is a simple module.

theorem TauCeti.pairwise_isEmpty_linearEquiv_vertexSimpleModuleFG (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : Pairwise fun (i j : Q) => IsEmpty (↑(vertexSimpleModuleFG k Q i) ≃ₗ[pathAlgebra k Q] ↑(vertexSimpleModuleFG k Q j))

Vertex simples at distinct vertices are nonisomorphic as path-algebra modules.

theorem TauCeti.isExhaustiveSimpleFamily_vertexSimpleModuleFG (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] : IsExhaustiveSimpleFamily (vertexSimpleModuleFG k Q)

The vertex simples exhaust the simple modules of a finite-dimensional path algebra.