Orienting a simple graph and recovering its doubled quiver

An orientation of a simple graph chooses exactly one dart over every edge. The chosen darts form a quiver with one arrow over each edge, and symmetrifying that quiver recovers the doubled quiver of the graph. This file constructs mutually inverse, reversal-preserving prefunctors which implement that identification.

The definition keeps the choice of orientation separate from the doubled quiver. In particular, the comparison does not impose an ordering on the graph's vertices: a linear order merely supplies one convenient witness that every graph admits an orientation.

Main definitions

• TauCeti.DoubledQuiver.Orientation: a choice of one dart from each reversed pair.
• TauCeti.DoubledQuiver.Orientation.ofLinearOrder: orient every edge from its smaller endpoint to its larger endpoint.
• SimpleGraph.Coloring.sourceSink: direct every edge toward the true endpoint of a two-colouring.
• TauCeti.DoubledQuiver.OrientedQuiver: the quiver of the chosen darts.
• TauCeti.DoubledQuiver.OrientedQuiver.homEquiv: its arrows over a pair of graph vertices are exactly the adjacency proofs whose dart the orientation selects.
• TauCeti.DoubledQuiver.OrientedQuiver.card_hom_ofLinearOrder, TauCeti.DoubledQuiver.OrientedQuiver.lt_of_path_of_length_pos_ofLinearOrder, TauCeti.DoubledQuiver.OrientedQuiver.le_of_path_ofLinearOrder, and TauCeti.DoubledQuiver.OrientedQuiver.isAcyclic_ofLinearOrder: arrow counts, path monotonicity, and acyclicity for the linear-order orientation.
• TauCeti.DoubledQuiver.OrientedQuiver.card_symmetrify_hom: symmetrifying an orientation recovers the adjacency counts of the graph.
• TauCeti.DoubledQuiver.OrientedQuiver.sum_card_hom_add_card_hom_mul: a vertex weight summed against the arrow counts of an orientation in both directions is its neighbour sum, via which a positive superadditive weight on the oriented quiver excludes isolated vertices (TauCeti.DoubledQuiver.OrientedQuiver.exists_adj_of_pos_two_mul_le_sum).
• TauCeti.DoubledQuiver.symmetrifyMap: the canonical prefunctor from the symmetrification of an oriented graph to its doubled quiver.
• TauCeti.DoubledQuiver.unsymmetrifyMap: its inverse prefunctor.
• TauCeti.exists_forall_exists_nonempty_reorient_hom: a neighbour choice without mutual choices gives a reorientation of any orientation with no sinks.

References

The comparison uses Mathlib's universal property Quiver.Symmetrify.lift.

structure TauCeti.DoubledQuiver.Orientation {V : Type u} (G : SimpleGraph V) : Type u

An orientation of a simple graph is a set of darts containing exactly one dart over each edge. The displayed condition says that a reversed dart is chosen exactly when the original dart is not chosen.

• carrier : Set G.Dart

  The set of darts belonging to the orientation.

• symm_mem_iff_not_mem (d : G.Dart) : d.symm ∈ self.carrier ↔ d ∉ self.carrier

@[instance_reducible]

instance TauCeti.DoubledQuiver.Orientation.instSetLikeDart {V : Type u} (G : SimpleGraph V) : SetLike (Orientation G) G.Dart

theorem TauCeti.DoubledQuiver.Orientation.ext {V : Type u} (G : SimpleGraph V) {o₁ o₂ : Orientation G} (h : ∀ (d : G.Dart), d ∈ o₁ ↔ d ∈ o₂) : o₁ = o₂

theorem TauCeti.DoubledQuiver.Orientation.ext_iff {V : Type u} {G : SimpleGraph V} {o₁ o₂ : Orientation G} : o₁ = o₂ ↔ ∀ (d : G.Dart), d ∈ o₁ ↔ d ∈ o₂

@[simp]

theorem TauCeti.DoubledQuiver.Orientation.symm_notMem_iff_mem {V : Type u} (G : SimpleGraph V) (o : Orientation G) (d : G.Dart) : d.symm ∉ o ↔ d ∈ o

A reversed dart is not chosen exactly when the original dart is chosen.

def TauCeti.DoubledQuiver.Orientation.ofLinearOrder {V : Type u} (G : SimpleGraph V) [LinearOrder V] : Orientation G

The orientation induced by a linear order, with each edge directed from its smaller endpoint to its larger endpoint.

@[simp]

theorem TauCeti.DoubledQuiver.Orientation.mem_ofLinearOrder_iff {V : Type u} (G : SimpleGraph V) [LinearOrder V] (d : G.Dart) : d ∈ ofLinearOrder G ↔ d.toProd.1 < d.toProd.2

