Representations of a quiver

A representation of a quiver over a field assigns a vector space to every vertex and a linear map to every arrow, compatibly with path composition. This is precisely a functor from Mathlib's free path category to its category of modules.

This file introduces the standard abbreviation, finite biproducts of representations, and the fact that the trivial path acts as the identity. It also names the vertex spaces as a family TauCeti.QuiverRep.vertexSpace indexed by the vertices, with TauCeti.QuiverRep.mapₗ the structure maps between them; that is what a construction indexed by the vertices — a direct sum, a product — needs, since instance search does not see the objects of CategoryTheory.Paths Q as vertices when it is asked for a family of instances over Q (see the implementation notes). The equivalence with modules over the path algebra is TauCeti.quiverRepEquivalence, built in TauCeti.RepresentationTheory.Quiver.Representation.AsModule.

Implementation notes

A representation is a functor out of CategoryTheory.Paths Q, whose objects are vertices only after unfolding the semireducible CategoryTheory.Paths. Instance search does not see through that when it is asked for the family ∀ v : Q, AddCommMonoid (M.obj v), although it succeeds at each individual vertex; naming the family as TauCeti.QuiverRep.vertexSpace and giving it its two instances by inferInstanceAs is what makes such a family usable.

References

This implements the category-of-representations part of Layer 1 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md.

@[reducible, inline]

abbrev TauCeti.QuiverRep (k : Type u) (Q : Type v) [Field k] [Quiver Q] : Type (max (max v u_1) u_2 v u (u_2 + 1))

The category of representations of a quiver Q over a field k.

Equations

• TauCeti.QuiverRep k Q = CategoryTheory.Functor (CategoryTheory.Paths Q) (ModuleCat k)

instance TauCeti.instHasFiniteBiproductsQuiverRep {k : Type u} {Q : Type v} [Field k] [Quiver Q] : CategoryTheory.Limits.HasFiniteBiproducts (QuiverRep k Q)

Representations of a quiver have finite biproducts, computed vertexwise.

@[simp]

theorem TauCeti.QuiverRep.map_nil {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) (a : Q) : M.map Quiver.Path.nil = CategoryTheory.CategoryStruct.id (M.obj a)

The trivial path acts as the identity. In the free path category Quiver.Path.nil is the identity morphism, so a representation carries it to the identity map. Stated separately because Quiver.Path.nil is what appears when a path is taken apart, while CategoryTheory.Functor.map_id is phrased in terms of 𝟙: the two agree only by unfolding the semireducible CategoryTheory.Paths, so simp only [Functor.map_id] makes no progress on a goal about Quiver.Path.nil, and simp cannot compute the action of the trivial path without this lemma. Mathlib states the same restatement for functors of the form CategoryTheory.Paths.lift φ, as CategoryTheory.Paths.lift_nil; that lemma does not apply to a general representation.

theorem TauCeti.QuiverRep.map_nil_apply {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) (a : Q) (x : ↑(M.obj a)) : (CategoryTheory.ConcreteCategory.hom (M.map Quiver.Path.nil)) x = x

The element-level form of TauCeti.QuiverRep.map_nil: the trivial path fixes every vector.

def TauCeti.QuiverRep.vertexSpace (k : Type u) (Q : Type v) [Field k] [Quiver Q] (M : QuiverRep k Q) (v : Q) : Type t

The vertex space, as a bare type indexed by the vertices.

Equations

• TauCeti.QuiverRep.vertexSpace k Q M v = ↑(M.obj v)

@[instance_reducible]

instance TauCeti.QuiverRep.instAddCommGroupVertexSpace (k : Type u) (Q : Type v) [Field k] [Quiver Q] (M : QuiverRep k Q) (v : Q) : AddCommGroup (vertexSpace k Q M v)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.QuiverRep.instModuleVertexSpace (k : Type u) (Q : Type v) [Field k] [Quiver Q] (M : QuiverRep k Q) (v : Q) : Module k (vertexSpace k Q M v)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.QuiverRep.mapₗ (k : Type u) (Q : Type v) [Field k] [Quiver Q] (M : QuiverRep k Q) {a b : Q} (p : Quiver.Path a b) : vertexSpace k Q M a →ₗ[k] vertexSpace k Q M b

The structure map of a representation along a path, retyped between vertex spaces.

@[expose] is load-bearing rather than a leak: a goal about a vertex-indexed construction that has been unfolded to the underlying ModuleCat morphisms — as the naturality square of TauCeti.QuiverRep.asModuleIso is — only matches this once the body is visible.

Equations

• TauCeti.QuiverRep.mapₗ k Q M p = ModuleCat.Hom.hom (M.map p)

theorem TauCeti.QuiverRep.mapₗ_apply (k : Type u) (Q : Type v) [Field k] [Quiver Q] (M : QuiverRep k Q) {a b : Q} (p : Quiver.Path a b) (z : vertexSpace k Q M a) : (mapₗ k Q M p) z = (CategoryTheory.ConcreteCategory.hom (M.map p)) z

The retyped structure map is the structure map.

@[simp]

theorem TauCeti.QuiverRep.mapₗ_nil (k : Type u) (Q : Type v) [Field k] [Quiver Q] (M : QuiverRep k Q) (a : Q) : mapₗ k Q M Quiver.Path.nil = LinearMap.id

The trivial path acts as the identity, the element-level TauCeti.QuiverRep.map_nil_apply read as an equation of linear maps.

theorem TauCeti.QuiverRep.mapₗ_comp (k : Type u) (Q : Type v) [Field k] [Quiver Q] (M : QuiverRep k Q) {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path b c) : mapₗ k Q M (p.comp q) = mapₗ k Q M q ∘ₗ mapₗ k Q M p

Concatenation of paths composes the structure maps, the functoriality of a representation read on the retyped maps.