The extended Dynkin quiver of type D~

For m : ℕ, the quiver TauCeti.Quiver.AffineD m has a spine of m + 1 vertices spine 0 → spine 1 → ⋯ → spine m, joined by one arrow from each spine vertex to the next, and four leaves: the leaves 0 and 1 each carry one arrow into the first spine vertex spine 0, and the leaves 2 and 3 each carry one arrow into the last spine vertex spine m. Its underlying graph is the extended Dynkin diagram D~ₘ₊₄, on m + 5 vertices, in one fixed orientation. For m = 0 the spine is a single vertex receiving all four arrows, and the quiver is the four subspace quiver TauCeti.Quiver.Subspace (Fin 4) of the extended Dynkin diagram D~₄.

This file carries the vertex and arrow data, and the shape of the underlying graph: it is a tree, with at most one arrow between any two vertices, because every vertex is the source of at most one arrow and every arrow moves towards spine m. The representation theory, that the quiver has infinite representation type, is in TauCeti.RepresentationTheory.Quiver.AffineD.FiniteRepType.

Main definitions

• TauCeti.Quiver.AffineD: the vertex type, with constructors leaf and spine, and a Quiver instance.
• TauCeti.Quiver.AffineD.vertexEquiv: the vertices as Fin 4 ⊕ Fin (m + 1), so that there are m + 5 of them (TauCeti.Quiver.AffineD.card_eq).
• TauCeti.Quiver.AffineD.leafTarget: the spine vertex a leaf is attached to.
• TauCeti.Quiver.AffineD.leafArrow and TauCeti.Quiver.AffineD.spineArrow: the arrow from a leaf into the spine, and the arrow from a spine vertex to the next one.

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Volume I, Chapter VII.
• H. Derksen, J. Weyman, An Introduction to Quiver Representations, Chapter 4.

inductive TauCeti.Quiver.AffineD (m : ℕ) : Type

The extended Dynkin quiver D~ₘ₊₄: a spine of m + 1 vertices with an arrow from each to the next, and four leaves, two attached by an arrow into each end of the spine.

• leaf {m : ℕ} (i : Fin 4) : AffineD m

  The leaf indexed by i, the tail of a single arrow into an end of the spine.

• spine {m : ℕ} (j : Fin (m + 1)) : AffineD m

  The spine vertex indexed by j.

@[instance_reducible]

instance TauCeti.Quiver.instDecidableEqAffineD {m✝ : ℕ} : DecidableEq (AffineD m✝)

def TauCeti.Quiver.instDecidableEqAffineD.decEq {m✝ : ℕ} (x✝ x✝¹ : AffineD m✝) : Decidable (x✝ = x✝¹)

The m + 5 vertices

def TauCeti.Quiver.AffineD.vertexEquiv (m : ℕ) : AffineD m ≃ Fin 4 ⊕ Fin (m + 1)

The vertices of TauCeti.Quiver.AffineD m as Fin 4 ⊕ Fin (m + 1): the leaves on the left, the spine on the right.

@[simp]

theorem TauCeti.Quiver.AffineD.vertexEquiv_leaf {m : ℕ} (i : Fin 4) : (vertexEquiv m) (leaf i) = Sum.inl i

Leaves correspond to the left summand of the vertex coordinates.

@[simp]

theorem TauCeti.Quiver.AffineD.vertexEquiv_spine {m : ℕ} (j : Fin (m + 1)) : (vertexEquiv m) (spine j) = Sum.inr j

Spine vertices correspond to the right summand of the vertex coordinates.

@[simp]

theorem TauCeti.Quiver.AffineD.vertexEquiv_symm_inl {m : ℕ} (i : Fin 4) : (vertexEquiv m).symm (Sum.inl i) = leaf i

The left summand of the vertex coordinates gives a leaf.

@[simp]

theorem TauCeti.Quiver.AffineD.vertexEquiv_symm_inr {m : ℕ} (j : Fin (m + 1)) : (vertexEquiv m).symm (Sum.inr j) = spine j

