The vertex projective as a module over the path algebra

TauCeti.indecProjRep is the vertex projective Pᵢ in the category of representations of a quiver, while constructions such as Ext live in the category ModuleCat (kQ) of modules over the path algebra. This file carries Pᵢ across the equivalence TauCeti.quiverRepFunctor: it names the module TauCeti.indecProjModule whose representation is Pᵢ, records that it is a projective object, and transports the universal property TauCeti.indecProjRepHomEquiv of Pᵢ to it. What comes out of the universal property is the dimension of the morphism space,

dim_k Hom(Pᵢ, Y) = (dim Y)ᵢ,

together with the finite-dimensionality of that space. The transport is k-linear, and not merely a bijection, because TauCeti.quiverRepFunctor is a k-linear functor; that is what lets a dimension computed for representations be read as one for kQ-modules.

As with TauCeti.indecProjRep, indecomposability of the vertex projective is not proved here; the name follows that of the representation it carries.

Main definitions

• TauCeti.indecProjModule k Q i: the kQ-module carrying the vertex projective Pᵢ, with TauCeti.indecProjModuleIso identifying its representation with Pᵢ.
• TauCeti.indecProjModuleHomEquiv: the universal property of Pᵢ in the module category, the k-linear isomorphism (Pᵢ ⟶ Y) ≃ₗ[k] Yᵢ.

Main results

• TauCeti.finrank_hom_indecProjModule: dim_k Hom(Pᵢ, Y) is the i-th coordinate of the dimension vector of Y.
• TauCeti.finiteDimensional_hom_indecProjModule: Hom(Pᵢ, Y) is finite-dimensional as soon as the vertex space of Y at i is.

References

• Ibrahim Assem, Daniel Simson and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 2, for the vertex projective as the left ideal kQ · eᵢ and its Hom functor.

noncomputable def TauCeti.indecProjModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) : ModuleCat (pathAlgebra k Q)

The vertex projective Pᵢ as a module over the path algebra. It is a preimage of the representation TauCeti.indecProjRep under the equivalence TauCeti.quiverRepFunctor; under the usual identification of representations with left modules it is the left ideal kQ · eᵢ.

noncomputable def TauCeti.indecProjModuleIso (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) : (quiverRepFunctor k Q).obj (indecProjModule k Q i) ≅ indecProjRep k Q i

The representation carried by TauCeti.indecProjModule is the vertex projective Pᵢ.

instance TauCeti.instProjectiveQuiverRepObjModuleCatPathAlgebraQuiverRepFunctorIndecProjModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) : CategoryTheory.Projective ((quiverRepFunctor k Q).obj (indecProjModule k Q i))

instance TauCeti.instProjectiveModuleCatPathAlgebraIndecProjModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) : CategoryTheory.Projective (indecProjModule k Q i)

noncomputable def TauCeti.indecProjModuleHomEquiv (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) (Y : ModuleCat (pathAlgebra k Q)) : (indecProjModule k Q i ⟶ Y) ≃ₗ[k] ↑(((quiverRepFunctor k Q).obj Y).obj ((CategoryTheory.Paths.of Q).obj i))

The universal property of the vertex projective in the module category: a kQ-linear map out of TauCeti.indecProjModule is, k-linearly in the map, an element of the i-th vertex space of the target. TauCeti.finrank_hom_indecProjModule and TauCeti.finiteDimensional_hom_indecProjModule below read the dimension and the finite-dimensionality of Hom(Pᵢ, Y) off it.

@[simp]

theorem TauCeti.finrank_hom_indecProjModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) (Y : ModuleCat (pathAlgebra k Q)) : Module.finrank k (indecProjModule k Q i ⟶ Y) = dimVector ((quiverRepFunctor k Q).obj Y) i

The morphisms out of a vertex projective are its vertex space. The dimension of Hom(Pᵢ, Y) is the i-th coordinate of the dimension vector of the representation of Y.

theorem TauCeti.finiteDimensional_hom_indecProjModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) (Y : ModuleCat (pathAlgebra k Q)) (hY : FiniteDimensional k ↑(((quiverRepFunctor k Q).obj Y).obj ((CategoryTheory.Paths.of Q).obj i))) : FiniteDimensional k (indecProjModule k Q i ⟶ Y)

One vertex space suffices for Hom-finiteness: the morphisms out of Pᵢ are the vertex space of Y at i, so their finite-dimensionality asks nothing of the other vertex spaces.

instance TauCeti.instFiniteDimensionalHomModuleCatPathAlgebraIndecProjModuleOfCarrier (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) (Y : ModuleCat (pathAlgebra k Q)) [FiniteDimensional k ↑Y] : FiniteDimensional k (indecProjModule k Q i ⟶ Y)