Theorem 18 — three characterizations of the components

Proved

WhitneyMatroid.Components.components_tfae

by mikedeng1 · 1 vote · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

connectivitymatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $M$ be a finite matroid on a ground set $E$ with rank function $r$ , and let $M_1,\dots,M_p$ be distinct, nonempty, non-separable subsets of $E$ with $M_1+\cdots+M_p=E$ . Then the following statements are equivalent:

$M_1,\dots,M_p$ are the components of $M$ (the set $\{M_1,\dots,M_p\}$ is the set of components);
no two of $M_1,\dots,M_p$ have common elements, and there is no circuit of $M$ containing elements of more than one of them;

r(E) = r(M_1)+\cdots+r(M_p).

The theorem shows that the components are detected by rank additivity alone, and that they are separated from each other by circuits.

Formalization Note Whitney tacitly takes $M_1,\dots,M_p$ to be distinct, nonempty matroids. Both are made explicit: if two of them could coincide, a single loop $e$ listed twice ( $M_1=M_2=\{e\}$ ) would satisfy (3) but not (2); if one could be empty, (2) and (3) would hold but (1) would fail. The family is indexed by $\mathrm{Fin}\,p$ ; ranks are Mathlib's M.eRk, finite here. As Whitney remarks, rank cannot be replaced by nullity in (3).

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_Components_IsSeparable
import Definitions.Def_WhitneyMatroid_Components_IsComponent

Formal statement

namespace WhitneyMatroid.Components

theorem components_tfae {α : Type*} (M : Matroid α) [M.Finite]
    (p : ℕ) (Ms : Fin p → Set α) (hcover : (⋃ i, Ms i) = M.E)
    (hinj : Function.Injective Ms) (hne : ∀ i, (Ms i).Nonempty)
    (hns : ∀ i, IsNonSeparable M (Ms i)) :
    [Set.range Ms = {K : Set α | IsComponent M K},
     (∀ i j, i ≠ j → Disjoint (Ms i) (Ms j)) ∧
       ¬ ∃ (P : Set α) (i j : Fin p), i ≠ j ∧ M.IsCircuit P ∧
         (P ∩ Ms i).Nonempty ∧ (P ∩ Ms j).Nonempty,
     M.eRk M.E = ∑ i, M.eRk (Ms i)].TFAE := by sorry

end WhitneyMatroid.Components

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 520, Theorem 18

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph