Orientations of multigraphs

An orientation of a multigraph orders the two ends of every actual edge. The edge identity is retained, so parallel edges can be oriented independently. A loop has equal tail and head and therefore gives one directed loop, without an additional choice of direction.

The explicit arrow family Graph.Orientation.Hom has one arrow for each actual edge, from its chosen tail to its chosen head. It can be supplied directly to quiver and network constructions without installing a Quiver instance on the graph's vertex type. Reversing an orientation reverses every arrow while preserving its edge identity.

Main declarations

• Graph.Orientation: an ordering of the ends of every actual edge.
• Graph.Orientation.ofEdgeEnds: an arbitrary orientation available for every multigraph.
• Graph.Orientation.ofHead: the orientation with prescribed heads.
• Graph.Orientation.reverse: reversal of every chosen edge direction.
• Graph.Orientation.Hom: the associated explicit arrow family.
• Graph.Orientation.totalHomEquiv: the total arrows are equivalent to the actual edges.

structure Graph.Orientation {V : Type u} {E : Type v} (G : Graph V E) : Type (max u v)

An orientation of a multigraph chooses a tail and head for every actual edge, compatible with that edge's incidence. Parallel edges retain separate choices, while a loop necessarily has the same tail and head.

• tail : ↑G.edgeSet → ↑G.vertexSet

  The chosen tail of an actual edge.

• head : ↑G.edgeSet → ↑G.vertexSet

  The chosen head of an actual edge.

• isLink (e : ↑G.edgeSet) : G.IsLink ↑e ↑(self.tail e) ↑(self.head e)

  The chosen tail and head are the two ends of the edge.

theorem Graph.Orientation.ext {V : Type u} {E : Type v} {G : Graph V E} {o₁ o₂ : G.Orientation} (htail : ∀ (e : ↑G.edgeSet), o₁.tail e = o₂.tail e) (hhead : ∀ (e : ↑G.edgeSet), o₁.head e = o₂.head e) : o₁ = o₂

Two orientations are equal when they choose the same tail and head for every edge.

theorem Graph.Orientation.ext_iff {V : Type u} {E : Type v} {G : Graph V E} {o₁ o₂ : G.Orientation} : o₁ = o₂ ↔ (∀ (e : ↑G.edgeSet), o₁.tail e = o₂.tail e) ∧ ∀ (e : ↑G.edgeSet), o₁.head e = o₂.head e