A dart belongs to the linear-order orientation exactly when its source is smaller than its target.

def TauCeti.DoubledQuiver.OrientedQuiver {V : Type u} (G : SimpleGraph V) (_o : Orientation G) : Type u

The quiver obtained by retaining only the darts selected by an orientation.

def TauCeti.DoubledQuiver.OrientedQuiver.vertex {V : Type u} (G : SimpleGraph V) (o : Orientation G) (v : V) : OrientedQuiver G o

Include a graph vertex into the oriented quiver.

def TauCeti.DoubledQuiver.OrientedQuiver.vertexEquiv {V : Type u} (G : SimpleGraph V) (o : Orientation G) : V ≃ OrientedQuiver G o

The graph vertices and the vertices of an oriented quiver are canonically equivalent.

@[simp]

theorem TauCeti.DoubledQuiver.OrientedQuiver.vertexEquiv_apply {V : Type u} (G : SimpleGraph V) (o : Orientation G) (v : V) : (vertexEquiv G o) v = vertex G o v

@[simp]

theorem TauCeti.DoubledQuiver.OrientedQuiver.vertexEquiv_symm_vertex {V : Type u} (G : SimpleGraph V) (o : Orientation G) (v : V) : (vertexEquiv G o).symm (vertex G o v) = v

@[instance_reducible]

instance TauCeti.DoubledQuiver.OrientedQuiver.instQuiver {V : Type u} (G : SimpleGraph V) (o : Orientation G) : Quiver (OrientedQuiver G o)

instance TauCeti.DoubledQuiver.OrientedQuiver.instIsThin {V : Type u} (G : SimpleGraph V) (o : Orientation G) : Quiver.IsThin (OrientedQuiver G o)

instance TauCeti.DoubledQuiver.OrientedQuiver.instFinite {V : Type u} (G : SimpleGraph V) (o : Orientation G) [Finite V] : Finite (OrientedQuiver G o)

@[instance_reducible]

noncomputable instance TauCeti.DoubledQuiver.OrientedQuiver.instFintypeOfFinite {V : Type u} (G : SimpleGraph V) (o : Orientation G) [Finite V] : Fintype (OrientedQuiver G o)

The oriented quiver has finitely many vertices when the graph does.

instance TauCeti.DoubledQuiver.OrientedQuiver.instFiniteHom {V : Type u} (G : SimpleGraph V) (o : Orientation G) (i j : OrientedQuiver G o) : Finite (i ⟶ j)

@[instance_reducible]

noncomputable instance TauCeti.DoubledQuiver.OrientedQuiver.instFintypeHom {V : Type u} (G : SimpleGraph V) (o : Orientation G) (i j : OrientedQuiver G o) : Fintype (i ⟶ j)

The arrows of an oriented simple graph form a finite type between any two vertices.

def TauCeti.DoubledQuiver.OrientedQuiver.arrow {V : Type u} (G : SimpleGraph V) (o : Orientation G) {i j : V} (h : G.Adj i j) (ho : { fst := i, snd := j, adj := h } ∈ o) : vertex G o i ⟶ vertex G o j

The oriented-quiver arrow corresponding to a chosen dart.

