Matroids in mathlib - feedback?

Stream: mathlib4

[Peter Nelson]

I'm making this post to solicit feedback on my lean4 matroid repo : https://github.com/apnelson1/Matroid

This work has undergone many iterations in the last couple of years, including huge refactors to make it more sane, and most recently a porting to lean4; now I think it's basically in a decent state for mathlib . The reason I haven't PRed it yet is that I'm waiting on a couple of PRs currently in the queue (#5908 and #5911) to give me some API for enat set cardinality and some minimality/maximality stuff that I need. (This is all in the ForMathlib subfolder).

I'm imagining that the sequence of PRs for the project itself will take quite some reviewing, since this adds up to a lot of new stuff, so I'm hoping to get a jump on at least the first one by inviting anyone interested to take a look now.

The first PR will be the contents of the file https://github.com/apnelson1/Matroid/blob/main/Matroid/Basic.lean, which defines matroids, and contains definitions of bases, independence, and bases of sets, and gives a few different constructors for matroids via sets of axioms. The docstring contains a detailed discussion of what I would consider the important design decisions. These decisions are mostly my own, and I'd be very happy to learn from experts how I could improve things.

The rest of the project is less well-document but I think it's nearly all in good shape - it contains around 5k loc, with API for the majority of basic matroid notions including duality, minors, circuits, closure, flats, hyperplanes, uniform matroids, the rank function, and relaxation. Apart from one or two leaf files, it's all sorry-free.

Notable omissions are linear representations of matroids and graph representations of matroids, which are important topics but are still work in progress.

[Jireh Loreaux]

@Peter Nelson I'll review #5908 tomorrow.

[Yaël Dillies]

Just to comment: For having helped Alena a bit with her sorries, I think the entire repo needs a general cleanup and design review. Once that's done, in mathlib it goes.

[Peter Nelson]

Yes, a design review is what I'm asking for. Do you have any specific comments?

[Eric Wieser]

Having only looked very briefly: is there a reason you need the ground set in matroids vs using the type directly?

[Eric Wieser]

For instance, why not

