Iterating the reflection of a quiver along a list of vertices

Reflecting a quiver at a vertex reverses the arrows meeting that vertex. Iterating a reflection changes the quiver, not the vertex type, so the carrier here is the quiver structure rather than the type synonym TauCeti.Quiver.Reflect: the reflection at the second vertex has to be taken with respect to the structure produced by the first. Accordingly TauCeti.Quiver.reflectAt repackages TauCeti.Quiver.reflectHom as an operation on Quiver structures on a fixed vertex type — it has the arrows of Reflect V i, by TauCeti.Quiver.hom_reflectAt_eq_hom_reflect — and TauCeti.Quiver.reflectList folds it along a list.

Main definitions

• TauCeti.Quiver.reflectAt: reflection at a vertex, as an operation on quiver structures.
• TauCeti.Quiver.reflectList: reflection at each vertex of a list, in order.
• TauCeti.Quiver.fintypeHomReflectList: arrow-finiteness transported along reflectList, the iterated counterpart of TauCeti.Quiver.instFintypeReflectHom.

Main results

• TauCeti.Quiver.reflectAt_reflectAt: reflecting twice at the same vertex returns the quiver structure it started from.
• TauCeti.Quiver.reflectList_reverse_reflectList: reflecting along a list and then along its reverse returns the original quiver structure.
• Quiver.nonempty_reflectList_sum_hom_equiv: reflecting along any list keeps the arrows joining two vertices in either direction, so it changes the orientation of a quiver but not its underlying multigraph.
• TauCeti.Quiver.hom_reflectList and TauCeti.Quiver.hom_reflectList_of_not_iff: reflecting along a repetition-free list reverses exactly the arrows joining a vertex of the list to a vertex outside it.
• TauCeti.Quiver.reflectList_eq_self: reflecting once at every vertex restores the original quiver structure, with TauCeti.Quiver.hom_reflectList_of_forall_mem the same statement on arrow types.

Implementation notes

All three definitions are @[expose]d. A module that iterates the reflection of representations needs the reductions reflectList q (i :: l) = reflectList (reflectAt q i) l and (a ⟶ b) = TauCeti.Quiver.reflectHom i a b in reflectAt q i to hold definitionally, so that a recursive construction typechecks against the quiver structure its predecessor produced; the same goes for the recursion of fintypeHomReflectList along the list.

References

The lists along which this iteration is sink-admissible are studied in TauCeti.RepresentationTheory.Quiver.Reflection.Admissible. A sink-admissible list may be empty, may repeat a vertex and need not exhaust the vertices; it is along a sink-admissible ordering — a sink-admissible list that is repetition-free and contains every vertex — that the reflection functors compose into the Coxeter functor. See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem.

Reflection as an operation on quiver structures

@[instance_reducible]

noncomputable def TauCeti.Quiver.reflectAt {V : Type u} (q : Quiver V) (i : V) : Quiver V

Reflection at the vertex i, as an operation on the quiver structures carried by a fixed vertex type: reflectAt q i has the arrows of q with every arrow incident to i reversed. Unlike the type synonym TauCeti.Quiver.Reflect, this form iterates, which is what a sequence of reflections needs.

@[simp]

theorem TauCeti.Quiver.hom_reflectAt {V : Type u} (q : Quiver V) (i a b : V) : (a ⟶ b) = reflectHom i a b

The arrows of reflectAt q i are the ones computed by TauCeti.Quiver.reflectHom.

theorem TauCeti.Quiver.hom_reflectAt_eq_hom_reflect {V : Type u} [q : Quiver V] (i a b : V) : (a ⟶ b) = (a ⟶ b)

reflectAt reproduces the quiver carried by the type synonym TauCeti.Quiver.Reflect.

theorem TauCeti.Quiver.IsSink.isSource_reflectAt {V : Type u} {q : Quiver V} {i : V} (h : IsSink i) : IsSource i

A sink becomes a source after reflecting the quiver at that vertex.

theorem TauCeti.Quiver.IsSource.isSink_reflectAt {V : Type u} {q : Quiver V} {i : V} (h : IsSource i) : IsSink i

A source becomes a sink after reflecting the quiver at that vertex.

@[simp]

theorem TauCeti.Quiver.reflectAt_reflectAt {V : Type u} (q : Quiver V) (i : V) : reflectAt (reflectAt q i) i = q

Reflection at a vertex is an involution. Reflecting twice at the same vertex reverses the arrows meeting it twice, returning the quiver structure it started from. Since reflectAt carries the arrows of the type synonym TauCeti.Quiver.Reflect, the arrow types agree by TauCeti.Quiver.hom_reflect_reflect.