def TauCeti.DoubledQuiver.OrientedQuiver.homEquiv {V : Type u} (G : SimpleGraph V) (o : Orientation G) (i j : V) : (vertex G o i ⟶ vertex G o j) ≃ { h : G.Adj i j // { fst := i, snd := j, adj := h } ∈ o }

The arrows of the oriented quiver between two graph vertices are exactly the adjacency proofs whose dart is selected by the orientation. This is the characteristic description of the quiver structure, so consumers never need to unfold the Quiver instance.

@[simp]

theorem TauCeti.DoubledQuiver.OrientedQuiver.homEquiv_arrow {V : Type u} (G : SimpleGraph V) (o : Orientation G) {i j : V} (h : G.Adj i j) (ho : { fst := i, snd := j, adj := h } ∈ o) : (homEquiv G o i j) (arrow G o h ho) = ⟨h, ho⟩

The characteristic description of the oriented-quiver arrows reads off the adjacency proof underlying the arrow of a selected dart.

@[simp]

theorem TauCeti.DoubledQuiver.OrientedQuiver.homEquiv_symm_apply {V : Type u} (G : SimpleGraph V) (o : Orientation G) {i j : V} (h : G.Adj i j) (ho : { fst := i, snd := j, adj := h } ∈ o) : (homEquiv G o i j).symm ⟨h, ho⟩ = arrow G o h ho

The characteristic description of the oriented-quiver arrows sends a selected dart back to its arrow.

theorem TauCeti.DoubledQuiver.OrientedQuiver.exists_eq_arrow {V : Type u} (G : SimpleGraph V) (o : Orientation G) {i j : V} (e : vertex G o i ⟶ vertex G o j) : ∃ (h : G.Adj i j) (ho : { fst := i, snd := j, adj := h } ∈ o), e = arrow G o h ho

Every arrow of the oriented quiver comes from a dart selected by the orientation.

theorem TauCeti.DoubledQuiver.OrientedQuiver.card_hom_ofLinearOrder {V : Type u} (G : SimpleGraph V) [LinearOrder V] (i j : V) [Decidable (i < j ∧ G.Adj i j)] : Nat.card (vertex G (Orientation.ofLinearOrder G) i ⟶ vertex G (Orientation.ofLinearOrder G) j) = if i < j ∧ G.Adj i j then 1 else 0

For the linear-order orientation, there is one arrow from i to j exactly when i < j and the vertices are adjacent.

theorem TauCeti.DoubledQuiver.OrientedQuiver.lt_of_path_of_length_pos_ofLinearOrder {V : Type u} (G : SimpleGraph V) [LinearOrder V] {a b : OrientedQuiver G (Orientation.ofLinearOrder G)} (p : Quiver.Path a b) (hp : 0 < p.length) : (vertexEquiv G (Orientation.ofLinearOrder G)).symm a < (vertexEquiv G (Orientation.ofLinearOrder G)).symm b

Along any positive-length path in the linear-order orientation, the start vertex is strictly smaller than the end vertex.

theorem TauCeti.DoubledQuiver.OrientedQuiver.le_of_path_ofLinearOrder {V : Type u} (G : SimpleGraph V) [LinearOrder V] {a b : OrientedQuiver G (Orientation.ofLinearOrder G)} (p : Quiver.Path a b) : (vertexEquiv G (Orientation.ofLinearOrder G)).symm a ≤ (vertexEquiv G (Orientation.ofLinearOrder G)).symm b

Along any path in the linear-order orientation, the start vertex is at most the end vertex.

theorem TauCeti.DoubledQuiver.OrientedQuiver.isAcyclic_ofLinearOrder {V : Type u} (G : SimpleGraph V) [LinearOrder V] : Quiver.IsAcyclic (OrientedQuiver G (Orientation.ofLinearOrder G))

Orienting every edge of a graph from the smaller vertex to the larger makes an acyclic quiver.

theorem TauCeti.DoubledQuiver.OrientedQuiver.card_hom_add_card_hom {V : Type u} (G : SimpleGraph V) (o : Orientation G) [DecidableRel G.Adj] (i j : V) : Nat.card (vertex G o i ⟶ vertex G o j) + Nat.card (vertex G o j ⟶ vertex G o i) = if G.Adj i j then 1 else 0

An orientation has one arrow, in total across the two directions, over each edge.

theorem TauCeti.DoubledQuiver.OrientedQuiver.card_symmetrify_hom {V : Type u} (G : SimpleGraph V) (o : Orientation G) [DecidableRel G.Adj] (i j : V) : Fintype.card (Quiver.Symmetrify.of.obj (vertex G o i) ⟶ Quiver.Symmetrify.of.obj (vertex G o j)) = if G.Adj i j then 1 else 0

The symmetrification of an oriented graph has one arrow between two vertices exactly when they are adjacent: the chosen arrow over the edge or its formal reverse.

theorem TauCeti.DoubledQuiver.OrientedQuiver.sum_card_hom_add_card_hom_mul {V : Type u} (G : SimpleGraph V) (o : Orientation G) [Fintype V] [DecidableRel G.Adj] {S : Type u_1} [NonAssocSemiring S] (δ : V → S) (i : V) : ∑ j : OrientedQuiver G o, ↑(Fintype.card (vertex G o i ⟶ j) + Fintype.card (j ⟶ vertex G o i)) * δ ((vertexEquiv G o).symm j) = ∑ j ∈ G.neighborFinset i, δ j

A weight on a graph read on an orientation: for every vertex i, the multigraph sum ∑_j (#(i ⟶ j) + #(j ⟶ i)) δ_j over the vertices of the oriented quiver is the neighbour sum ∑_{j ∼ i} δ_j, since an orientation has exactly one arrow over each edge.

theorem TauCeti.DoubledQuiver.OrientedQuiver.exists_adj_of_pos_two_mul_le_sum {V : Type u} (G : SimpleGraph V) (o : Orientation G) [Finite V] {S : Type u_1} [Semiring S] [PartialOrder S] [IsOrderedRing S] (δ : OrientedQuiver G o → S) (hδ : ∀ (i : OrientedQuiver G o), 0 < δ i) (hδle : ∀ (i : OrientedQuiver G o), 2 * δ i ≤ ∑ j : OrientedQuiver G o, ↑(Fintype.card (i ⟶ j) + Fintype.card (j ⟶ i)) * δ j) (i : V) : ∃ (j : V), G.Adj i j

A positive superadditive weight on an oriented graph excludes isolated vertices. Let δ be a weight on the vertices of an orientation of a finite simple graph over an ordered semiring, positive at every vertex, with 2 δ_i ≤ ∑_j (#(i ⟶ j) + #(j ⟶ i)) δ_j at every vertex of the oriented quiver. Then every vertex of the graph has a neighbour.

def TauCeti.DoubledQuiver.OrientedQuiver.forget {V : Type u} (G : SimpleGraph V) (o : Orientation G) : OrientedQuiver G o ⥤q DoubledQuiver G

Forgetting the choice of orientation includes the oriented quiver into the doubled quiver.

@[simp]

theorem TauCeti.DoubledQuiver.OrientedQuiver.forget_obj {V : Type u} (G : SimpleGraph V) (o : Orientation G) (i : V) : (forget G o).obj (vertex G o i) = DoubledQuiver.vertex G i

@[simp]

theorem TauCeti.DoubledQuiver.OrientedQuiver.forget_arrow {V : Type u} (G : SimpleGraph V) (o : Orientation G) {i j : V} (h : G.Adj i j) (ho : { fst := i, snd := j, adj := h } ∈ o) : (forget G o).map (arrow G o h ho) = Quiver.homOfEq (DoubledQuiver.arrow G h) ⋯ ⋯

def TauCeti.DoubledQuiver.symmetrifyMap {V : Type u} (G : SimpleGraph V) (o : Orientation G) : Quiver.Symmetrify (OrientedQuiver G o) ⥤q DoubledQuiver G

Symmetrifying an oriented graph and forgetting the orientation maps to the doubled quiver.

@[simp]

theorem TauCeti.DoubledQuiver.symmetrifyMap_obj {V : Type u} (G : SimpleGraph V) (o : Orientation G) (i : V) : (symmetrifyMap G o).obj (OrientedQuiver.vertex G o i) = vertex G i

@[simp]

theorem TauCeti.DoubledQuiver.symmetrifyMap_toPos {V : Type u} (G : SimpleGraph V) (o : Orientation G) {i j : V} (h : G.Adj i j) (ho : { fst := i, snd := j, adj := h } ∈ o) : (symmetrifyMap G o).map (Sum.inl (OrientedQuiver.arrow G o h ho)) = Quiver.homOfEq (arrow G h) ⋯ ⋯

The comparison sends the positive copy of an oriented arrow to the doubled-quiver arrow of the selected dart.

@[simp]

theorem TauCeti.DoubledQuiver.symmetrifyMap_toNeg {V : Type u} (G : SimpleGraph V) (o : Orientation G) {i j : V} (h : G.Adj i j) (ho : { fst := i, snd := j, adj := h } ∈ o) : (symmetrifyMap G o).map (Sum.inr (OrientedQuiver.arrow G o h ho)) = Quiver.homOfEq (arrow G ⋯) ⋯ ⋯

The comparison sends the negative copy of an oriented arrow to the doubled-quiver arrow of the reversed dart.

instance TauCeti.DoubledQuiver.symmetrifyMapMapReverse {V : Type u} (G : SimpleGraph V) (o : Orientation G) : (symmetrifyMap G o).MapReverse

The comparison from a symmetrified orientation to the doubled quiver preserves reversal.

noncomputable def TauCeti.DoubledQuiver.unsymmetrifyMap {V : Type u} (G : SimpleGraph V) (o : Orientation G) : DoubledQuiver G ⥤q Quiver.Symmetrify (OrientedQuiver G o)

The inverse comparison sends a doubled arrow to the positive copy when its dart was chosen, and to the negative copy of the oppositely oriented arrow otherwise.

@[simp]

theorem TauCeti.DoubledQuiver.unsymmetrifyMap_obj {V : Type u} (G : SimpleGraph V) (o : Orientation G) (i : V) : (unsymmetrifyMap G o).obj (vertex G i) = OrientedQuiver.vertex G o i

instance TauCeti.DoubledQuiver.instIsThinSymmetrifyOrientedQuiver {V : Type u} (G : SimpleGraph V) (o : Orientation G) : Quiver.IsThin (Quiver.Symmetrify (OrientedQuiver G o))

The symmetrification of an oriented simple graph is thin, as it has exactly one arrow in each direction over every graph edge.

@[simp]

theorem TauCeti.DoubledQuiver.unsymmetrifyMap_arrow_of_mem {V : Type u} (G : SimpleGraph V) (o : Orientation G) {i j : V} (h : G.Adj i j) (ho : { fst := i, snd := j, adj := h } ∈ o) : (unsymmetrifyMap G o).map (arrow G h) = Quiver.homOfEq (Sum.inl (OrientedQuiver.arrow G o h ho)) ⋯ ⋯

On a chosen dart, the inverse comparison returns the positive copy of the corresponding oriented-quiver arrow.

@[simp]

theorem TauCeti.DoubledQuiver.unsymmetrifyMap_arrow_of_not_mem {V : Type u} (G : SimpleGraph V) (o : Orientation G) {i j : V} (h : G.Adj i j) (ho : { fst := i, snd := j, adj := h } ∉ o) : (unsymmetrifyMap G o).map (arrow G h) = Quiver.homOfEq (Sum.inr (OrientedQuiver.arrow G o ⋯ ⋯)) ⋯ ⋯

On a dart not selected by the orientation, the inverse comparison returns the negative copy of the oppositely oriented arrow.

@[simp]

theorem TauCeti.DoubledQuiver.unsymmetrifyMap_comp_symmetrifyMap {V : Type u} (G : SimpleGraph V) (o : Orientation G) : unsymmetrifyMap G o ⋙q symmetrifyMap G o = 𝟭q (DoubledQuiver G)

Forgetting after restoring an orientation is the identity doubled-quiver prefunctor.

@[simp]

theorem TauCeti.DoubledQuiver.symmetrifyMap_comp_unsymmetrifyMap {V : Type u} (G : SimpleGraph V) (o : Orientation G) : symmetrifyMap G o ⋙q unsymmetrifyMap G o = 𝟭q (Quiver.Symmetrify (OrientedQuiver G o))

Restoring the orientation after forgetting it is the identity on the symmetrified oriented quiver.

instance TauCeti.DoubledQuiver.unsymmetrifyMapMapReverse {V : Type u} (G : SimpleGraph V) (o : Orientation G) : (unsymmetrifyMap G o).MapReverse

The inverse comparison also preserves arrow reversal.

theorem TauCeti.DoubledQuiver.unsymmetrifyMap_isCovering {V : Type u} (G : SimpleGraph V) (o : Orientation G) : (unsymmetrifyMap G o).IsCovering

The comparison from a doubled graph to a symmetrified orientation is a quiver covering. In fact it is an isomorphism of quivers, but the covering interface is the part needed to transport sums over the arrows incident to a vertex.

theorem TauCeti.DoubledQuiver.symmetrifyMap_isCovering {V : Type u} (G : SimpleGraph V) (o : Orientation G) : (symmetrifyMap G o).IsCovering

The inverse comparison from a symmetrified orientation to the doubled graph is also a quiver covering.

theorem TauCeti.exists_forall_exists_nonempty_reorient_hom {V : Type u} {G : SimpleGraph V} (o : DoubledQuiver.Orientation G) {f : V → V} (hf : ∀ (u : V), G.Adj u (f u) ∧ f (f u) ≠ u) : ∃ (σ : ⦃i j : DoubledQuiver.OrientedQuiver G o⦄ → (i ⟶ j) → Bool), ∀ (u : DoubledQuiver.OrientedQuiver G o), ∃ (w : DoubledQuiver.OrientedQuiver G o), Nonempty (reorientVertex σ u ⟶ reorientVertex σ w)

If f chooses a neighbour at every vertex of G with no two vertices choosing each other, then some reorientation of any orientation of G has no sinks: turning around the arrows j ⟶ i with f i = j leaves every vertex u with the outgoing arrow u ⟶ f u.

def SimpleGraph.Coloring.sourceSink {V : Type u_1} {G : SimpleGraph V} (C : G.Coloring Bool) : TauCeti.DoubledQuiver.Orientation G

The source--sink orientation supplied by a two-colouring: an edge is directed toward its endpoint of colour true.

@[simp]

theorem SimpleGraph.Coloring.mem_sourceSink_iff {V : Type u_1} {G : SimpleGraph V} (C : G.Coloring Bool) (d : G.Dart) : d ∈ C.sourceSink ↔ C d.toProd.2 = true

A dart belongs to the source--sink orientation exactly when its target has colour true.