The vertex simple as a path algebra module

The equivalence between quiver representations and left modules over the path algebra carries the vertex simple Sᵢ to a module and transports its length-one projective resolution. Thus the path algebra module Sᵢ has projective dimension at most one, without an acyclicity assumption. This is the short exact sequence used to calculate its Ext groups and Euler pairings against other modules.

The resolution is the standard first-arrow sequence 0 ⟶ ⨁_{e : i ⟶ j} Pⱼ ⟶ Pᵢ ⟶ Sᵢ ⟶ 0; see Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 2.

Over an acyclic quiver the vertex simples are the only simple modules: TauCeti.exists_iso_vertexSimpleModule_of_simple transports the classification of simple representations along the same equivalence. Together with the resolution it reduces statements about all simple path algebra modules, such as Euler-admissibility, to the vertex simples.

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

The left path algebra module corresponding to the vertex simple representation Sᵢ.

noncomputable def TauCeti.vertexSimpleModuleIso (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) : (quiverRepFunctor k Q).obj (vertexSimpleModule k Q i) ≅ simpleRep k Q i

The representation associated with vertexSimpleModule is the vertex simple.

instance TauCeti.finiteDimensional_vertexSimpleModule_obj (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i j : Q) : FiniteDimensional k ↑(((quiverRepFunctor k Q).obj (vertexSimpleModule k Q i)).obj j)

Every vertex space of a vertex simple path-algebra module is finite-dimensional.

instance TauCeti.simple_vertexSimpleModule (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) : CategoryTheory.Simple (vertexSimpleModule k Q i)

The vertex simple is a simple object of the path algebra module category.

theorem TauCeti.exists_iso_vertexSimpleModule_of_simple (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (hQ : Quiver.IsAcyclic Q) (M : ModuleCat (pathAlgebra k Q)) [CategoryTheory.Simple M] : ∃ (i : Q), Nonempty (M ≅ vertexSimpleModule k Q i)

Over an acyclic quiver, every simple path algebra module is a vertex simple.

noncomputable def TauCeti.vertexSimpleModuleResolution (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : CategoryTheory.ShortComplex (ModuleCat (pathAlgebra k Q))

The first-arrow projective resolution of the vertex simple, transported from quiver representations to path algebra modules.

theorem TauCeti.shortExact_vertexSimpleModuleResolution (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : (vertexSimpleModuleResolution k i).ShortExact

The transported first-arrow sequence is short exact.

noncomputable def TauCeti.vertexSimpleModuleResolutionX₂Iso (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : (vertexSimpleModuleResolution k i).X₂ ≅ indecProjModule k Q i

The middle term of the transported resolution is the vertex projective module.

noncomputable def TauCeti.vertexSimpleModuleResolutionX₁Iso (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : (vertexSimpleModuleResolution k i).X₁ ≅ ⨁ fun (a : (j : Q) × (i ⟶ j)) => indecProjModule k Q a.fst

The first term of the resolution is the direct sum of the vertex projective modules at the heads of the arrows leaving i.

noncomputable def TauCeti.vertexSimpleModuleResolutionX₃Iso (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : (vertexSimpleModuleResolution k i).X₃ ≅ vertexSimpleModule k Q i

The quotient of the transported resolution is the vertex simple module.

noncomputable def TauCeti.arrowSumToIndecProjModule (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : (⨁ fun (a : (j : Q) × (i ⟶ j)) => indecProjModule k Q a.fst) ⟶ indecProjModule k Q i

The first differential of the module resolution, expressed between the direct sum of vertex projective modules and the vertex projective module.

noncomputable def TauCeti.indecProjModuleToVertexSimpleModule (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : indecProjModule k Q i ⟶ vertexSimpleModule k Q i

The quotient map of the module resolution, from the vertex projective to the vertex simple.

@[simp]

theorem TauCeti.vertexSimpleModuleResolution_f (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolution k i).f (vertexSimpleModuleResolutionX₂Iso k i).hom = CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolutionX₁Iso k i).hom (arrowSumToIndecProjModule k i)

Under the term isomorphisms, the first differential is the module first-arrow map.

@[simp]

theorem TauCeti.vertexSimpleModuleResolution_f_assoc (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] {Z : ModuleCat (pathAlgebra k Q)} (h : indecProjModule k Q i ⟶ Z) : CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolution k i).f (CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolutionX₂Iso k i).hom h) = CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolutionX₁Iso k i).hom (CategoryTheory.CategoryStruct.comp (arrowSumToIndecProjModule k i) h)

Under the term isomorphisms, the first differential is the module first-arrow map.

@[simp]

theorem TauCeti.vertexSimpleModuleResolution_g (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolution k i).g (vertexSimpleModuleResolutionX₃Iso k i).hom = CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolutionX₂Iso k i).hom (indecProjModuleToVertexSimpleModule k i)

Under the term isomorphisms, the second differential is the module quotient map.

@[simp]

theorem TauCeti.vertexSimpleModuleResolution_g_assoc (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] {Z : ModuleCat (pathAlgebra k Q)} (h : vertexSimpleModule k Q i ⟶ Z) : CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolution k i).g (CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolutionX₃Iso k i).hom h) = CategoryTheory.CategoryStruct.comp (vertexSimpleModuleResolutionX₂Iso k i).hom (CategoryTheory.CategoryStruct.comp (indecProjModuleToVertexSimpleModule k i) h)

Under the term isomorphisms, the second differential is the module quotient map.

theorem TauCeti.shortExact_arrowSumToIndecProjModule (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : { X₁ := ⨁ fun (a : (j : Q) × (i ⟶ j)) => indecProjModule k Q a.fst, X₂ := indecProjModule k Q i, X₃ := vertexSimpleModule k Q i, f := arrowSumToIndecProjModule k i, g := indecProjModuleToVertexSimpleModule k i, zero := ⋯ }.ShortExact

The canonical first-arrow sequence of path algebra modules is short exact.

instance TauCeti.projective_vertexSimpleModuleResolution_X₁ (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : CategoryTheory.Projective (vertexSimpleModuleResolution k i).X₁

The first term of the transported resolution is projective.

instance TauCeti.projective_vertexSimpleModuleResolution_X₂ (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : CategoryTheory.Projective (vertexSimpleModuleResolution k i).X₂

The middle term of the first-arrow sequence is projective.

theorem TauCeti.hasProjectiveDimensionLT_two_vertexSimpleModule (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] : CategoryTheory.HasProjectiveDimensionLT (vertexSimpleModule k Q i) 2

A vertex simple of a path algebra has projective dimension less than two. This holds for finite quivers with finitely many arrows leaving the given vertex, including quivers with cycles.