The D₄ quiver

The D₄ quiver has a central vertex and three outer vertices, with one arrow running from each outer vertex into the centre. Its underlying graph is the simply-laced Dynkin diagram D₄, the smallest one that is not of type A, which makes it the standard test of the positive-root count beyond type A.

This file constructs the quiver and its combinatorics: the centre is a sink and the outer vertices are sources, so the quiver is acyclic and its only nontrivial paths are the three arrows. The dimension of its path algebra is computed in TauCeti.RepresentationTheory.Quiver.D4.PathAlgebra, and its Euler and Tits forms, with the twelve positive roots they cut out, in TauCeti.RepresentationTheory.Quiver.D4.EulerForm.

Main definitions

• TauCeti.Quiver.D4: the vertex type, with constructors center and outer, and a Quiver instance whose only arrows are the three outer i ⟶ center.
• TauCeti.Quiver.D4.vertexEquiv: the vertices as Option (Fin 3), the centre being none.
• TauCeti.Quiver.D4.arrow and TauCeti.Quiver.D4.arrowPath: the arrow attached to an outer vertex, and the length-one path it traces.

Main results

• TauCeti.Quiver.D4.isSink_center and TauCeti.Quiver.D4.isSource_outer: the centre is a sink and each outer vertex is a source.
• TauCeti.Quiver.D4.isAcyclic: the quiver is acyclic, since all of its arrows run the same way.
• TauCeti.Quiver.D4.instUniquePathOuterCenter: the only path from an outer vertex to the centre is the arrow there, so the quiver has seven paths in all.

References

The orientation used here is outer i ⟶ center, with all three arrows pointing into the central sink. For background on Dynkin quivers, see Derksen--Weyman, An Introduction to Quiver Representations, and Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. II.

inductive TauCeti.Quiver.D4 : Type

The D₄ quiver: a central vertex together with three outer vertices, with one arrow from each outer vertex into the centre. Its underlying graph is the Dynkin diagram D₄.

• center : D4

  The central vertex, the head of every arrow.

• outer (i : Fin 3) : D4

  The i-th outer vertex, the tail of the i-th arrow.

@[instance_reducible]

instance TauCeti.Quiver.instDecidableEqD4 : DecidableEq D4

def TauCeti.Quiver.instDecidableEqD4.decEq (x✝ x✝¹ : D4) : Decidable (x✝ = x✝¹)

The four vertices

def TauCeti.Quiver.D4.vertexEquiv : D4 ≃ Option (Fin 3)

The vertices of the D₄ quiver as Option (Fin 3): the centre is none, and the i-th outer vertex is some i.

@[simp]

theorem TauCeti.Quiver.D4.vertexEquiv_center : vertexEquiv center = none

@[simp]

theorem TauCeti.Quiver.D4.vertexEquiv_outer (i : Fin 3) : vertexEquiv (outer i) = some i

@[simp]

theorem TauCeti.Quiver.D4.vertexEquiv_symm_none : vertexEquiv.symm none = center

@[simp]

theorem TauCeti.Quiver.D4.vertexEquiv_symm_some (i : Fin 3) : vertexEquiv.symm (some i) = outer i

@[instance_reducible]

instance TauCeti.Quiver.D4.instFintype : Fintype D4

@[simp]

theorem TauCeti.Quiver.D4.card_eq_four : Fintype.card D4 = 4

@[simp]

theorem TauCeti.Quiver.D4.sum_univ {M : Type u_1} [AddCommMonoid M] (f : D4 → M) : ∑ v : D4, f v = f center + ∑ i : Fin 3, f (outer i)

A sum over the vertices of D₄ splits into the value at the centre and a sum over the three outer vertices.

theorem TauCeti.Quiver.D4.eq_zero_iff {M : Type u_1} [Zero M] {f : D4 → M} : f = 0 ↔ f center = 0 ∧ ∀ (i : Fin 3), f (outer i) = 0

A function on the vertices vanishes exactly when all four of its values do.

