The Ext-Euler characteristic of a vertex simple

The first-arrow exact sequence 0 ⟶ ⨁_{i ⟶ j} Pⱼ ⟶ Pᵢ ⟶ Sᵢ ⟶ 0 computes the Ext-Euler characteristic of a vertex simple against a module with finite-dimensional spaces at that vertex and the heads of its outgoing arrows. The result is the combinatorial Euler form with the simple's dimension vector on the left. Cycles are allowed: the finite-arrow condition gives the short resolution, while only finite-dimensionality at these target vertex spaces is needed for the Hom dimensions.

See Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 3, and Derksen--Weyman, An Introduction to Quiver Representations, Chapter 1.

theorem TauCeti.isEulerAdmissible_vertexSimpleModule (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] (Y : ModuleCat (pathAlgebra k Q)) (hYi : FiniteDimensional k ↑(((quiverRepFunctor k Q).obj Y).obj ((CategoryTheory.Paths.of Q).obj i))) (hY : ∀ (j : Q) (a : i ⟶ j), FiniteDimensional k ↑(((quiverRepFunctor k Q).obj Y).obj ((CategoryTheory.Paths.of Q).obj j))) : IsEulerAdmissible k (vertexSimpleModule k Q i) Y

A vertex simple is Euler-admissible when the target has finite-dimensional spaces at the chosen vertex and at the heads of its outgoing arrows. The first-arrow resolution bounds Ext above degree one.

theorem TauCeti.extEuler_vertexSimpleModule (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i : Q) [Fintype ((j : Q) × (i ⟶ j))] (Y : ModuleCat (pathAlgebra k Q)) (hYi : FiniteDimensional k ↑(((quiverRepFunctor k Q).obj Y).obj ((CategoryTheory.Paths.of Q).obj i))) (hY : ∀ (j : Q) (a : i ⟶ j), FiniteDimensional k ↑(((quiverRepFunctor k Q).obj Y).obj ((CategoryTheory.Paths.of Q).obj j))) : extEuler k ⋯ = ↑(dimVector ((quiverRepFunctor k Q).obj Y) i) - ∑ a : (j : Q) × (i ⟶ j), ↑(dimVector ((quiverRepFunctor k Q).obj Y) a.fst)

The Ext-Euler value of a vertex simple is its vertex coordinate minus the dimensions at the heads of all arrows leaving that vertex.

@[simp]

theorem TauCeti.extEuler_vertexSimpleModule_vertexSimpleModule (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (i j : Q) [Finite ((a : Q) × (i ⟶ a))] : extEuler k ⋯ = (if i = j then 1 else 0) - ↑(Nat.card (i ⟶ j))

The Ext-Euler value between vertex simples is the Kronecker delta minus the number of arrows from the first vertex to the second.

theorem TauCeti.extEuler_vertexSimpleModule_eq_eulerForm (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] (i : Q) (Y : ModuleCat (pathAlgebra k Q)) (hYi : FiniteDimensional k ↑(((quiverRepFunctor k Q).obj Y).obj ((CategoryTheory.Paths.of Q).obj i))) (hY : ∀ (j : Q) (a : i ⟶ j), FiniteDimensional k ↑(((quiverRepFunctor k Q).obj Y).obj ((CategoryTheory.Paths.of Q).obj j))) : extEuler k ⋯ = ((eulerForm Q) fun (j : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj (vertexSimpleModule k Q i)) j)) fun (j : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj Y) j)

The Ext-Euler characteristic of a vertex simple is the quiver Euler form of its dimension vector against that of the target module.