Geelen, Gerards, Kapoor: seven excluded minors for $\mathrm{GF}(4)$

Statement. The theorem TenChallenges.challenge_02_r4_B7 asserts the proposition $\mathrm{statement}_{02}(4, 7)$, a definition from this bundle, which unfolds to the following: for every natural number $p$ and every natural number $m$, assuming (as an instance-style hypothesis) that $p$ is a prime number, if $0 < m$ and $p^m \le 4$, then $\mathrm{ExcludedMinorsAtMost}(p, m, 7)$ holds.

The hypotheses "$p$ prime, $m \ge 1$, $p^m \le 4$" are satisfied by exactly three pairs, $(p, m) = (2, 1)$, $(3, 1)$ and $(2, 2)$. Hence the theorem asserts the conjunction of $\mathrm{ExcludedMinorsAtMost}(2, 1, 7)$, $\mathrm{ExcludedMinorsAtMost}(3, 1, 7)$ and $\mathrm{ExcludedMinorsAtMost}(2, 2, 7)$: one statement for each of $\mathrm{GF}(2)$, $\mathrm{GF}(3)$ and $\mathrm{GF}(4)$, each with the bound $B = 7$ applied separately to that field (each field gets its own set $S$ of at most $7$ matroids; there is no joint bound).

Here $\mathrm{GF}(p^m)$ denotes Mathlib's GaloisField p m, the finite field defined as the splitting field of $X^{p^m} - X$ over $\mathbb{Z}/p\mathbb{Z}$; because $m \ge 1$ is assumed, it has exactly $p^m$ elements.

Unfolding $\mathrm{ExcludedMinorsAtMost}(p, m, B)$ (bundle definition). It says: there exists a finite set $S$ of matroids on the type $\mathbb{N}$ (Mathlib matroids whose ground set is a set of natural numbers; the members of $S$ are pairwise distinct as matroids, but nothing requires them to be pairwise non-isomorphic, to have finite ground sets, to be excluded minors, or to be non-representable) such that

and for every type $\beta$ (any type in Lean's lowest universe) and every Mathlib matroid $M$ on $\beta$ whose ground set $E(M)$ is finite, if $M$ is an excluded minor for $\mathrm{GF}(p^m)$-representability (in the sense defined below), then there exists some $N \in S$ with $N \cong M$ (in the sense defined below). The set $S$ is chosen once, before $\beta$ and $M$ are quantified. $S = \emptyset$ is permitted; in that case the claim is that no finite matroid is an excluded minor.

Excluded minor (bundle definition $\mathrm{IsExcludedMinorFor}(P, M)$, used with $P =$ "is $\mathrm{GF}(p^m)$-representable"). $M$ is an excluded minor if and only if both

• $M$ is not $\mathrm{GF}(p^m)$-representable, and
• every matroid $N$ on the same type $\beta$ with $N <_m M$ is $\mathrm{GF}(p^m)$-representable.

Here $N <_m M$ is Mathlib's strict-minor relation: $N \le_m M$ and not $M \le_m N$, where $N \le_m M$ means that $N = (M / C) \setminus D$ for some sets $C, D \subseteq \beta$ (Mathlib's contraction of $C$ followed by deletion of $D$; $C$ and $D$ are arbitrary subsets of $\beta$, not required to be disjoint or to lie inside $E(M)$). By Mathlib lemmas, $N <_m M$ is equivalent to "$N \le_m M$ and $N \ne M$", and also to "$N \le_m M$ and $E(N) \subsetneq E(M)$".

Representability (bundle definition $\mathrm{IsGFRepresentable}(p, m, M)$ for a matroid $M$ on a type $\beta$). $M$ is $\mathrm{GF}(p^m)$-representable if and only if there exist a type $W$ (in Lean's lowest universe) together with an additive commutative group structure on $W$ and a $\mathrm{GF}(p^m)$-module structure on $W$ (so $W$ is an arbitrary vector space over $\mathrm{GF}(p^m)$; no finite-dimensionality is required), and a function $v : \beta \to W$ (defined on all of $\beta$, not only on $E(M)$), such that for every subset $I \subseteq \beta$,

The right-hand side is Mathlib's LinearIndepOn: linear independence of the family indexed by the elements of $I$ (so, in particular, $x \mapsto v_x$ is injective on $I$ and $v_x \ne 0$ for every $x \in I$). The subsets $I$ range over all subsets of $\beta$, including those not contained in $E(M)$; since in Mathlib every independent set of a matroid is contained in its ground set, for such $I$ the left-hand side is false, so the family $(v_x)_{x \in I}$ must be linearly dependent (for $I = \{x\}$ with $x \notin E(M)$ this forces $v_x = 0$).

Isomorphism (bundle definition Matroid.IsIso, not Mathlib's notion). For $N$ a matroid on $\mathbb{N}$ and $M$ a matroid on $\beta$, $N \cong M$ means: there exists a bijection $e : E(N) \to E(M)$ such that for every subset $I \subseteq E(N)$,

Finiteness. The hypothesis on $M$ is Mathlib's Matroid.Finite, which says exactly that the ground set $E(M)$ is a finite set; the type $\beta$ itself may be infinite.

In summary, the theorem asserts: for each of the three fields $\mathbb{F} = \mathrm{GF}(2)$, $\mathrm{GF}(3)$, $\mathrm{GF}(4)$ separately, there is a set $S_{\mathbb{F}}$ consisting of at most seven matroids on $\mathbb{N}$ such that every matroid $M$ (on any type) with finite ground set which is not $\mathbb{F}$-representable but all of whose strict minors are $\mathbb{F}$-representable is isomorphic, via a bijection of ground sets carrying independent sets exactly to independent sets, to a member of $S_{\mathbb{F}}$.