Sink-admissible orderings of the vertices of a quiver

Reflecting a quiver at a sink reverses the arrows meeting that vertex. Composing several such reflections calls for a list of vertices that is sink-admissible: each entry must be a sink of the quiver obtained by reflecting at all the entries preceding it, the iterated reflection TauCeti.Quiver.reflectList of TauCeti.RepresentationTheory.Quiver.Reflection.Iterate. This file constructs such an ordering for every finite acyclic quiver.

Main definitions

• TauCeti.Quiver.IsSinkAdmissible: a list of vertices each of which is a sink of the quiver reflected at its predecessors.

Main results

• TauCeti.Quiver.IsAcyclic.exists_isSinkAdmissible: a finite acyclic quiver has a repetition-free sink-admissible ordering of all of its vertices.
• TauCeti.Quiver.isSinkAdmissible_of_pairwise: a repetition-free list along which no arrow runs forwards, whose entries carry no loop and emit no arrow off the list, is sink-admissible, with TauCeti.Quiver.isSinkAdmissible_of_pairwise_of_forall_mem the case of a list of all the vertices, where the last hypothesis — that no arrow leaves the list — is automatic.
• TauCeti.Quiver.IsSinkAdmissible.isEmpty_hom_self: no vertex of a repetition-free sink-admissible list carries a loop.

References

This is the admissible-ordering milestone opening Layer 5 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, the input the Coxeter functor of Layer 4 is assembled from. See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, VII.5.

Sink-admissible lists

def TauCeti.Quiver.IsSinkAdmissible {V : Type u} (q : Quiver V) (l : List V) : Prop

A list of vertices is sink-admissible for the quiver structure q when each of its entries is a sink of the quiver obtained by reflecting q at all the entries preceding it. This is the hypothesis under which the reflection functors at the successive entries can be composed at all; the composite is the Coxeter functor when the list is in addition repetition-free and contains every vertex, in which case the reflections carry q back to itself by TauCeti.Quiver.reflectList_eq_self.

Equations

• TauCeti.Quiver.IsSinkAdmissible q l = ∀ (t u : List V) (i : V), l = t ++ i :: u → TauCeti.Quiver.IsSink i

theorem TauCeti.Quiver.isSinkAdmissible_def {V : Type u} (q : Quiver V) (l : List V) : IsSinkAdmissible q l ↔ ∀ (t u : List V) (i : V), l = t ++ i :: u → IsSink i

The defining condition for a sink-admissible list.

@[simp]

theorem TauCeti.Quiver.isSinkAdmissible_nil {V : Type u} (q : Quiver V) : IsSinkAdmissible q []

@[simp]

theorem TauCeti.Quiver.isSinkAdmissible_cons {V : Type u} {q : Quiver V} {i : V} {l : List V} : IsSinkAdmissible q (i :: l) ↔ IsSink i ∧ IsSinkAdmissible (reflectAt q i) l

A list is sink-admissible exactly when its head is a sink and its tail is sink-admissible for the quiver reflected at that head.

Recognising a sink-admissible ordering

theorem TauCeti.Quiver.isSinkAdmissible_of_pairwise {V : Type u} (q : Quiver V) {l : List V} (hnd : l.Nodup) (hloop : ∀ x ∈ l, IsEmpty (x ⟶ x)) (hp : List.Pairwise (fun (x y : V) => IsEmpty (x ⟶ y)) l) (hout : ∀ x ∈ l, ∀ b ∉ l, IsEmpty (x ⟶ b)) : IsSinkAdmissible q l

A topological ordering is sink-admissible. If l repeats no vertex, no entry of l carries a loop, no arrow runs from an earlier entry of l to a later one — equivalently, the target of such an arrow precedes its source — and no arrow leaves l for a vertex outside it, then each entry is a sink once its predecessors have been reflected. The list need not exhaust the vertices; TauCeti.Quiver.isSinkAdmissible_of_pairwise_of_forall_mem is the case where it does, in which the last hypothesis is vacuous.

theorem TauCeti.Quiver.isSinkAdmissible_of_pairwise_of_forall_mem {V : Type u} (q : Quiver V) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hloop : ∀ (v : V), IsEmpty (v ⟶ v)) (hp : List.Pairwise (fun (x y : V) => IsEmpty (x ⟶ y)) l) : IsSinkAdmissible q l

A repetition-free list of all the vertices along which no arrow runs forwards, no vertex carrying a loop, is sink-admissible: this is the case of TauCeti.Quiver.isSinkAdmissible_of_pairwise in which nothing lies outside the list, so no arrow can leave it. Such a list is a sink-admissible ordering, the input the Coxeter functor is assembled from.

Loops along a sink-admissible ordering

theorem TauCeti.Quiver.IsSinkAdmissible.isEmpty_hom_self {V : Type u} {q : Quiver V} {l : List V} (hnd : l.Nodup) (hl : IsSinkAdmissible q l) {i : V} (hi : i ∈ l) : IsEmpty (i ⟶ i)

No vertex of a repetition-free sink-admissible list carries a loop. At its own stage the vertex is a sink of the reflected quiver, so it carries no loop there; and reflecting along a repetition-free prefix leaves the loops at any vertex alone (TauCeti.Quiver.hom_reflectList), because both ends of a loop lie on the same side of the prefix. This is the looplessness hypothesis under which the composite of the simple reflections along the list preserves the Tits form.

Existence for a finite acyclic quiver

theorem TauCeti.Quiver.IsAcyclic.exists_isSinkAdmissible {V : Type u} [q : Quiver V] [Finite V] (h : IsAcyclic V) : ∃ (l : List V), l.Nodup ∧ (∀ (v : V), v ∈ l) ∧ IsSinkAdmissible q l

Every finite acyclic quiver has a sink-admissible ordering of its vertices: a list without repetitions containing every vertex, each entry of which is a sink once its predecessors have been reflected. This is what lets the reflection functors at the successive vertices be composed into the Coxeter functor, and by TauCeti.Quiver.reflectList_eq_self the composite returns to the original quiver.