Prove2Me

Theorem 15 — a matroid is the sum of its components in a unique manner

Proved
WhitneyMatroid.Components.component_decomposition_unique

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

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

Let MM be a finite matroid on a ground set EE, and let C(M)\mathcal C(M) be the set of its components. Then

  1. the components cover the ground set:
⋃K∈C(M)K=E;\bigcup_{K\in\mathcal C(M)} K = E;
  1. the expression is unique: if K\mathcal K is any family of components of MM whose union is EE, then K=C(M)\mathcal K = \mathcal C(M).

Together with Theorem 14 (distinct components are disjoint), this says that every matroid is, in exactly one way, the sum of disjoint components.

Formalization Note "Expressed as a sum of components" is read as "the union of a family of components equals the ground set", and "in a unique manner" as "that family is necessarily the family of all components". For the matroid with no elements both families are empty, which is why components are required to be nonempty.

Preamble
import Mathlib
import Definitions.Def_WhitneyMatroid_Components_IsSeparable
import Definitions.Def_WhitneyMatroid_Components_IsComponent
Formal statement
namespace WhitneyMatroid.Components

theorem component_decomposition_unique {α : Type*} (M : Matroid α) [M.Finite] :
    ⋃₀ {K : Set α | IsComponent M K} = M.E ∧
    ∀ 𝒦 : Set (Set α), (∀ K ∈ 𝒦, IsComponent M K) → ⋃₀ 𝒦 = M.E →
      𝒦 = {K : Set α | IsComponent M K} := by sorry

end WhitneyMatroid.Components
Source
Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 519, Theorem 15
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