Sinks, sources, and the reflection of a quiver at a vertex

Reflecting a quiver V at a vertex i reverses every arrow incident to i and leaves the remaining arrows alone. This is the change of orientation underlying the Bernstein-Gelfand-Ponomarev reflection functors, which carry representations of V to representations of the reflected quiver.

The reflected quiver is TauCeti.Quiver.Reflect V i, a type synonym for the vertex type V carrying the reversed arrows; its arrow types are computed by TauCeti.Quiver.reflectHom. Reflection is applied at a sink (a vertex with no outgoing arrow) or, dually, at a source, and it exchanges the two: reflecting at a sink turns it into a source (TauCeti.Quiver.IsSink.isSource_reflect). Preservation of acyclicity and the existence of sinks and sources in finite acyclic quivers are proved in TauCeti.RepresentationTheory.Quiver.Reflection.Acyclic.

Main definitions

• TauCeti.Quiver.IsSink, TauCeti.Quiver.IsSource: a vertex with no outgoing, respectively no incoming, arrow.
• TauCeti.Quiver.reflectHom: the arrow types of the quiver obtained by reversing every arrow incident to a given vertex.
• TauCeti.Quiver.Reflect: that quiver, on the same vertex type.
• TauCeti.Quiver.reflectArrow and TauCeti.Quiver.reflectArrowSource: an arrow into, respectively out of, i, read in the opposite direction in the reflected quiver.
• TauCeti.Quiver.reflectArrowOfNeOfNe: an arrow of V between two vertices other than i, read as an arrow of the reflected quiver.

Main results

• TauCeti.Quiver.IsSink.isSource_reflect: reflecting at a sink turns it into a source.
• TauCeti.Quiver.IsSink.path_self_eq_nil: a closed path at a sink is the trivial one, with TauCeti.Quiver.IsSource.path_self_eq_nil its dual.
• TauCeti.Quiver.hom_reflect_reflect: reflecting twice at the same vertex restores the original arrows, so reflection at a vertex is an involution.

References

This file supplies the reflected quiver Q.reflect i that the reflection functors of Layer 4 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md map into. See Derksen--Weyman, An Introduction to Quiver Representations, and Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem.

Sinks and sources

def TauCeti.Quiver.IsSink {V : Type u} [Quiver V] (i : V) : Prop

A vertex of a quiver is a sink if no arrow leaves it.

Equations

• TauCeti.Quiver.IsSink i = ∀ (b : V), IsEmpty (i ⟶ b)

def TauCeti.Quiver.IsSource {V : Type u} [Quiver V] (i : V) : Prop

A vertex of a quiver is a source if no arrow enters it.

Equations

• TauCeti.Quiver.IsSource i = ∀ (a : V), IsEmpty (a ⟶ i)

theorem TauCeti.Quiver.IsSink_def {V : Type u} [Quiver V] (i : V) : IsSink i ↔ ∀ (b : V), IsEmpty (i ⟶ b)

The defining condition for a sink.

theorem TauCeti.Quiver.IsSource_def {V : Type u} [Quiver V] (i : V) : IsSource i ↔ ∀ (a : V), IsEmpty (a ⟶ i)

The defining condition for a source.

theorem TauCeti.Quiver.IsSink.isEmpty_hom {V : Type u} [Quiver V] {i : V} (h : IsSink i) (b : V) : IsEmpty (i ⟶ b)

No arrow leaves a sink.

theorem TauCeti.Quiver.IsSource.isEmpty_hom {V : Type u} [Quiver V] {i : V} (h : IsSource i) (a : V) : IsEmpty (a ⟶ i)

No arrow enters a source.

theorem TauCeti.Quiver.IsSink.isEmpty_hom_self {V : Type u} [Quiver V] {i : V} (h : IsSink i) : IsEmpty (i ⟶ i)

A sink carries no loop.

theorem TauCeti.Quiver.IsSource.isEmpty_hom_self {V : Type u} [Quiver V] {i : V} (h : IsSource i) : IsEmpty (i ⟶ i)

A source carries no loop.

