Representability over $\mathrm{GF}(p^m)$, excluded minors, matroid isomorphism

Read-back of the four definitions in Def_TenChallenges_MatroidRepresentability (namespace-free, with α, β arbitrary types).

Background used by all four definitions. A matroid $M$ on a type $\alpha$ is Mathlib's Matroid α: a ground set $E(M) \subseteq \alpha$ (an arbitrary subset of $\alpha$: it may be infinite, and it may be empty), together with a predicate "$B$ is a base" and a predicate "$I$ is independent" on subsets of $\alpha$, subject to the axioms: a set is independent if and only if it is contained in some base; at least one base exists; bases satisfy the exchange property (for bases $B, B'$ and $a \in B \setminus B'$ there is $b \in B' \setminus B$ with $(B \setminus \{a\}) \cup \{b\}$ a base); for every $X \subseteq E(M)$, every independent subset of $X$ is contained in a maximal independent subset of $X$; every base is contained in $E(M)$. Consequently every independent set is a subset of $E(M)$, and $\emptyset$ is always independent. Infinite matroids are included.

---

1. $\mathrm{IsGFRepresentable}(p, m, M)$. Data: natural numbers $p, m$, a typeclass hypothesis that $p$ is prime, and a matroid $M$ on $\alpha$. Write $\mathrm{GF}(p^m)$ for Mathlib's GaloisField p m, the splitting field of $X^{p^m} - X$ over $\mathbb{Z}/p\mathbb{Z}$: for $m \ge 1$ this is the field with $p^m$ elements; for $m = 0$ the polynomial is $X^1 - X = 0$, so $\mathrm{GF}(p^0)$ is the splitting field of the zero polynomial, i.e. (up to isomorphism) $\mathbb{Z}/p\mathbb{Z}$ itself with $p$ elements, not a one-element field. The definition asserts:

there exist a type $W$ (in the lowest universe), an additive commutative group structure on $W$, a $\mathrm{GF}(p^m)$-vector-space structure on $W$, and a function $v : \alpha \to W$ (defined on every element of $\alpha$, not only on $E(M)$), such that for every subset $I \subseteq \alpha$ (not only subsets of $E(M)$)

$$I \text{ is independent in } M \quad\Longleftrightarrow\quad (v(x))_{x \in I} \text{ is linearly independent over } \mathrm{GF}(p^m).$$

"Linearly independent" is Mathlib's LinearIndepOn: the family of vectors indexed by the elements of $I$ is linearly independent, meaning the linear map sending a finitely supported coefficient function $c : I \to \mathrm{GF}(p^m)$ to $\sum_{x \in I} c_x\, v(x)$ is injective (no non-trivial finite linear combination vanishes). Because the family is indexed by $I$ and not by the set of vectors, two distinct $x \neq y$ in $I$ with $v(x) = v(y)$ make the family dependent, $v(x) = 0$ makes $\{x\}$ dependent, and the empty family is independent.

Edge cases: no bound is placed on the dimension of $W$ (it may be infinite-dimensional, or the zero space); no finiteness of $M$ is assumed. Since independent sets of $M$ lie inside $E(M)$, taking $I = \{x\}$ with $x \notin E(M)$ shows that the condition forces $v(x) = 0$ for every $x \notin E(M)$. If $W$ is the zero space, the condition holds only when $\emptyset$ is the sole independent set of $M$.

---

2. $\mathrm{IsExcludedMinorFor}(P, M)$. Data: a property $P$ of matroids on $\alpha$ and a matroid $M$ on $\alpha$. The definition asserts the conjunction

$$\neg P(M) \quad\text{and}\quad \forall N \text{ a matroid on } \alpha:\; N <_m M \implies P(N).$$

Here $N <_m M$ is Mathlib's strict minor relation IsStrictMinor: $N \le_m M$ and not $M \le_m N$, where $N \le_m M$ (Mathlib's IsMinor) means there exist sets $C, D \subseteq \alpha$ (not required to be disjoint, nor to be contained in $E(M)$) with

$$N = (M / C) \setminus D,$$

i.e. $N$ is obtained by contracting $C$ and then deleting $D$. Deletion $M \setminus D$ is the restriction of $M$ to $E(M) \setminus D$ (its independent sets are the $M$-independent subsets of $E(M) \setminus D$); contraction $M / C$ is defined as $(M^{*} \setminus C)^{*}$, the dual of the deletion of $C$ from the dual matroid $M^{*}$, and has ground set $E(M) \setminus C$. Mathlib's documentation states that $N <_m M$ is equivalent to "$N$ is a minor of $M$ and $N \neq M$".

Edge cases: only matroids on the same type $\alpha$ are considered as minors. If $M$ has no strict minors at all (for instance when $E(M) = \emptyset$, since any minor has ground set inside $E(M)$), the second clause holds vacuously and $M$ is an excluded minor for $P$ exactly when $\neg P(M)$. The definition does not require $E(M)$ to be finite.

---

3. $\mathrm{IsIso}(M, N)$ (declared here under the name Matroid.IsIso; this is a definition of this bundle, not a Mathlib notion). Data: a matroid $M$ on $\alpha$ and a matroid $N$ on $\beta$ (possibly different types). The definition asserts:

there exists a bijection $e : E(M) \to E(N)$ between the ground sets such that for every subset $I \subseteq E(M)$,

$$I \text{ is independent in } M \quad\Longleftrightarrow\quad e(I) = \{\, e(x) : x \in I \,\} \text{ is independent in } N.$$

Only subsets of the ground set $E(M)$ are compared. The existence of the bijection forces $E(M)$ and $E(N)$ to have the same cardinality (both may be empty, or both infinite). Nothing else (e.g. equality of the underlying types) is required.

---

4. $\mathrm{ExcludedMinorsAtMost}(p, m, B)$. Data: natural numbers $p, m$, a typeclass hypothesis that $p$ is prime, and a natural number $B$. The definition asserts:

there exists a finite set $S$ of matroids on the type $\mathbb{N}$ (each member has ground set some subset of $\mathbb{N}$, with no restriction: possibly infinite, possibly empty) with

$$|S| \le B,$$

such that for every type $\beta$ (in the lowest universe) and every matroid $M$ on $\beta$: if $E(M)$ is finite, and $M$ is an excluded minor for the property "$\mathrm{IsGFRepresentable}(p, m, \cdot)$" in the sense of Definition 2 (that is: $M$ is not $\mathrm{GF}(p^m)$-representable in the sense of Definition 1, and every strict minor $N <_m M$ among matroids on $\beta$ is $\mathrm{GF}(p^m)$-representable), then

$$\exists\, N \in S \text{ such that } \mathrm{IsIso}(N, M),$$

i.e. some $N \in S$ admits a bijection $E(N) \to E(M)$ carrying $N$-independent sets exactly to $M$-independent sets (Definition 3).

Edge cases: if $B = 0$ then $S = \emptyset$ and the statement says that no finite excluded minor exists for any type $\beta$. The members of $S$ are not required to be excluded minors themselves, to be finite, to be $\mathrm{GF}(p^m)$-representable or not, or to be pairwise non-isomorphic; $S$ may have fewer than $B$ elements. Excluded minors with infinite ground set are not constrained at all. The value $m = 0$ is permitted, in which case $\mathrm{GF}(p^0)$ is $\mathbb{Z}/p\mathbb{Z}$ as explained in Definition 1.