Sands-Sauer-Woodrow Corollary 2: a two-coloured tournament has a monochromatic sink
OpenSandsSauerWoodrow.two_coloured_tournament_sinkThis is Corollary 2 of Sands, Sauer and Woodrow, On monochromatic paths in edge-coloured digraphs, J. Combin. Theory Ser. B 33 (1982), 271–275, stated on p. 273.
Let be a tournament on a nonempty finite set of vertices — that is, a directed graph in which every two distinct vertices are joined by exactly one arc — and let each arc of carry one of three colours, only the colours and being used. Then there is a vertex such that for every vertex there is a directed path from to all of whose arcs have the same colour.
The common colour may depend on , and the path is not required to be short: the source observes that no bound on its length is possible. In the source's terms the conclusion says that the tournament contains a monochromatic sink. This is the settled two-colour case of the question raised by Erdős on p. 275 of the same paper, whether three colours force either a rainbow directed triangle or such a vertex; that three-colour question is open.
Formalization Note. A colouring is a function on all ordered pairs of vertices; the hypothesis constrains its values only on arcs, which is all the conclusion depends on. The source allows loops and multiple edges; here a digraph is a relation and is a tournament, so neither occurs. Nonemptiness of is required: for an empty vertex set there is no vertex to exhibit.
import Definitions.Def_opg1808_colored_tournaments open OPG1808 universe u
namespace SandsSauerWoodrow
theorem two_coloured_tournament_sink {V : Type u} [Fintype V] [Nonempty V]
(D : Digraph V) (color : ArcColoring V) (htournament : IsTournament D)
(htwo : ∀ u v, D u v → (color u v = 0 ∨ color u v = 1)) :
∃ v : V, ∀ x : V, x ≠ v → MonochromaticallyReaches D color x v := by sorry
end SandsSauerWoodrow