theorem TauCeti.Quiver.IsSink.ne_of_hom {V : Type u} [Quiver V] {i b : V} (h : IsSink i) (e : b ⟶ i) : b ≠ i

An arrow into a sink starts somewhere else, since a sink carries no loop.

theorem TauCeti.Quiver.IsSource.ne_of_hom {V : Type u} [Quiver V] {i b : V} (h : IsSource i) (e : i ⟶ b) : b ≠ i

An arrow out of a source ends somewhere else, since a source carries no loop.

theorem TauCeti.Quiver.IsSink.eq_of_path {V : Type u} [Quiver V] {i b : V} (h : IsSink i) (p : Quiver.Path i b) : i = b

A path out of a sink is trivial, so it ends where it started.

theorem TauCeti.Quiver.IsSource.eq_of_path {V : Type u} [Quiver V] {i a : V} (h : IsSource i) (p : Quiver.Path a i) : a = i

A path into a source is trivial, so it starts where it ends.

theorem TauCeti.Quiver.IsSink.path_self_eq_nil {V : Type u} [Quiver V] {i : V} (h : IsSink i) (p : Quiver.Path i i) : p = Quiver.Path.nil

A closed path at a sink is the trivial one: its last arrow would have to be a loop at the sink. This is the form TauCeti.Quiver.IsSink.eq_of_path takes once its conclusion has been substituted, and it is what says that a sink acts on a representation only through the identity.

theorem TauCeti.Quiver.IsSource.path_self_eq_nil {V : Type u} [Quiver V] {i : V} (h : IsSource i) (p : Quiver.Path i i) : p = Quiver.Path.nil

A closed path at a source is the trivial one.

The arrows of the reflected quiver

noncomputable def TauCeti.Quiver.reflectHom {V : Type u} [Quiver V] (i a b : V) : Type v

The arrows from a to b in the quiver obtained from V by reversing every arrow incident to the vertex i. Arrows between two vertices other than i are untouched, an arrow b ⟶ i becomes an arrow i ⟶ b, and the loops at i are reversed among themselves.

Equations

• TauCeti.Quiver.reflectHom i a b = if a = i then if b = i then i ⟶ i else b ⟶ i else if b = i then i ⟶ a else a ⟶ b

@[simp]

theorem TauCeti.Quiver.reflectHom_left {V : Type u} [Quiver V] (i b : V) : reflectHom i i b = (b ⟶ i)

The arrows out of i in the reflected quiver are the arrows into i in the original one.

@[simp]

theorem TauCeti.Quiver.reflectHom_right {V : Type u} [Quiver V] (i a : V) : reflectHom i a i = (i ⟶ a)

The arrows into i in the reflected quiver are the arrows out of i in the original one.

@[simp]

theorem TauCeti.Quiver.reflectHom_of_ne_of_ne {V : Type u} [Quiver V] {i a b : V} (ha : a ≠ i) (hb : b ≠ i) : reflectHom i a b = (a ⟶ b)

Away from i the reflected quiver has the arrows of the original one.

@[instance_reducible]

noncomputable instance TauCeti.Quiver.instFintypeReflectHom {V : Type u} [Quiver V] [(a b : V) → Fintype (a ⟶ b)] (i a b : V) : Fintype (reflectHom i a b)

Equations

• TauCeti.Quiver.instFintypeReflectHom i a b = if ha : a = i then ⋯ ▸ ⋯.mpr inferInstance else if hb : b = i then ⋯ ▸ ⋯.mpr inferInstance else ⋯.mpr inferInstance

The reflected quiver

def TauCeti.Quiver.Reflect (V : Type u) (_i : V) : Type u

The reflection of a quiver at a vertex i: a type synonym for the vertex type, carrying the quiver in which every arrow incident to i is reversed.

Equations

• TauCeti.Quiver.Reflect V _i = V

@[instance_reducible]

noncomputable instance TauCeti.Quiver.reflectQuiver {V : Type u} [Quiver V] (i : V) : Quiver (Reflect V i)

Equations

• TauCeti.Quiver.reflectQuiver i = { Hom := fun (a b : V) => TauCeti.Quiver.reflectHom i a b }

@[instance_reducible]

