Theorem 16 — non-separable of nullity 1 iff circuit

Proved

WhitneyMatroid.Components.nonSeparable_nullity_one_iff_isCircuit

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 $X\subseteq E$ . Write $n(X)=\rho(X)-r(X)$ for the nullity of $X$ ( $\rho(X)$ the number of its elements). Then

X \text{ is non-separable and } n(X)=1 \iff X \text{ is a circuit of } M .

Circuits (minimal dependent sets) are thus exactly the non-separable submatroids of the smallest possible positive nullity; they are the building blocks of non-separable matroids (Theorem 17).

Formalization Note Whitney states the theorem for a matroid $M$ ; here $X$ is a subset of the ground set of an ambient finite matroid, which is the same statement applied to the submatroid $X$ (a set is a circuit of the submatroid $X$ iff it is a circuit of $M$ contained in $X$ ). Circuits are Mathlib's Matroid.IsCircuit. A loop $\{e\}$ is a circuit, non-separable, and of nullity $1$ .

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_Components_IsSeparable
import Definitions.Def_WhitneyMatroid_Components_nullity

Formal statement

namespace WhitneyMatroid.Components

theorem nonSeparable_nullity_one_iff_isCircuit {α : Type*} (M : Matroid α) [M.Finite]
    (X : Set α) (hX : X ⊆ M.E) :
    (IsNonSeparable M X ∧ nullity M X = 1) ↔ M.IsCircuit X := by sorry

end WhitneyMatroid.Components

Source

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

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