Lemma 10 — the support of a point of $H$ is a union of circuits

Proved

WhitneyMatroid.Fano.support_isUnion_circuits

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

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

Let $\mathbf M'$ be a real matrix with matroid $M'$ , let $\mathbf M$ be a circuit matrix of $\mathbf M'$ , and let $H$ be the hyperplane (linear subspace) of $\mathbb R^n$ spanned by the rows of $\mathbf M$ . Let $(b_1,\dots,b_n)$ be a point of $H$ lying in $Z_{i_1\cdots i_p}$ , i.e. with $b_j\neq 0$ exactly for $j\in\{i_1,\dots,i_p\}$ . Then

N'=e_{i_1}+\cdots+e_{i_p}\ \text{ is the union of a set of circuits of } M'.

Here $e_i$ in $M'$ corresponds to the column $C_i$ . The lemma says that the supports of vectors in the row space of a circuit matrix are exactly built from circuits; it is used to produce circuits from vectors in Lemma 11 and Theorem 32.

Formalization Note The point of $H$ is any vector in the real span of the rows of $\mathbf M$ . A union of circuits is the union of a family (possibly empty, for the zero vector) of circuits of $M'$ .

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_Fano_IsMatroidOf
import Definitions.Def_WhitneyMatroid_Fano_IsCircuitMatrix

Formal statement

namespace WhitneyMatroid.Fano

/-- Whitney, Lemma 10 (p. 528). Let `B` (Whitney's `𝐌`) be the circuit matrix of the real matrix
`A` (Whitney's `𝐌′`), whose matroid is `M′`, and let `H` be the subspace spanned by the rows of
`B`. If a point `b` of `H` is in `Z_{i₁⋯i_p}`, i.e. its set of nonzero coordinates is
`N′ = {i₁, …, i_p}`, then `N′` is the union of a set of circuits of `M′`. -/
theorem support_isUnion_circuits {ι : Type*} [Fintype ι] {m : ℕ} {κ : Type*}
    (A : Matrix (Fin m) ι ℝ) (M' : Matroid ι) (B : Matrix κ ι ℝ)
    (row : κ ≃ {P : Set ι // M'.IsCircuit P}) (hB : IsCircuitMatrix M' A B row)
    (b : ι → ℝ) (hb : b ∈ Submodule.span ℝ (Set.range B)) (N' : Set ι) (hbN : InZ b N') :
    ∃ 𝒞 : Set (Set ι), (∀ C ∈ 𝒞, M'.IsCircuit C) ∧ ⋃₀ 𝒞 = N' := by sorry

end WhitneyMatroid.Fano

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 528, Lemma 10

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

Lemma 10 — the support of a point of HHH is a union of circuits

Lemma 10 — the support of a point of $H$ is a union of circuits