The Hom differential of quiver representations

The Hom differential sends a family of vertex maps fᵢ : Mᵢ → Nᵢ to the arrowwise commutativity defects N(a) fᵢ - fⱼ M(a). Its kernel is the space of representation morphisms. For finite-dimensional representations of a finite quiver, the difference between the dimensions of its kernel and cokernel is the Euler form.

The cokernel measures the obstruction to making vertexwise splittings of extensions compatible with the arrows. The constructions here require no acyclicity assumption.

References

H. Derksen and J. Weyman, An Introduction to Quiver Representations, Chapter 1, for the vertex-and-arrow Hom differential and the Euler form.

@[reducible, inline]

abbrev TauCeti.QuiverRep.HomVertex {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) : Type (max v t)

Families of linear maps between corresponding vertex spaces.

noncomputable def TauCeti.QuiverRep.homVertex {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) (f : M ⟶ N) : M.HomVertex N

The vertex components of a morphism of representations, retyped between vertex spaces.

theorem TauCeti.QuiverRep.homVertex_apply {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) (f : M ⟶ N) (i : Q) (x : vertexSpace k Q M i) : (M.homVertex N f i) x = (ModuleCat.Hom.hom (f.app ((CategoryTheory.Paths.of Q).obj i))) x

The vertex family of a morphism evaluates to its components.

theorem TauCeti.QuiverRep.homVertex_naturality {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) (f : M ⟶ N) (i j : Q) (a : i ⟶ j) (x : vertexSpace k Q M i) : (M.homVertex N f j) ((mapₗ k Q M a.toPath) x) = (mapₗ k Q N a.toPath) ((M.homVertex N f i) x)

The vertex components of a morphism commute with each arrow action.

@[reducible, inline]

abbrev TauCeti.QuiverRep.HomArrow {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) : Type (max (max v w) t)

Families of linear maps from the source space of each arrow to its target space.

noncomputable def TauCeti.QuiverRep.homDifferential {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) : M.HomVertex N →ₗ[k] M.HomArrow N

The arrowwise commutativity defect of a family of vertex maps.

@[simp]

theorem TauCeti.QuiverRep.homDifferential_apply {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) (f : M.HomVertex N) {i j : Q} (a : i ⟶ j) : (M.homDifferential N) f i j a = mapₗ k Q N a.toPath ∘ₗ f i - f j ∘ₗ mapₗ k Q M a.toPath

Evaluation of the Hom differential on an arrow.

@[simp]

theorem TauCeti.QuiverRep.homDifferential_eq_zero_iff {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) (f : M.HomVertex N) : (M.homDifferential N) f = 0 ↔ ∀ (i j : Q) (a : i ⟶ j), mapₗ k Q N a.toPath ∘ₗ f i = f j ∘ₗ mapₗ k Q M a.toPath

The Hom differential vanishes precisely when the vertex maps commute with every arrow.

noncomputable def TauCeti.QuiverRep.homEquivKerDifferential {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) : (M ⟶ N) ≃ₗ[k] ↥(M.homDifferential N).ker

The kernel of the Hom differential is the space of representation morphisms.

@[simp]

theorem TauCeti.QuiverRep.homEquivKerDifferential_apply {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) (f : M ⟶ N) (i : Q) : ↑((M.homEquivKerDifferential N) f) i = ModuleCat.Hom.hom (f.app i)

The kernel identification sends a morphism to its vertex components.

@[simp]

theorem TauCeti.QuiverRep.homEquivKerDifferential_symm_apply {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) (f : ↥(M.homDifferential N).ker) (i : Q) : ((M.homEquivKerDifferential N).symm f).app i = ModuleCat.ofHom (↑f i)

The inverse kernel identification has the prescribed vertex components.

theorem TauCeti.QuiverRep.finiteDimensional_hom {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} [Finite Q] (hM : IsFinDim k Q M) (hN : IsFinDim k Q N) : FiniteDimensional k (M ⟶ N)

Morphisms between pointwise finite-dimensional representations of a quiver with finitely many vertices form a finite-dimensional vector space. No finiteness of the arrows is needed.

theorem TauCeti.QuiverRep.eulerForm_eq_finrank_homVertex_sub_finrank_homArrow {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (hM : ∀ (i : Q), FiniteDimensional k ↑(M.obj i)) (hN : ∀ (i : Q), FiniteDimensional k ↑(N.obj i)) : (((eulerForm Q) fun (i : Q) => ↑(dimVector M i)) fun (i : Q) => ↑(dimVector N i)) = ↑(Module.finrank k (M.HomVertex N)) - ↑(Module.finrank k (M.HomArrow N))

The Euler form is the vertex-map dimension minus the arrow-map dimension.

theorem TauCeti.QuiverRep.eulerForm_eq_finrank_hom_sub_finrank_coker {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (hM : ∀ (i : Q), FiniteDimensional k ↑(M.obj i)) (hN : ∀ (i : Q), FiniteDimensional k ↑(N.obj i)) : (((eulerForm Q) fun (i : Q) => ↑(dimVector M i)) fun (i : Q) => ↑(dimVector N i)) = ↑(Module.finrank k (M ⟶ N)) - ↑(Module.finrank k (M.HomArrow N ⧸ (M.homDifferential N).range))

The Euler form is the morphism dimension minus the cokernel dimension of the Hom differential.

theorem TauCeti.QuiverRep.homDifferential_surjective_iff {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M N : QuiverRep k Q) [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (hM : ∀ (i : Q), FiniteDimensional k ↑(M.obj i)) (hN : ∀ (i : Q), FiniteDimensional k ↑(N.obj i)) : Function.Surjective ⇑(M.homDifferential N) ↔ (((eulerForm Q) fun (i : Q) => ↑(dimVector M i)) fun (i : Q) => ↑(dimVector N i)) = ↑(Module.finrank k (M ⟶ N))

Surjectivity of the Hom differential is detected by equality between the Euler form and the dimension of the morphism space.