Documentation

TauCeti.RepresentationTheory.Quiver.Representation.Projective.Finite

Finiteness of vertex projectives #

Every vertex projective is a finitely generated path-algebra module. This places vertex projectives in the category of finitely generated modules and its Grothendieck group.

See Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 2.

source
theorem TauCeti.module_finite_indecProjModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) :
Module.Finite (pathAlgebra k Q) ↑(indecProjModule k Q i)

A vertex projective is finitely generated as a path-algebra module.

source
noncomputable def TauCeti.vertexProjectiveModuleFG (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) :
FGModuleCat (pathAlgebra k Q)

A vertex projective as a finitely generated path-algebra module.

Instances For
    source
    @[simp]
    theorem TauCeti.vertexProjectiveModuleFG_obj (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) :
    (vertexProjectiveModuleFG k Q i).obj = indecProjModule k Q i

    The underlying module of a finite vertex projective is indecProjModule.

    source
    instance TauCeti.instProjectivePathAlgebraCarrierVertexProjectiveModuleFG (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) :
    Module.Projective (pathAlgebra k Q) ↑(vertexProjectiveModuleFG k Q i)

    A finite vertex projective is projective as a path-algebra module.

    source
    instance TauCeti.instProjectiveFGModuleCatPathAlgebraVertexProjectiveModuleFG (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) :
    CategoryTheory.Projective (vertexProjectiveModuleFG k Q i)

    A finite vertex projective is a projective object of finitely generated modules.