The subspace quiver

The subspace quiver on an index type ι has a central vertex and one outer vertex for each i : ι, with a single arrow running from each outer vertex into the centre. A representation of it whose arrows act injectively is a family of subspaces of the vector space at the centre, which is where the name comes from.

Its underlying graph is the star with |ι| leaves. With three leaves this is the Dynkin diagram D₄, and the quiver is isomorphic to TauCeti.Quiver.D4; with four leaves it is the extended Dynkin diagram D4~, the graph of the classical four subspace problem, and the quiver has infinite representation type (TauCeti.RepresentationTheory.Quiver.Subspace.FiniteRepType).

This file carries the vertex and arrow data alone.

Main definitions

• TauCeti.Quiver.Subspace: the vertex type, with constructors center and outer, and a Quiver instance whose only arrows are the outer i ⟶ center.
• TauCeti.Quiver.Subspace.arrow: the arrow from an outer vertex into the centre.

References

• I. M. Gelfand, V. A. Ponomarev, Problems of linear algebra and classification of quadruples of subspaces in a finite-dimensional vector space, Colloq. Math. Soc. János Bolyai 5 (1972), 163--237.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Volume I, Chapter VII.

inductive TauCeti.Quiver.Subspace (ι : Type v) : Type v

The subspace quiver on ι: a central vertex together with one outer vertex for each i : ι, with one arrow from each outer vertex into the centre.

• center {ι : Type v} : Subspace ι

  The central vertex, the head of every arrow.

• outer {ι : Type v} (i : ι) : Subspace ι

  The outer vertex indexed by i, the tail of a single arrow.

@[instance_reducible]

instance TauCeti.Quiver.Subspace.instQuiver {ι : Type v} : Quiver (Subspace ι)

def TauCeti.Quiver.Subspace.arrow {ι : Type v} (i : ι) : outer i ⟶ center

The arrow running from the outer vertex indexed by i into the centre.

@[instance_reducible]

instance TauCeti.Quiver.Subspace.instUniqueHomOuterCenter {ι : Type v} (i : ι) : Unique (outer i ⟶ center)

instance TauCeti.Quiver.Subspace.instIsEmptyHomCenter {ι : Type v} : IsEmpty (center ⟶ center)

instance TauCeti.Quiver.Subspace.instIsEmptyHomCenterOuter {ι : Type v} (i : ι) : IsEmpty (center ⟶ outer i)

instance TauCeti.Quiver.Subspace.instIsEmptyHomOuter {ι : Type v} (i j : ι) : IsEmpty (outer i ⟶ outer j)

instance TauCeti.Quiver.Subspace.instSubsingletonHom {ι : Type v} (a b : Subspace ι) : Subsingleton (a ⟶ b)

Between any two vertices of the subspace quiver there is at most one arrow.