Dimension vectors of quiver representations

The dimension vector of a representation records the Module.finrank of its vector space at each vertex. No finite-dimensionality is assumed in the definition, so an infinite-dimensional component has value 0 by the convention for Module.finrank. This file defines dimension vectors and proves their fundamental functorial properties: invariance under isomorphism and additivity on biproducts and short exact sequences. It also records that, among pointwise finite-dimensional representations, only the zero object has vanishing dimension vector, so that an indecomposable one has a nonzero dimension vector.

References

This implements Layer 4, item “Dimension vectors”, of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md.

noncomputable def TauCeti.dimVector {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) : Q → ℕ

The Module.finrank dimension vector of a quiver representation, indexed by the vertices of the quiver. An infinite-dimensional component has value 0 by convention.

Equations

• TauCeti.dimVector M i = Module.finrank k ↑(M.obj ((CategoryTheory.Paths.of Q).obj i))

@[simp]

theorem TauCeti.dimVector_apply {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) (i : Q) : dimVector M i = Module.finrank k ↑(M.obj ((CategoryTheory.Paths.of Q).obj i))

The value of the dimension vector at a vertex is the Module.finrank of the corresponding vector space.

theorem TauCeti.dimVector_eq_of_iso {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} (e : M ≅ N) : dimVector M = dimVector N

Isomorphic quiver representations have the same dimension vector.

@[simp]

theorem TauCeti.dimVector_zero {k : Type u} {Q : Type v} [Field k] [Quiver Q] : dimVector 0 = 0

The zero representation has zero dimension vector.

@[simp]

theorem TauCeti.dimVector_biprod {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) (hM : ∀ (i : Q), FiniteDimensional k ↑(M.obj ((CategoryTheory.Paths.of Q).obj i))) (hN : ∀ (i : Q), FiniteDimensional k ↑(N.obj ((CategoryTheory.Paths.of Q).obj i))) : dimVector (M ⊞ N) = dimVector M + dimVector N

The dimension vector is additive on biproducts of pointwise finite-dimensional representations.

theorem TauCeti.dimVector_add_of_shortExact {k : Type u} {Q : Type v} [Field k] [Quiver Q] {S : CategoryTheory.ShortComplex (QuiverRep k Q)} (hS : S.ShortExact) (h₁ : ∀ (i : Q), FiniteDimensional k ↑(S.X₁.obj ((CategoryTheory.Paths.of Q).obj i))) (h₃ : ∀ (i : Q), FiniteDimensional k ↑(S.X₃.obj ((CategoryTheory.Paths.of Q).obj i))) : dimVector S.X₂ = dimVector S.X₁ + dimVector S.X₃

In a short exact sequence of pointwise finite-dimensional quiver representations, the middle dimension vector is the sum of the outer dimension vectors.

theorem TauCeti.isZero_of_dimVector_eq_zero {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (hfd : ∀ (i : Q), FiniteDimensional k ↑(M.obj ((CategoryTheory.Paths.of Q).obj i))) (h : dimVector M = 0) : CategoryTheory.Limits.IsZero M

A pointwise finite-dimensional representation with vanishing dimension vector is a zero object. Finite-dimensionality is needed: the convention making Module.finrank vanish on an infinite-dimensional space would otherwise make the dimension vector of a nonzero representation zero.

theorem TauCeti.dimVector_eq_zero_of_isZero {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (h : CategoryTheory.Limits.IsZero M) : dimVector M = 0

A zero object has vanishing dimension vector, the converse of TauCeti.isZero_of_dimVector_eq_zero; no finite-dimensionality is needed in this direction.

theorem TauCeti.dimVector_ne_zero_of_indecomposable {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (hfd : ∀ (i : Q), FiniteDimensional k ↑(M.obj ((CategoryTheory.Paths.of Q).obj i))) (hM : CategoryTheory.Indecomposable M) : dimVector M ≠ 0

A pointwise finite-dimensional indecomposable representation has nonzero dimension vector, since it is not the zero object. This is the nonvanishing half of the statement that the dimension vector of an indecomposable is a positive root.