The underlying graph of a quiver

The underlying graph of a quiver joins two distinct vertices when an arrow runs between them in either direction (TauCeti.Quiver.underlyingGraph). It forgets loops, the direction of the arrows and their multiplicity, so it records what orientation-free statements about a quiver, such as Gabriel's theorem, are phrased in terms of; it depends only on the arrows joining each pair of distinct vertices, whatever their direction (TauCeti.Quiver.underlyingGraph_congr).

Main definitions

• TauCeti.Quiver.underlyingGraph: the simple graph underlying a quiver.

Main results

• TauCeti.Quiver.underlyingGraph_adj: two vertices are adjacent when they are distinct and joined by an arrow in one direction or the other.
• TauCeti.Quiver.underlyingGraph_congr: two quiver structures joining the same pairs of distinct vertices by an arrow, in either direction, have the same underlying graph.
• TauCeti.Quiver.isAcyclic_underlyingGraph_of_lt: a quiver in which the arrows out of each vertex all share their target, and every arrow strictly lowers a height function, has a forest as its underlying graph.
• TauCeti.Quiver.subsingleton_hom_sum_of_lt: for fixed vertices a and b, if each directional arrow type is subsingleton and arrows between them lower an asymmetric height relation, then at most one arrow joins a and b, counted in both directions.

def TauCeti.Quiver.underlyingGraph (V : Type u) [Quiver V] : SimpleGraph V

The simple graph underlying a quiver: two distinct vertices are adjacent when an arrow runs between them in either direction. Loops, the direction of the arrows and their multiplicity are forgotten.

Equations

• TauCeti.Quiver.underlyingGraph V = SimpleGraph.fromRel fun (a b : V) => Nonempty (a ⟶ b)

@[simp]

theorem TauCeti.Quiver.underlyingGraph_adj {V : Type u} [Quiver V] {a b : V} : (underlyingGraph V).Adj a b ↔ a ≠ b ∧ (Nonempty (a ⟶ b) ∨ Nonempty (b ⟶ a))

Two vertices are adjacent in the underlying graph when they are distinct and joined by an arrow in one direction or the other.

theorem TauCeti.Quiver.underlyingGraph_adj_of_hom {V : Type u} [Quiver V] {a b : V} (e : a ⟶ b) (hab : a ≠ b) : (underlyingGraph V).Adj a b

The two ends of an arrow which is not a loop are adjacent in the underlying graph.

theorem TauCeti.Quiver.isAcyclic_underlyingGraph_of_lt {V : Type u} [Quiver V] {α : Type u_1} [LT α] [IsStrictOrder α fun (x1 x2 : α) => x1 < x2] (ht : V → α) (hlt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), ht b < ht a) (hout : ∀ ⦃a b b' : V⦄ (a_1 : a ⟶ b) (a : a ⟶ b'), b = b') : (underlyingGraph V).IsAcyclic

The underlying graph of an in-forest is acyclic. If the arrows out of each vertex of a quiver all share their target, and every arrow strictly lowers a height function ht into a strictly ordered type, then the underlying graph of the quiver has no cycle.

theorem TauCeti.Quiver.subsingleton_hom_sum_of_lt {V : Type u} [Quiver V] {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] (ht : V → α) (a b : V) (hlt : ∀ (a_1 : a ⟶ b), ht b < ht a) (hlt' : ∀ (a_1 : b ⟶ a), ht a < ht b) [Subsingleton (a ⟶ b)] [Subsingleton (b ⟶ a)] : Subsingleton ((a ⟶ b) ⊕ (b ⟶ a))

For fixed vertices a and b, if each of a ⟶ b and b ⟶ a is subsingleton and arrows between them lower a height function into a type with an asymmetric relation, then (a ⟶ b) ⊕ (b ⟶ a) is subsingleton.

theorem TauCeti.Quiver.underlyingGraph_congr {V : Type u} {q : Quiver V} {q' : Quiver V} (h : ∀ (a b : V), a ≠ b → (Nonempty ((a ⟶ b) ⊕ (b ⟶ a)) ↔ Nonempty ((a ⟶ b) ⊕ (b ⟶ a)))) : underlyingGraph V = underlyingGraph V

The underlying graph depends only on which vertices are joined: two quiver structures which join the same pairs of distinct vertices by an arrow, in one direction or the other, have the same underlying graph. The arrow types may live in different universes, and loops need not agree.