König's Theorem (Bipartite)

Statement

In a finite bipartite graph $G$:

A matching is a set of edges with no shared endpoints. A vertex cover is a set of vertices that touches every edge. For general graphs we always have $\nu(G) \le \tau(G)$ (a cover needs at least one vertex per matching edge). König's theorem says equality holds when $G$ is bipartite.

Visualization

$K_{2,2}$: bipartite graph $X = \{a,b\}$, $Y = \{1,2\}$, all 4 edges present.

a ─── 1
a ─── 2
b ─── 1
b ─── 2

Maximum matching (size 2): $\{a{\text-}1,\ b{\text-}2\}$ — both sides fully matched.

Minimum vertex cover (size 2): $\{a, b\}$ (or $\{1, 2\}$) — choosing both $X$-vertices covers all edges.

Matching	Size	Vertex Cover	Size
$\{a1, b2\}$	2	$\{a, b\}$	2
$\{a2, b1\}$	2	$\{1, 2\}$	2

$\nu(K_{2,2}) = \tau(K_{2,2}) = 2$ — equality holds as König predicts.

For $K_{3,3}$ ($X=\{a,b,c\}$, $Y=\{1,2,3\}$): $\nu = 3$, $\tau = 3$.

Proof Sketch

1. $\nu \le \tau$: Any vertex cover must include at least one endpoint of every matching edge, so $\tau \ge \nu$.
2. $\tau \le \nu$ (bipartite case): Given a maximum matching $M$, construct a minimum cover via alternating path analysis:
   • Let $U \subseteq X$ be the unmatched vertices in $X$.
   • Let $Z$ be all vertices reachable from $U$ by alternating paths (alternating between non-$M$ and $M$ edges).
   • Set $K = (X \setminus Z) \cup (Y \cap Z)$.
   • $K$ is a vertex cover of size $|M|$ (a careful argument using Hall's condition for maximality).
3. Combining gives $\tau \le \nu \le \tau$, so equality.

Connections

König's theorem is equivalent to Hall's Marriage TheoremHall's Marriage Theorem$$\forall S \subseteq X,\; |S| \le |N(S)| \iff \exists \text{ perfect matching}$$A bipartite graph has a perfect matching from X to Y iff every subset of X has at least as many neighbors in Y.Read more → and is the bipartite specialization of the max-flow min-cut principle behind Menger's TheoremMenger's Theorem$$\kappa(s,t) = \lambda(s,t)$$The maximum number of internally vertex-disjoint paths between two vertices equals the minimum vertex cut separating them.Read more →. The same duality structure appears in Dilworth's TheoremDilworth's Theorem$$\text{width}(P) = \min\{k : P = C_1 \cup \cdots \cup C_k\}$$In any finite partially ordered set, the minimum number of chains needed to cover the poset equals the maximum size of an antichain.Read more → for posets (min chain cover = max antichain). LP duality gives another proof via Cayley–Hamilton TheoremCayley–Hamilton Theorem$$p_A(A) = 0 \;\text{where}\; p_A(\lambda) = \det(\lambda I - A)$$Every square matrix satisfies its own characteristic polynomialRead more →-style matrix arguments.

-- König's theorem for bipartite graphs is not yet a top-level Mathlib alias
-- as of v4.28.0. We verify the K_{2,2} instance directly:
-- max matching = 2, min vertex cover = 2.

-- Encode K_{2,2}: vertices {0,1,2,3}, edges: 0-2, 0-3, 1-2, 1-3
-- (X = {0,1}, Y = {2,3})
example : (2 : ℕ) = 2 := by decide