Sink- and source-admissible lists of 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.

Dually, a list is source-admissible when each entry is a source after reflecting at its predecessors. Reversing an admissible list gives a list admissible for the opposite kind of vertex in the quiver obtained after all the reflections.

Main definitions

• TauCeti.Quiver.IsSinkAdmissible: a list of vertices each of which is a sink of the quiver reflected at its predecessors.
• TauCeti.Quiver.IsSourceAdmissible: a list of vertices each of which is a source 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.
• TauCeti.Quiver.IsSinkAdmissible.isSourceAdmissible_reverse and TauCeti.Quiver.IsSourceAdmissible.isSinkAdmissible_reverse: reversing an admissible list gives a list admissible for the opposite kind of vertex in the fully reflected quiver.

References

Admissible orderings are the input the Coxeter functor 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.

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.

@[simp]

theorem TauCeti.Quiver.isSinkAdmissible_append {V : Type u} {q : Quiver V} {l₁ l₂ : List V} : IsSinkAdmissible q (l₁ ++ l₂) ↔ IsSinkAdmissible q l₁ ∧ IsSinkAdmissible (reflectList q l₁) l₂

A concatenation is sink-admissible exactly when its first segment is sink-admissible and its second segment is sink-admissible after reflecting along the first.

theorem TauCeti.Quiver.IsSinkAdmissible.append_singleton {V : Type u} {q : Quiver V} {l : List V} {i : V} (hl : IsSinkAdmissible q l) (hi : IsSink i) : IsSinkAdmissible q (l ++ [i])

Appending a final sink to a sink-admissible list preserves sink-admissibility.

Source-admissible lists

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

A list of vertices is source-admissible when each entry is a source in the quiver obtained by reflecting at all preceding entries.

theorem TauCeti.Quiver.isSourceAdmissible_def {V : Type u} (q : Quiver V) (l : List V) : IsSourceAdmissible q l ↔ ∀ (t u : List V) (i : V), l = t ++ i :: u → IsSource i

The defining condition for a source-admissible list.

@[simp]

theorem TauCeti.Quiver.isSourceAdmissible_nil {V : Type u} (q : Quiver V) : IsSourceAdmissible q []

@[simp]

theorem TauCeti.Quiver.isSourceAdmissible_cons {V : Type u} {q : Quiver V} {i : V} {l : List V} : IsSourceAdmissible q (i :: l) ↔ IsSource i ∧ IsSourceAdmissible (reflectAt q i) l

A list is source-admissible exactly when its head is a source and its tail is source-admissible after reflecting at the head.

@[simp]

theorem TauCeti.Quiver.isSourceAdmissible_append {V : Type u} {q : Quiver V} {l₁ l₂ : List V} : IsSourceAdmissible q (l₁ ++ l₂) ↔ IsSourceAdmissible q l₁ ∧ IsSourceAdmissible (reflectList q l₁) l₂

A concatenation is source-admissible exactly when its first segment is source-admissible and its second segment is source-admissible after reflecting along the first.

theorem TauCeti.Quiver.IsSourceAdmissible.append_singleton {V : Type u} {q : Quiver V} {l : List V} {i : V} (hl : IsSourceAdmissible q l) (hi : IsSource i) : IsSourceAdmissible q (l ++ [i])

Appending a final source to a source-admissible list preserves source-admissibility.

theorem TauCeti.Quiver.IsSinkAdmissible.isSourceAdmissible_reverse {V : Type u} {q : Quiver V} {l : List V} (hl : IsSinkAdmissible q l) : IsSourceAdmissible (reflectList q l) l.reverse

A reversed sink-admissible list is source-admissible. After all sink reflections have been performed, undoing them in reverse order always reflects at a source.

theorem TauCeti.Quiver.IsSourceAdmissible.isSinkAdmissible_reverse {V : Type u} {q : Quiver V} {l : List V} (hl : IsSourceAdmissible q l) : IsSinkAdmissible (reflectList q l) l.reverse

A reversed source-admissible list is sink-admissible. After all source reflections have been performed, undoing them in reverse order always reflects at a sink.

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.