The right summand of the vertex coordinates gives a spine vertex.

@[instance_reducible]

instance TauCeti.Quiver.AffineD.instFintype {m : ℕ} : Fintype (AffineD m)

@[simp]

theorem TauCeti.Quiver.AffineD.card_eq {m : ℕ} : Fintype.card (AffineD m) = m + 5

TauCeti.Quiver.AffineD m has m + 5 vertices, as the extended Dynkin diagram D~ₘ₊₄ should.

The arrows

def TauCeti.Quiver.AffineD.leafTarget (m : ℕ) (i : Fin 4) : Fin (m + 1)

The spine vertex a leaf is attached to: the first one for the leaves 0 and 1, the last one for the leaves 2 and 3.

@[simp]

theorem TauCeti.Quiver.AffineD.leafTarget_of_lt_two {m : ℕ} (i : Fin 4) (h : ↑i < 2) : leafTarget m i = 0

Leaves with index less than two attach to the first spine vertex.

@[simp]

theorem TauCeti.Quiver.AffineD.leafTarget_of_not_lt_two {m : ℕ} (i : Fin 4) (h : ¬↑i < 2) : leafTarget m i = Fin.last m

Leaves with index not less than two attach to the last spine vertex.

@[instance_reducible]

instance TauCeti.Quiver.AffineD.instQuiver {m : ℕ} : Quiver (AffineD m)

The arrows are from each leaf to its endpoint leafTarget m i, and from each spine vertex to the next. All other hom types are empty.

def TauCeti.Quiver.AffineD.leafArrow (m : ℕ) (i : Fin 4) : leaf i ⟶ spine (leafTarget m i)

The arrow from the leaf indexed by i into the spine vertex it is attached to.

def TauCeti.Quiver.AffineD.spineArrow {m : ℕ} (j : Fin m) : spine j.castSucc ⟶ spine j.succ

The arrow from the spine vertex indexed by j to the next one.

instance TauCeti.Quiver.AffineD.instIsEmptyHomLeaf {m : ℕ} (i i' : Fin 4) : IsEmpty (leaf i ⟶ leaf i')

instance TauCeti.Quiver.AffineD.instIsEmptyHomSpineLeaf {m : ℕ} (j : Fin (m + 1)) (i : Fin 4) : IsEmpty (spine j ⟶ leaf i)

@[simp]

theorem TauCeti.Quiver.AffineD.not_nonempty_hom_leaf {m : ℕ} (a : AffineD m) (i : Fin 4) : ¬Nonempty (a ⟶ leaf i)

No arrow has a leaf as its target.

@[simp]

theorem TauCeti.Quiver.AffineD.nonempty_leaf_spine_iff {m : ℕ} (i : Fin 4) (j : Fin (m + 1)) : Nonempty (leaf i ⟶ spine j) ↔ j = leafTarget m i

A leaf has an arrow precisely to its designated spine endpoint.

@[simp]

theorem TauCeti.Quiver.AffineD.nonempty_spine_spine_iff {m : ℕ} (j j' : Fin (m + 1)) : Nonempty (spine j ⟶ spine j') ↔ ↑j' = ↑j + 1

Spine arrows join precisely consecutive vertices, in increasing order.

instance TauCeti.Quiver.AffineD.instSubsingletonHom {m : ℕ} (a b : AffineD m) : Subsingleton (a ⟶ b)

Between any two vertices of TauCeti.Quiver.AffineD m there is at most one arrow.

The underlying graph

theorem TauCeti.Quiver.AffineD.isAcyclic_underlyingGraph {m : ℕ} : (underlyingGraph (AffineD m)).IsAcyclic

The underlying graph of TauCeti.Quiver.AffineD m is acyclic, so it is the tree D~ₘ₊₄.

theorem TauCeti.Quiver.AffineD.subsingleton_hom_sum {m : ℕ} (a b : AffineD m) : Subsingleton ((a ⟶ b) ⊕ (b ⟶ a))

Two vertices of TauCeti.Quiver.AffineD m are joined by at most one arrow, counted in both directions.