instance TauCeti.Quiver.instDecidableEqReflect {V : Type u} (i : V) [DecidableEq V] : DecidableEq (Reflect V i)

Equations

• TauCeti.Quiver.instDecidableEqReflect i = TauCeti.Quiver.instDecidableEqReflect._aux_1 i

@[instance_reducible]

instance TauCeti.Quiver.instFintypeReflect {V : Type u} (i : V) [Fintype V] : Fintype (Reflect V i)

Equations

• TauCeti.Quiver.instFintypeReflect i = TauCeti.Quiver.instFintypeReflect._aux_1 i

instance TauCeti.Quiver.instNonemptyReflect {V : Type u} (i : V) [Nonempty V] : Nonempty (Reflect V i)

@[instance_reducible]

noncomputable instance TauCeti.Quiver.instFintypeHomReflect {V : Type u} [Quiver V] (i : V) [(a b : V) → Fintype (a ⟶ b)] (a b : Reflect V i) : Fintype (a ⟶ b)

Equations

• TauCeti.Quiver.instFintypeHomReflect i a b = TauCeti.Quiver.instFintypeReflectHom i a b

@[simp]

theorem TauCeti.Quiver.hom_reflect {V : Type u} [Quiver V] (i : V) (a b : Reflect V i) : (a ⟶ b) = reflectHom i a b

The arrow types of the reflected quiver are the ones computed by TauCeti.Quiver.reflectHom.

The arrows of the reflected quiver, named

An arrow of the reflected quiver is a cast of an arrow of V, because TauCeti.Quiver.reflectHom is an if on equality with i. The two casts that the reflection of a representation at a sink uses are named here, together with their computation rules and the matching elimination rules, which read an arbitrary arrow of the reflected quiver as one of the two.

def TauCeti.Quiver.reflectArrow {V : Type u} [Quiver V] (i : V) {b : V} (e : b ⟶ i) : i ⟶ b

An arrow b ⟶ i of V, read as the reversed arrow i ⟶ b of the reflected quiver.

Equations

• TauCeti.Quiver.reflectArrow i e = cast ⋯ e

def TauCeti.Quiver.reflectArrowSource {V : Type u} [Quiver V] (i : V) {b : V} (e : i ⟶ b) : b ⟶ i

An arrow i ⟶ b of V, read as the reversed arrow b ⟶ i of the reflected quiver. This is the source-side counterpart of TauCeti.Quiver.reflectArrow.

Equations

• TauCeti.Quiver.reflectArrowSource i e = cast ⋯ e

def TauCeti.Quiver.reflectArrowOfNeOfNe {V : Type u} [Quiver V] {i a b : V} (ha : a ≠ i) (hb : b ≠ i) (e : a ⟶ b) : a ⟶ b

An arrow a ⟶ b of V between two vertices other than i, read as an arrow of the reflected quiver, where it is untouched.

Equations

• TauCeti.Quiver.reflectArrowOfNeOfNe ha hb e = cast ⋯ e

@[simp]

theorem TauCeti.Quiver.cast_reflectArrow {V : Type u} [Quiver V] (i : V) {b : V} (e : b ⟶ i) (h : (i ⟶ b) = (b ⟶ i)) : cast h (reflectArrow i e) = e

Casting a reversed arrow back to V recovers the arrow it came from. Stated for an arbitrary proof of the type equality, since the definition of a reflected representation produces its own.

@[simp]

theorem TauCeti.Quiver.cast_reflectArrowSource {V : Type u} [Quiver V] (i : V) {b : V} (e : i ⟶ b) (h : (b ⟶ i) = (i ⟶ b)) : cast h (reflectArrowSource i e) = e

Casting a source-side reversed arrow back to V recovers the arrow it came from.

@[simp]

theorem TauCeti.Quiver.cast_reflectArrowOfNeOfNe {V : Type u} [Quiver V] {i a b : V} (ha : a ≠ i) (hb : b ≠ i) (e : a ⟶ b) (h : (a ⟶ b) = (a ⟶ b)) : cast h (reflectArrowOfNeOfNe ha hb e) = e

Casting an arrow away from i back to V recovers the arrow it came from.

@[simp]

