Matroids in lean

Stream: maths

[Bryan Gin-ge Chen]

As my next learning project, I've moved on from Fibonacci numbers and have been working on a formalization of matroids based on the book "Matroid theory" by Oxley. Roughly speaking, a matroid on a set is a family of subsets that encodes an abstract version of linear dependence between the elements, and they appear in many different guises in combinatorics and related fields. My work-in-progress is in my lean-matroids repository. In "lean" terms, I've defined there 3 complicated structures which build off of data.finset and proven that they are equivalent to each other.

This kind of fiddly combinatorial stuff seems to be a bit outside the interests of people here, but nonetheless I would be grateful for any feedback or suggestions on the style of the proofs. And thanks very much to everyone here for the help I've received so far! I'm off to bed now but I'll be back with various questions later on.

[Kevin Buzzard]

[off-topic: I have an uncared-for repo about Fibonacci numbers by the way -- https://github.com/kbuzzard/lean-squares-in-fibonacci . I am interested in the result, it's just very low priority right now. So if you ever feel like coming back...]

[Bryan Gin-ge Chen]

I noticed that matrices have been added to mathlib and that there's more stuff along the way in "kbb". Is there a convenient way to work with linear dependence of / independence of / subspaces spanned by rows of a matrix? Sorry, I'm asking this without having taken a careful look at the files in mathlib yet, in the hopes that someone will know how to do this off the top of their head.

[Kevin Buzzard]

The kbb stuff was just a surprise appearance. I would recommend that you formalise a precise statement and ask if it can be proved, or formulate a precise object and ask if it can be defined. Or several statements and objects if you'd rather.

[Bryan Gin-ge Chen]

The code has evolved a fair bit since I posted this thread. The latest version is currently in the "fintype2" branch

In the first version, I started out using finsets for everything (including the ground set) (now living in matroids-old.lean) and managed to formalize the independent set, circuits, bases and rank function definitions of matroids as well as various equivalences between them.

After thinking about Mario's comments here and here, I then switched to using a fintype for the ground set (matroids.lean), which was a fairly painless refactoring up until I had to define restrictions of matroids (right before defining rank functions). That's where I'm stuck now.

I think I probably need to define "submatroids" as a new structure to continue (like how mathlib defines both groups and subgroups separately), since I've hit a wall juggling subtypes and finsets of the ground set. At the same time, I've also been thinking it may make more sense to rework everything in terms of sets instead of finsets.

[Adam Topaz]

Just wondering -- Is there a particular reason to use finite types? Algebraic (in)dependence in field extensions, for example, forms a finitary matroid which is not finite, right?

[Bryan Gin-ge Chen]

I started formalizing finite matroids since I was following Oxley's book. Presumably a decent amount of the work could carry over to finitary matroids, but I haven't tried.