structure Matroid (α : Type _) where
  (Base : Set α → Prop)
  (exists_base' : ∃ B, Base B)
  (base_exchange' : Matroid.ExchangeProperty Base)
  (maximality' : ∀ X, Matroid.ExistsMaximalSubsetProperty (∃ B, Base B ∧ · ⊆ B) X)

instead of your

@[ext] structure Matroid (α : Type _) where
  (ground : Set α)
  (Base : Set α → Prop)
  (exists_base' : ∃ B, Base B)
  (base_exchange' : Matroid.ExchangeProperty Base)
  (maximality' : ∀ X, X ⊆ ground →
    Matroid.ExistsMaximalSubsetProperty (∃ B, Base B ∧ · ⊆ B) X)
  (subset_ground' : ∀ B, Base B → B ⊆ ground)

[Peter Nelson]

Yes, this is discussed in the docstring at the top. It's basically because of how often one needs to consider a number of related matroids on related but distinct ground sets.

[Kyle Miller]

https://github.com/apnelson1/Matroid/blob/main/Matroid/Basic.lean#L70

[Eric Wieser]

Many of the concerns there feel like they could also be applied to vector spaces, which we solved by having a separate Module _ V typeclass and a Submodule R V structure (and ModuleCat.{R} _ which bundles the ground type). Would a similar approach work for matroids, or are they not similar enough for the analogy to hold?

[Kyle Miller]

I was thinking about this earlier today, comparing it to the choices made for graphs. For graphs, this would affect graph homomorphisms, since a graph homomorphism is a map on vertices that carries adjacent vertices to adjacent vertices. If they used ground sets, then you'd need to either work with functions on the ambient type that restrict to the ground sets or with functions on the subtypes. With the first, you lose extensionality, and with the second, you have the annoyance of subtypes.

Are matroid homomorphisms used much in the literature? I once saw a definition for strong maps (inverse images of flats are flats), but I have no idea how important these are.

[Kyle Miller]

(For simple graphs, there docs#SimpleGraph with a fixed vertex type and docs#SimpleGraph.Subgraph for bundling in a ground set; here you can use the coincidence that the Subgraphs of the complete graph give you the alternative definition of a simple graph. Only SimpleGraph has homomomorphisms. @Eric Wieser I think this is closer of an analogy than Module/Submodule.)

[Johan Commelin]

Eric Wieser said:

Many of the concerns there feel like they could also be applied to vector spaces, which we solved by having a separate Module _ V typeclass and a Submodule R V structure (and ModuleCat.{R} _ which bundles the ground type). Would a similar approach work for matroids, or are they not similar enough for the analogy to hold?

To be fair, converting between these different POVs can be quite painful. (i) The DG-algebra challenge is still an open problem. (ii) Working with graded rings/modules is not as smooth in Lean as in the informal counterpart.

[Peter Nelson]

Strong/weak maps do show up, but aren't particularly central, at least to the research on my personal radar. (I have weak maps defined in my lean3 repo, where I hadn't yet adopted this 'ground set is a Set' approach).

A similar issue shows up when I define matroid isomorphisms in the Equivfile. They are defined using LocalEquiv, which is a little awkward. Dealing with minors, which are everywhere in the literature, is so absolutely hellish if the ground set is a type, that I've learned to live with such things.

[Eric Wieser]

@Johan Commelin, I agree that the Module/Submodule/ModuleCat design may not be perfect; but there's a lot of value to using the same approach throughout mathlib for consistency

[Peter Nelson]

I've thought about the module/submodule analogy; in fact, it kinda got me to where I am now with this. For matroid theory, one ends up being drawn towards absolutely everything in the API existing for the analogous object to a Submodule, and getting to a point where the Module object is secondary.

[Kyle Miller]

Eric Wieser said:

there's a lot of value to using the same approach throughout mathlib for consistency

Just so long as it's not a foolish consistency.

Already it's different because Module/Submodule/ModuleCat is designed around using typeclasses for implementing the usual synecdoche (that M is a module). Matroids don't use synecdoche.

[Kyle Miller]

Typeclasses also implement transparent coercions between different structures in the algebraic hierarchy, but I'm not sure matroids need that either.

[Peter Nelson]

I think the concrete problem with the ground set being a type is that you can't talk about minors reasonably. See the lemmas here, for example : https://github.com/apnelson1/Matroid/blob/main/Matroid/Minor.lean#L560

They are mathematically trivial, but would have formal statements involving canonical maps between images/preimages of coercions of four sets between multiple subtypes, subtypes of subtypes, etc. I tried this for a long long time, becoming intimately familiar with preimage_image_coe-type lemmas, but it just isn't sustainable.

[Kyle Miller]

Another potential design for minors (which definitely involves a tradeoff) is to introduce another type that records what should be deleted and what should be contracted. This at least works for graphs (you record a set of edges to keep and a subset of those edges to contract), but the issue is that you can't apply any theorems about graphs to minors without using a toGraph function.

It seems that the reasons for wanting this in graphs (such as avoiding quotient types until you really need them) don't apply to matroids though.

[Kyle Miller]

It's nice that for matroids with an embedded ground set you can get contraction-deletion as an Eq

[Peter Nelson]

Kyle Miller said:

It's nice that for matroids with an embedded ground set you can get contraction-deletion as an Eq

Yes. The first time I used rw with such an equality (after months of DTT hell) filled me with joy!

[Peter Nelson]

I actually think a similar approach might be reasonable for minors in graph theory in some cases. If you have an embedded edge and vertex set, then you can contract an edge uv by choosing one of the ends uv to contract it to, so you get a graph whose vertex and edge sets live in the same type, avoiding quotients. Tradeoffs abound, of course.

[Kyle Miller]

Yeah, though it's too bad that choosing representatives isn't very stable (ex: contracting an edge between two contracted components yields a representative that might have no relation to either components' representative), and the edge set won't generally be a subset of the original edge set.

[Peter Nelson]

the edge set will still be a subset if you have an edge type (if you're doing anything with minors, this seems almost a necessity to me)

[Peter Nelson]

(to be clear, I mean a type in which the edges are an embedded set)

[Peter Nelson]

Kyle Miller said:

Are matroid homomorphisms used much in the literature? I once saw a definition for strong maps (inverse images of flats are flats), but I have no idea how important these are.

On this topic, much of the interest of strong/weak maps can be captured in the special case where they are between two matroids on the same ground set; so my approach doesn't rule that out. Homomorphisms aren't really well-defined for general matroids, but they are pretty much just linear maps in the representable case, and that is quite compatible with the 'embedded ground sets' approach as well; elements outside the ground set are just 'zero'.

[Peter Nelson]

#6352
I started this before my kid was born; he's now 2.5 years old and I'm finally making a matroid PR!