Modularity, Extensions and Connectivity in Infinite Matroids
Mattias Ehatamm, Peter Nelson, Fernanda Rivera Omana
math.CO
Apr 22, 2026 · v1
TL;DR
Provides a Lean4-formalized repository of all main results on modularity, extensions, and connectivity in infinite matroids.
Abstract
We generalize the well-studied notion of a modular pair of a finite matroid to arbitrary families of sets in infinite matroids, and use it to develop the theory of infinite matroids in several as-yet-unexplored areas. Our results include a complete theory of single-element extensions, a description of the relationship between quotients and projections, a proof that matroids for which every flat is modular must be finitary, and two new perspectives on the infinite matroid connectivity parameter λ. In most cases, existing theory for finite matroids either fails completely or does not extend in obvious ways, and as a result we develop multiple new techniques for reasoning about infinite matroids, including establishing well-behaved infinite analogues of nullity, local connectivity and skewness. We also point to an online repository containing formalized proofs of all our results using the lean4 proof assistant
Problem
Much finite-matroid theory around modular pairs, single-element extensions, quotients, and connectivity either fails or does not extend obviously to infinite matroids.
Approach
The authors generalize modular pairs to arbitrary families of sets in infinite matroids and develop single-element extensions, the relationship between quotients and projections, modular flats, and the connectivity parameter lambda, introducing infinite analogues of nullity, local connectivity, and skewness. All results are formalized in the Lean4 proof assistant in an online repository.
Results
A complete theory of single-element extensions, a proof that matroids in which every flat is modular must be finitary, and new perspectives on the infinite connectivity parameter, with machine-checked Lean4 statements and proofs for all results.