Reflecting along a list of vertices

@[instance_reducible]

noncomputable def TauCeti.Quiver.reflectList {V : Type u} (q : Quiver V) (l : List V) : Quiver V

Reflection at each vertex of a list in turn, starting from the head.

@[simp]

theorem TauCeti.Quiver.reflectList_nil {V : Type u} (q : Quiver V) : reflectList q [] = q

@[simp]

theorem TauCeti.Quiver.reflectList_cons {V : Type u} (q : Quiver V) (i : V) (l : List V) : reflectList q (i :: l) = reflectList (reflectAt q i) l

@[simp]

theorem TauCeti.Quiver.reflectList_append {V : Type u} (q : Quiver V) (l₁ l₂ : List V) : reflectList q (l₁ ++ l₂) = reflectList (reflectList q l₁) l₂

Reflecting along a concatenation is reflecting along the two segments in turn, which is how an ordering is split into an already reflected initial segment and the entries still to come.

@[simp]

theorem TauCeti.Quiver.reflectList_reverse_reflectList {V : Type u} (q : Quiver V) (l : List V) : reflectList (reflectList q l) l.reverse = q

Reflecting along a list and then along its reverse returns the original quiver structure.

@[instance_reducible]

noncomputable def TauCeti.Quiver.fintypeHomReflectList {V : Type u} (l : List V) (q : Quiver V) (_hq : (a b : V) → Fintype (a ⟶ b)) (a b : V) : Fintype (a ⟶ b)

The arrows of an iteratively reflected quiver are finite in number whenever those of the original one are: reflection only reverses arrows. This is the iterated counterpart of TauCeti.Quiver.instFintypeReflectHom, recursive along the list because the reflection at each vertex is taken with respect to the structure the previous one produced.

The underlying multigraph

theorem Quiver.nonempty_reflectAt_sum_hom_equiv {V : Type u} (q : Quiver V) (i a b : V) : Nonempty ((a ⟶ b) ⊕ (b ⟶ a) ≃ (a ⟶ b) ⊕ (b ⟶ a))

Reflection at a vertex keeps the arrows joining two vertices, only redistributing them between the two directions: the arrows running from a to b or from b to a are the same before and after the reflection.

theorem Quiver.nonempty_reflectList_sum_hom_equiv {V : Type u} (q : Quiver V) (l : List V) (a b : V) : Nonempty ((a ⟶ b) ⊕ (b ⟶ a) ≃ (a ⟶ b) ⊕ (b ⟶ a))

Reflection along any list keeps the underlying multigraph: the arrows joining two vertices, in either direction, are the same before and after the reflections.

Reflecting along a repetition-free list

theorem TauCeti.Quiver.hom_reflectList {V : Type u} (q : Quiver V) {l : List V} (hl : l.Nodup) {a b : V} (h : a ∈ l ↔ b ∈ l) : (a ⟶ b) = (a ⟶ b)

Reflecting along a repetition-free list. An arrow joining two vertices that are both on the list, or both off it, survives: each of its ends is reversed the same number of times.

theorem TauCeti.Quiver.hom_reflectList_of_not_iff {V : Type u} (q : Quiver V) {l : List V} (hl : l.Nodup) {a b : V} (h : ¬(a ∈ l ↔ b ∈ l)) : (a ⟶ b) = (b ⟶ a)

Reflecting along a repetition-free list reverses the arrows joining a vertex of the list to a vertex outside it: exactly one of the two ends is met by a reflection.

theorem TauCeti.Quiver.hom_reflectList_of_forall_mem {V : Type u} (q : Quiver V) {l : List V} (hl : l.Nodup) (hall : ∀ (v : V), v ∈ l) (a b : V) : (a ⟶ b) = (a ⟶ b)

Reflecting once at every vertex restores the quiver. Both ends of every arrow are met by a reflection, so every arrow is reversed twice. This is the arrow-type form; the equality of quiver structures itself is TauCeti.Quiver.reflectList_eq_self.

theorem TauCeti.Quiver.reflectList_eq_self {V : Type u} (q : Quiver V) {l : List V} (hl : l.Nodup) (hall : ∀ (v : V), v ∈ l) : reflectList q l = q

Reflecting once at every vertex returns the quiver structure it started from. In particular the composite of the reflections along a full sink-admissible ordering — the combinatorial shadow of the Coxeter functor — is an operation from the quiver to itself, not to some other orientation.