theorem Graph.Orientation.edgeEnds_eq {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : G.edgeEnds e = s(o.tail e, o.head e)

The unordered pair formed by the chosen tail and head is the edge's pair of ends.

theorem Graph.Orientation.tail_inc {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : G.Inc ↑e ↑(o.tail e)

The chosen tail is incident to its edge.

theorem Graph.Orientation.head_inc {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : G.Inc ↑e ↑(o.head e)

The chosen head is incident to its edge.

theorem Graph.Orientation.head_eq_of_tail_eq {V : Type u} {E : Type v} {G : Graph V E} {o₁ o₂ : G.Orientation} {e : ↑G.edgeSet} (h : o₁.tail e = o₂.tail e) : o₁.head e = o₂.head e

Two orientations choosing the same tail for an edge also choose the same head.

theorem Graph.Orientation.ext_of_tail {V : Type u} {E : Type v} {G : Graph V E} {o₁ o₂ : G.Orientation} (h : ∀ (e : ↑G.edgeSet), o₁.tail e = o₂.tail e) : o₁ = o₂

Two orientations are equal when they choose the same tail for every edge.

theorem Graph.Orientation.tail_eq_of_head_eq {V : Type u} {E : Type v} {G : Graph V E} {o₁ o₂ : G.Orientation} {e : ↑G.edgeSet} (h : o₁.head e = o₂.head e) : o₁.tail e = o₂.tail e

Two orientations choosing the same head for an edge also choose the same tail.

theorem Graph.Orientation.ext_of_head {V : Type u} {E : Type v} {G : Graph V E} {o₁ o₂ : G.Orientation} (h : ∀ (e : ↑G.edgeSet), o₁.head e = o₂.head e) : o₁ = o₂

Two orientations are equal when they choose the same head for every edge.

noncomputable def Graph.Orientation.ofHead {V : Type u} {E : Type v} {G : Graph V E} (head : ↑G.edgeSet → ↑G.vertexSet) (h : ∀ (e : ↑G.edgeSet), G.Inc ↑e ↑(head e)) : G.Orientation

The orientation choosing a prescribed incident vertex as the head of every edge; the tail is the other end, which is the head itself for a loop.

@[simp]

theorem Graph.Orientation.ofHead_head {V : Type u} {E : Type v} {G : Graph V E} (head : ↑G.edgeSet → ↑G.vertexSet) (h : ∀ (e : ↑G.edgeSet), G.Inc ↑e ↑(head e)) (e : ↑G.edgeSet) : (ofHead head h).head e = head e

@[simp]

theorem Graph.Orientation.ofHead_self {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) : ofHead o.head ⋯ = o

theorem Graph.Orientation.tail_eq_and_head_eq_or_tail_eq_and_head_eq {V : Type u} {E : Type v} {G : Graph V E} (o₁ o₂ : G.Orientation) (e : ↑G.edgeSet) : o₁.tail e = o₂.tail e ∧ o₁.head e = o₂.head e ∨ o₁.tail e = o₂.head e ∧ o₁.head e = o₂.tail e

Two orientations either agree on an edge or orient it in opposite directions.

noncomputable def Graph.Orientation.ofEdgeEnds {V : Type u} {E : Type v} (G : Graph V E) : G.Orientation

Every multigraph admits an orientation, obtained from a representative of each unordered pair of edge ends.

@[simp]

theorem Graph.Orientation.ofEdgeEnds_tail {V : Type u} {E : Type v} (G : Graph V E) (e : ↑G.edgeSet) : (ofEdgeEnds G).tail e = (Quot.out (G.edgeEnds e)).1

@[simp]

theorem Graph.Orientation.ofEdgeEnds_head {V : Type u} {E : Type v} (G : Graph V E) (e : ↑G.edgeSet) : (ofEdgeEnds G).head e = (Quot.out (G.edgeEnds e)).2

def Graph.Orientation.reverse {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) : G.Orientation

Reverse every edge of an orientation.

@[simp]

theorem Graph.Orientation.reverse_tail {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : o.reverse.tail e = o.head e

@[simp]

theorem Graph.Orientation.reverse_head {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : o.reverse.head e = o.tail e

@[simp]

theorem Graph.Orientation.reverse_reverse {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) : o.reverse.reverse = o

theorem Graph.Orientation.reverse_involutive {V : Type u} {E : Type v} {G : Graph V E} : Function.Involutive reverse

theorem Graph.Orientation.reverse_injective {V : Type u} {E : Type v} {G : Graph V E} : Function.Injective reverse

@[simp]

theorem Graph.Orientation.reverse_inj {V : Type u} {E : Type v} {G : Graph V E} {o₁ o₂ : G.Orientation} : o₁.reverse = o₂.reverse ↔ o₁ = o₂

def Graph.Orientation.reverseEquiv {V : Type u} {E : Type v} (G : Graph V E) : Equiv.Perm G.Orientation

Reversing every edge is an involutive equivalence on orientations.

@[simp]

theorem Graph.Orientation.reverseEquiv_apply {V : Type u} {E : Type v} (G : Graph V E) (o : G.Orientation) : (reverseEquiv G) o = o.reverse

theorem Graph.Orientation.tail_eq_head_iff_isLoopAt {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : o.tail e = o.head e ↔ G.IsLoopAt ↑e ↑(o.tail e)

An edge is a loop at its chosen tail exactly when its chosen tail and head coincide.

theorem Graph.Orientation.edgeEnds_isDiag_iff {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : (G.edgeEnds e).IsDiag ↔ o.tail e = o.head e

The unordered ends of an edge are diagonal exactly when the orientation makes it a loop arrow.

structure Graph.Orientation.Hom {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (x y : ↑G.vertexSet) : Type v

The explicit family of arrows selected by an orientation. An arrow from x to y is an actual edge whose chosen tail is x and whose chosen head is y.

• edge : ↑G.edgeSet

  The actual edge underlying the arrow.

• tail_eq : o.tail self.edge = x

  The arrow's source is the chosen tail of its edge.

• head_eq : o.head self.edge = y

  The arrow's target is the chosen head of its edge.

theorem Graph.Orientation.Hom.ext_iff {V : Type u} {E : Type v} {G : Graph V E} {o : G.Orientation} {x y : ↑G.vertexSet} {x✝ y✝ : o.Hom x y} : x✝ = y✝ ↔ x✝.edge = y✝.edge

theorem Graph.Orientation.Hom.ext {V : Type u} {E : Type v} {G : Graph V E} {o : G.Orientation} {x y : ↑G.vertexSet} {x✝ y✝ : o.Hom x y} (edge : x✝.edge = y✝.edge) : x✝ = y✝

theorem Graph.Orientation.Hom.isLink {V : Type u} {E : Type v} {G : Graph V E} {o : G.Orientation} {x y : ↑G.vertexSet} (a : o.Hom x y) : G.IsLink ↑a.edge ↑x ↑y

The underlying edge of an oriented arrow links its source and target.

def Graph.Orientation.arrow {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : o.Hom (o.tail e) (o.head e)

Regard an actual edge as the arrow from its chosen tail to its chosen head.

@[simp]

theorem Graph.Orientation.arrow_edge {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : (o.arrow e).edge = e

@[reducible, inline]

abbrev Graph.Orientation.TotalHom {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) : Type (max u v u)

All arrows of an orientation, with their source and target vertices.

def Graph.Orientation.totalHomEquiv {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) : o.TotalHom ≃ ↑G.edgeSet

The total arrows of an orientation are exactly the actual edges of the multigraph. This equivalence retains parallel edge identities and sends a loop to one arrow.

@[simp]

theorem Graph.Orientation.totalHomEquiv_apply {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (a : o.TotalHom) : o.totalHomEquiv a = a.snd.snd.edge

@[simp]

theorem Graph.Orientation.totalHomEquiv_symm_apply {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (e : ↑G.edgeSet) : o.totalHomEquiv.symm e = ⟨o.tail e, ⟨o.head e, o.arrow e⟩⟩

theorem Graph.Orientation.totalHom_edge_val_injective {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) : Function.Injective fun (a : o.TotalHom) => ↑a.snd.snd.edge

The edge identity determines an oriented arrow, including its endpoints.

def Graph.Orientation.reverseHomEquiv {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (x y : ↑G.vertexSet) : o.Hom x y ≃ o.reverse.Hom y x

Reversing an orientation reverses an arrow while retaining its edge identity.

@[simp]

theorem Graph.Orientation.reverseHomEquiv_edge {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) {x y : ↑G.vertexSet} (a : o.Hom x y) : ((o.reverseHomEquiv x y) a).edge = a.edge

@[simp]

theorem Graph.Orientation.reverseHomEquiv_symm_edge {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) {x y : ↑G.vertexSet} (a : o.reverse.Hom y x) : ((o.reverseHomEquiv x y).symm a).edge = a.edge

instance Graph.Orientation.instFiniteHomOfElemEdgeSet {V : Type u} {E : Type v} {G : Graph V E} (o : G.Orientation) (x y : ↑G.vertexSet) [Finite ↑G.edgeSet] : Finite (o.Hom x y)

An orientation has finitely many arrows between any two vertices when its actual edge set is finite.