Prove2Me

Theorem 27 — a subspace of EnE_n has a unique associated matroid

Proved
WhitneyMatroid.Duality.exists_unique_associated

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

linear-algebramatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let HH be a hyperplane through the origin (a linear subspace) of nn-dimensional Euclidean space EnE_n. For a set SS of coordinates let rH(S)r_H(S) be the dimension of the projection of HH onto the coordinate subspace of the coordinates in SS. Then there is exactly one matroid MM on the elements e1,…,ene_1,\dots,e_n (one per coordinate) whose rank function is rHr_H:

∃! Msuch thatrM({ei:i∈S})=rH(S)  for all S⊆{1,…,n}.\exists!\, M\quad\text{such that}\quad r_M(\{e_i : i\in S\}) = r_H(S)\ \text{ for all } S\subseteq\{1,\dots,n\}.

This is what makes "the matroid associated with HH" well defined; it is the matroid in Theorem 28.

Formalization Note Matroids are Mathlib Matroid (Fin n) with ground set all of Fin n; the rank condition is the predicate IsAssociated (rank eRk equal to the finrank of the coordinate projection of HH). Uniqueness is among all such matroids.

Preamble
import Mathlib
import Definitions.Def_WhitneyMatroid_Duality_IsAssociated
Formal statement
namespace WhitneyMatroid.Duality

/-- Whitney, Theorem 27 (p. 526): there is a unique matroid `M` associated with any hyperplane `H`
through the origin in `Eₙ`, i.e. a unique matroid on the coordinates `e₁, …, eₙ` in which every
subset has as rank the dimension of the projection of `H` onto the corresponding coordinate
subspace. -/
theorem exists_unique_associated (n : ℕ) (H : Submodule ℝ (EuclideanSpace ℝ (Fin n))) :
    ∃! M : Matroid (Fin n), IsAssociated M H := by sorry

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