The three arrows

@[instance_reducible]

instance TauCeti.Quiver.D4.instQuiver : Quiver D4

def TauCeti.Quiver.D4.arrow (i : Fin 3) : outer i ⟶ center

The arrow running from the i-th outer vertex into the centre.

@[instance_reducible]

instance TauCeti.Quiver.D4.instUniqueHomOuterCenter (i : Fin 3) : Unique (outer i ⟶ center)

instance TauCeti.Quiver.D4.instIsEmptyHomCenter : IsEmpty (center ⟶ center)

instance TauCeti.Quiver.D4.instIsEmptyHomCenterOuter (i : Fin 3) : IsEmpty (center ⟶ outer i)

instance TauCeti.Quiver.D4.instIsEmptyHomOuter (i j : Fin 3) : IsEmpty (outer i ⟶ outer j)

theorem TauCeti.Quiver.D4.isEmpty_hom_from_center (b : D4) : IsEmpty (center ⟶ b)

No arrow leaves the centre.

theorem TauCeti.Quiver.D4.isEmpty_hom_to_outer (a : D4) (i : Fin 3) : IsEmpty (a ⟶ outer i)

No arrow ends at an outer vertex.

theorem TauCeti.Quiver.D4.isSink_center : IsSink center

The centre is a sink: every arrow of D₄ ends there.

theorem TauCeti.Quiver.D4.isSource_outer (i : Fin 3) : IsSource (outer i)

Each outer vertex is a source: every arrow of D₄ starts at one.

@[instance_reducible]

instance TauCeti.Quiver.D4.instFintypeHom (a b : D4) : Fintype (a ⟶ b)

The paths

theorem TauCeti.Quiver.D4.path_center_center_eq_nil (p : Quiver.Path center center) : p = Quiver.Path.nil

The only closed path at the centre is the trivial one, the centre being a sink.

theorem TauCeti.Quiver.D4.path_outer_outer_eq_nil (i : Fin 3) (p : Quiver.Path (outer i) (outer i)) : p = Quiver.Path.nil

The only closed path at an outer vertex is the trivial one, an outer vertex being a source.

theorem TauCeti.Quiver.D4.isAcyclic : IsAcyclic D4

The D₄ quiver is acyclic: all of its arrows run into the centre.

@[instance_reducible]

instance TauCeti.Quiver.D4.instUniquePathCenter : Unique (Quiver.Path center center)

@[instance_reducible]

instance TauCeti.Quiver.D4.instUniquePathOuterSelf (i : Fin 3) : Unique (Quiver.Path (outer i) (outer i))

instance TauCeti.Quiver.D4.instIsEmptyPathCenterOuter (i : Fin 3) : IsEmpty (Quiver.Path center (outer i))

theorem TauCeti.Quiver.D4.isEmpty_path_outer_outer {i j : Fin 3} (h : i ≠ j) : IsEmpty (Quiver.Path (outer i) (outer j))

There is no path between two distinct outer vertices: a path out of an outer vertex reaches the centre and stops there.

def TauCeti.Quiver.D4.arrowPath (i : Fin 3) : Quiver.Path (outer i) center

The length-one path traced by the arrow at an outer vertex.

@[instance_reducible]

instance TauCeti.Quiver.D4.instUniquePathOuterCenter (i : Fin 3) : Unique (Quiver.Path (outer i) center)

The only path from an outer vertex to the centre is the arrow there: that arrow is the only one leaving the vertex, and nothing can be appended to it because the centre is a sink.

@[instance_reducible]

instance TauCeti.Quiver.D4.instFintypePath (a b : D4) : Fintype (Quiver.Path a b)

@[simp]

theorem TauCeti.Quiver.D4.card_path_outer_outer (i j : Fin 3) : Fintype.card (Quiver.Path (outer i) (outer j)) = if i = j then 1 else 0

The only path between two outer vertices is the trivial one at a single vertex. The other three path counts of D₄ are read off by simp from the Unique and IsEmpty instances above.