Prove2Me

Lemma 11 — two points of HH supported on the same circuit are proportional

Proved
WhitneyMatroid.Fano.proportional_of_inZ_circuit

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

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

Let M′\mathbf M' be a real matrix with matroid M′M', let M\mathbf M be a circuit matrix of M′\mathbf M', and let HH be the subspace spanned by the rows of M\mathbf M. If P=ei1+⋯+eipP=e_{i_1}+\cdots+e_{i_p} is a circuit of M′M' and (b1,…,bn)(b_1,\dots,b_n), (b1′,…,bn′)(b'_1,\dots,b'_n) are points of HH that are both in Zi1⋯ipZ_{i_1\cdots i_p}, then the two are proportional:

(b1′,…,bn′)=c (b1,…,bn)for some real c≠0.(b'_1,\dots,b'_n)=c\,(b_1,\dots,b_n)\qquad\text{for some real } c\neq 0.

In particular the row of a circuit in a circuit matrix is determined up to a nonzero factor. Whitney uses this rigidity to normalise the matrix (16.3) in §16.

Preamble
import Mathlib
import Definitions.Def_WhitneyMatroid_Fano_IsMatroidOf
import Definitions.Def_WhitneyMatroid_Fano_IsCircuitMatrix
Formal statement
namespace WhitneyMatroid.Fano

/-- Whitney, Lemma 11 (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 `P = {i₁, …, i_p}` is a circuit of `M′` and the points `b`, `b′` of `H` are both in
`Z_{i₁⋯i_p}`, then they are proportional: `b′ = c • b` for some nonzero real `c`. -/
theorem proportional_of_inZ_circuit {ι : Type*} [Fintype ι] {m : ℕ} {κ : Type*}
    (A : Matrix (Fin m) ι ℝ) (M' : Matroid ι) (B : Matrix κ ι ℝ)
    (row : κ ≃ {P : Set ι // M'.IsCircuit P}) (hB : IsCircuitMatrix M' A B row)
    (P : Set ι) (hP : M'.IsCircuit P) (b b' : ι → ℝ)
    (hb : b ∈ Submodule.span ℝ (Set.range B)) (hb' : b' ∈ Submodule.span ℝ (Set.range B))
    (hbP : InZ b P) (hb'P : InZ b' P) :
    ∃ c : ℝ, c ≠ 0 ∧ b' = c • b := by sorry

end WhitneyMatroid.Fano
Source
Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 528, Lemma 11
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