Choosing a neighbour at every vertex without mutual choices

A function f : V → V with G.Adj u (f u) and f (f u) ≠ u for every vertex u chooses a neighbour at every vertex so that no two vertices choose each other. Orienting each edge {u, f u} away from u is then consistent, and every vertex is the tail of an edge: such a choice is the same as an orientation of G in which no vertex is a sink.

A preconnected graph with a cycle admits such a choice: go once around the cycle, and send every other vertex to a neighbour strictly closer to the cycle. In a finite tree there is no such choice, since the choice would give the tree as many edges as vertices.

Main results

• SimpleGraph.exists_forall_adj_and_apply_apply_ne_of_forall_reachable: if the vertices of a set S already choose neighbours in S without mutual choices, and every vertex can reach S, then the choice extends to all vertices.
• SimpleGraph.Walk.IsCycle.exists_forall_adj_and_apply_apply_ne: the vertices of a cycle choose their successors along it without mutual choices.
• SimpleGraph.Preconnected.exists_forall_adj_and_apply_apply_ne_of_not_isAcyclic: a preconnected graph which is not acyclic has a choice of neighbours without mutual choices.

theorem SimpleGraph.exists_forall_adj_and_apply_apply_ne_of_forall_reachable {V : Type u_1} (G : SimpleGraph V) {S : Set V} (g : V → V) (hg : ∀ s ∈ S, G.Adj s (g s) ∧ g s ∈ S ∧ g (g s) ≠ s) (hS : ∀ (u : V), ∃ s ∈ S, G.Reachable u s) : ∃ (f : V → V), (∀ s ∈ S, f s = g s) ∧ ∀ (u : V), G.Adj u (f u) ∧ f (f u) ≠ u

Extending a choice of neighbours without mutual choices. Suppose that g chooses, at every vertex of a set S, a neighbour in S, and that no two vertices of S choose each other. If every vertex can reach S, then some f chooses a neighbour at every vertex, still without mutual choices: it agrees with g on S and moves every other vertex strictly closer to S.

theorem SimpleGraph.Walk.IsCycle.exists_getVert_eq {V : Type u_1} {G : SimpleGraph V} {u s : V} {p : G.Walk u u} (hp : p.IsCycle) (hs : s ∈ p.support) : ∃ i < p.length, p.getVert i = s

Every vertex of a cycle is p.getVert i for some index i before the end of the cycle.

theorem SimpleGraph.Walk.IsCycle.exists_forall_adj_and_apply_apply_ne {V : Type u_1} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (hp : p.IsCycle) : ∃ (g : V → V), ∀ s ∈ p.support, G.Adj s (g s) ∧ g s ∈ p.support ∧ g (g s) ≠ s

Going once around a cycle chooses neighbours without mutual choices. The vertices of a cycle p have a choice g of neighbours on p such that no two of them choose each other: g sends p.getVert i to p.getVert (i + 1).

theorem SimpleGraph.Preconnected.exists_forall_adj_and_apply_apply_ne_of_not_isAcyclic {V : Type u_1} {G : SimpleGraph V} (hG : G.Preconnected) (hc : ¬G.IsAcyclic) : ∃ (f : V → V), ∀ (u : V), G.Adj u (f u) ∧ f (f u) ≠ u

A preconnected graph which is not acyclic has a choice of neighbours without mutual choices: some f sends every vertex u to a neighbour f u with f (f u) ≠ u. Equivalently, G has an orientation without sinks.