theorem TauCeti.Quiver.reflectArrow_cast {V : Type u} [Quiver V] (i : V) {b : V} (e : i ⟶ b) (h : (i ⟶ b) = (b ⟶ i)) : reflectArrow i (cast h e) = e

Every arrow out of i in the reflected quiver is a reversed arrow. Reading such an arrow back as an arrow of V and reflecting it again recovers it, so a case analysis on the endpoints lets TauCeti.Quiver.reflectArrow eliminate an arbitrary arrow i ⟶ b of the reflected quiver. Stated for an arbitrary proof of the type equality, like TauCeti.Quiver.cast_reflectArrow.

@[simp]

theorem TauCeti.Quiver.reflectArrowSource_cast {V : Type u} [Quiver V] (i : V) {b : V} (e : b ⟶ i) (h : (b ⟶ i) = (i ⟶ b)) : reflectArrowSource i (cast h e) = e

Every arrow into i in the reflected quiver is a source-side reversed arrow.

@[simp]

theorem TauCeti.Quiver.reflectArrowOfNeOfNe_cast {V : Type u} [Quiver V] {i a b : V} (ha : a ≠ i) (hb : b ≠ i) (e : a ⟶ b) (h : (a ⟶ b) = (a ⟶ b)) : reflectArrowOfNeOfNe ha hb (cast h e) = e

Every arrow of the reflected quiver away from i is an untouched arrow. Reading such an arrow back as an arrow of V and reflecting it again recovers it, so TauCeti.Quiver.reflectArrowOfNeOfNe eliminates an arbitrary arrow a ⟶ b of the reflected quiver with a ≠ i and b ≠ i.

theorem TauCeti.Quiver.IsSink.isSource_reflect {V : Type u} [Quiver V] {i : V} (h : IsSink i) : IsSource i

Reflecting at a sink turns it into a source: no arrow of the reflected quiver enters i.

theorem TauCeti.Quiver.IsSource.isSink_reflect {V : Type u} [Quiver V] {i : V} (h : IsSource i) : IsSink i

Reflecting at a source turns it into a sink: no arrow of the reflected quiver leaves i.

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

Reflecting twice at the same vertex restores the original arrow types: reflection at a vertex is an involution on quivers.

Arrow counts in the reflected quiver

theorem TauCeti.Quiver.card_reflectHom_left {V : Type u} [Quiver V] [(a b : V) → Fintype (a ⟶ b)] (i b : V) : Fintype.card (reflectHom i i b) = Fintype.card (b ⟶ i)

The reflected quiver has as many arrows i ⟶ b as the original has arrows b ⟶ i.

theorem TauCeti.Quiver.card_reflectHom_right {V : Type u} [Quiver V] [(a b : V) → Fintype (a ⟶ b)] (i a : V) : Fintype.card (reflectHom i a i) = Fintype.card (i ⟶ a)

The reflected quiver has as many arrows a ⟶ i as the original has arrows i ⟶ a.

theorem TauCeti.Quiver.card_reflectHom_of_ne_of_ne {V : Type u} [Quiver V] [(a b : V) → Fintype (a ⟶ b)] {i a b : V} (ha : a ≠ i) (hb : b ≠ i) : Fintype.card (reflectHom i a b) = Fintype.card (a ⟶ b)

Away from i the reflected quiver has the same arrow counts as the original.

theorem TauCeti.Quiver.card_reflectHom_add_swap {V : Type u} [Quiver V] [(a b : V) → Fintype (a ⟶ b)] (i a b : V) : Fintype.card (reflectHom i a b) + Fintype.card (reflectHom i b a) = Fintype.card (a ⟶ b) + Fintype.card (b ⟶ a)

Reflection at a vertex preserves the number of arrows joining any two vertices in either direction: it changes the orientation of the quiver, not its underlying graph.

theorem TauCeti.Quiver.card_reflectHom_right_of_isSink {V : Type u} [Quiver V] [(a b : V) → Fintype (a ⟶ b)] {i : V} (h : IsSink i) (a : V) : Fintype.card (reflectHom i a i) = 0

Reflecting at a sink leaves no arrow into i.