Rado's theorem on matroids

Stream: Is there code for X?

[Michael Stoll]

Do we have Rado's theorem on matroids, or at least its linear algebra incarnation, which says the following?

Let $V$ be a vector space over a field $F$, let $I$ be a finite set, and let $Z_i \subseteq V$ for $i \in I$ be subsets such that $\dim \langle \bigcup_{j \in J} Z_j \rangle \ge \#J$ for each subset $J \subseteq I$. Then there exists a linearly independent family in $\prod_{i \in I} Z_i$.

Searching for "Rado" in mathlib seems to turn up only stuff on Radon-Nikodym measures...

[Kyle Miller]

I suppose we have the special case of when $V$ has some fixed basis and each $Z_i$ is the span of some subset of that basis, which is Hall's marriage theorem docs#finset.all_card_le_bUnion_card_iff_exists_injective

[Michael Stoll]

Yes; Hall's theorem is the special case when "independent" just means "pairwise distinct". But I need the more general version...

[Michael Stoll]

Actually, I'm struggling a bit with how to formalize the statement. Should I use a finset for I? Then it seems that to write a union of sets indexed by a finset, I have to turn the finset into a setand I have to turn the cardinality of the finset into a cardinal. I could probably work with a fintype instead. Then I need to open_locale classical to be able to talk about the cardinality of J : set \iota. I'll see what works better, but also appreciate comments on the pros and cons.

[Kyle Miller]

I haven't tested it, but I'd expect something in the neighborhood of this to capture what you'd want for the condition: (Z : I → submodule F V) : ∀ (J : finset I), J.card ≤ module.rank (⨆ (i ∈ J), Z i)

[Kyle Miller]

⨆ is the supremum of the collection of subspaces, which is the subspace generated by the union of all of them.

[Michael Stoll]

Only that the $Z_i$ are subsets, not subspaces, so my current attempt (in the fintype version) is

open_locale classical
open submodule

variables {F V ι : Type*} [field F] [add_comm_group V] [module F V] [fintype ι]

variables (F)

def hall_condition (Z : ι → set V) : Prop :=
∀ J : set ι, ↑(fintype.card J) ≤ module.rank F (span F (set.Union (J.restrict Z)))

variables {F}

theorem rado (Z : ι → set V) (hZ : hall_condition F Z) :
  ∃ v : ι → V, (∀ i, v i ∈ Z i) ∧ linear_independent F v := ...

(EDITED: condition v i ∈ Z i was missing.)
(Note that module.rank gives a cardinal.)

[Kyle Miller]

Again untested, but you should be able to use notation for set.Union along with finset here, which can be easier to work with when you're doing cardinalities sometimes.

def hall_condition (Z : ι → set V) : Prop :=
∀ J : finset ι, ↑J.card ≤ module.rank F (span F (⋃ (i ∈ j), Z i))

You can also use docs#nat.card instead of docs#fintype.card if you don't want to worry about fintype instances or computability.

[Kyle Miller]

Do you know if Rado's theorem is true when $I$ is infinite? I think the compactness theorem should apply, letting you lift a proof of the finite case to the arbitrary cardinality case. (This is what mathlib's Hall's theorem does.)

[Michael Stoll]

It probably extends in the same way. But I'll worry about that later...

[Kyle Miller]

It's just a good reason to not rely on ι being finite when you state hall_condition

[Kyle Miller]

Michael Stoll said:

Only that the $Z_i$ are subsets, not subspaces

Where in the theorem statement does it depend on them being subsets and not subspaces? I'd switched them to subspaces because it didn't look like it mattered.

[Kyle Miller]

Oh, I got it, nevermind. I kept seeing $\prod_i Z_i$ as a vector space, not a product of sets.

[Kevin Buzzard]

Is there docs#module.finrank ?

[Kevin Buzzard]

It's docs#finite_dimensional.finrank

[Michael Stoll]

I guess one decision to make here is whether to work with sets Z i or finsets Z i. I think only the latter version will generalize fairly easily to an infinite indexing type (a product of finite sets with the discrete topology is compact), but for a finite indexing type, general sets should be OK as well.

[Michael Stoll]

It would probably make sense to define an abstract notion of "independence" (of families over a type) and prove the theorem in this context (this is what Rado does in his paper from 1942). Then one can specialize to Hall's theorem, linear independence, algebraic independence, what have you. I don't think I want to develop the general theory of matroids, though (which I don't really know anyway). What do you think?

[Yaël Dillies]

@Peter Nelson has.

[Peter Nelson]

https://github.com/e45lee/lean-matroids

Currently under construction after 2 years growing stale. A lot of the basic matroid stuff is in there.

[Michael Stoll]

Looking at your "basic.lean" file, I have the impression that you are carrying around a [fintype E] TC argument in most of what is done. This will be problematic for applications in (linear) algebra, as the relevant carrier sets can be infinite.

[Michael Stoll]

@Peter Nelson Do you have Rado's theorem somewhere?

[Peter Nelson]

Not as such. It would follow pretty easily from the stuff in the intersection/union subfolder, but that's currently very broken. I'll get there soon though.

[Michael Stoll]

My conclusion for now is that I'll implement a version that is good for what I need right now, with no intention to add that one to mathlib. But it would be nice if the result would make it into mahthlib(4) eventually as a part of matroids!

[Kyle Miller]

@Michael Stoll How different is the proof of Rado's theorem from Hall's marriage theorem? I'm wondering if what's in mathlib can be suitably linearized, which might speed up your work. (At least the compactness argument is already there and not specialized too much to Hall's theorem.)

[Michael Stoll]

The proof I have in mind for the linear algebra setting should not be too hard to formalize (but it uses quotients of vector spaces, so maybe does not generalize to arbitrary matroids). (Aside: I came up with the proof before I found out that the result was a special case of Rado's theorem.) Rado's original proof is two pages long and does not look too bad either (but that is easy to say before actually trying to formalize it...).

[Peter Nelson]

Rado is now done! See https://github.com/apnelson1/lean-matroids/blob/master/src/matroid/minmax/inter.lean

[Peter Nelson]

It's done purely matroidally - the project is not really set up for any interactions with linear algebra (yet). Hence it might be a little awkward to apply.

[Michael Stoll]

After struggling for a while with the linear algebra API (as can be seen to some extent here), I decided that the better way would be to build a proof of Rado's Theorem in the general setting of a rank function (on finite subsets of a not-necessarily-finite type) and then derive the result I want as a special case. This is what I have now done; see #18789.

[Michael Stoll]

The proof is, I think, the standard proof, but I did it from scratch. I develop some theory of rank functions, independent families and sections of families of (finite) sets to be able to state ands prove things nicely.

[Michael Stoll]

The PR is labeled "WIP" for now, since I'm not sure what the best way is to proceed relative to the port of mathlib. Most of what is in the PR is new material (and some of it depends on files that are not yet ported as of now), but, as usually happens, I found that I need a bunch of auxiliary lemmas and definitions that should be put into places like data.finset.basic. So proceeding with this as a mathlib(3) PR would create some forward-porting obligations, but right now it is not yet possible to do this in mathlib4.

[Michael Stoll]

Comments and reviews are welcome, of course. @Peter Nelson @Kyle Miller @Yaël Dillies

[Yaël Dillies]

(already on it!)

[Michael Stoll]

The stuff on rank functions and independence will certainly overlap with Matroid stuff (I didn't check yet), but for my purposes it is important that this is developed without a finiteness assumption on the ambient type. My impression regarding @Peter Nelson's Matroid code was that there is always a fintype assumption in place.

[Matthew Ballard]

Are linear_algebra.finite_dimensional and category_theory.cofiltered_systems the only un-ported dependencies?

[Peter Nelson]

Michael Stoll said:

The stuff on rank functions and independence will certainly overlap with Matroid stuff (I didn't check yet), but for my purposes it is important that this is developed without a finiteness assumption on the ambient type. My impression regarding Peter Nelson's Matroid code was that there is always a fintype assumption in place.

That's somewhat true. But in matroid language, the ambient type can, for instance, be a finite set of vectors in some infinite vector space. So one should be able to recover Rado's theorem in all the settings where it makes sense. I'm actually in the process of refactoring my matroid project to allow for infinite matroids of finite rank, which might make the connection be smoother.

[Michael Stoll]

Peter Nelson said:

But in matroid language, the ambient type can, for instance, be a finite set of vectors in some infinite vector space. So one should be able to recover Rado's theorem in all the settings where it makes sense.

But the version I did (which does not require the indexing type to be finite) will be impossible to obtain (directly) in this setting. (Of course, one can apply the compactness agrument afterwards.)

[Michael Stoll]

Matthew Ballard said:

Are linear_algebra.finite_dimensional and category_theory.cofiltered_systems the only un-ported dependencies?

Yes. The first one is only needed to derive the linear algebra version. The second one is needed to go to potentially infinite indexing types. Everything else is basic stuff. (data.finset.card and data.fintype.basic, to be precise; except the additional auxiliary lemmas.)

[Michael Stoll]

@Peter Nelson The point I'm trying to make is that one should develop the theory without the finiteness assumption to the extent possible, and then only impose it where it is really needed.

[Matthew Ballard]

I would surprised if linear_algebra.finite_dimensional is not ported by the end of next week (or even the end of this week). It will be at the top of board soon. category_theory.cofilitered_systems isn't that far from being ported either.

[Peter Nelson]

.

[Peter Nelson]

Michael Stoll said:

Peter Nelson The point I'm trying to make is that one should develop the theory without the finiteness assumption to the extent possible, and then only impose it where it is really needed.

That's right - but for my way of proving Rado's theorem (the matroid intersection theorem), that's not easy - the matroid intersection theorem for general infinite matroids is still open. So going via compactness would be the only way with my method, as you say. And your project already gets there a different way, so there is even less reason to do that from my end :)

The reason my project is mostly just for finite matroids is in line with the literature, 95% of which is on finite matroids. Even basic notions such as linear representation become pathological in the infinite setting, and infinite matroids can't in general be described by rank functions defined only on finite subsets.

[Kevin Buzzard]

@Michael Stoll it has been suggested in the recent past that a reasonable approach right now to new developments which need a few additions to ported files is the following: intentionally put the new lemmas in the wrong place, instead of data.finset.basic, and make a porting note to move them later on after the port.

[Michael Stoll]

... which is what I've done (see combinatorics.rado.auxiliary), minus the porting note.

[Yaël Dillies]

In your case, I think you in fact can dispense of all the preliminary lemmas

[Michael Stoll]

Well, six of them still stand. And some of them are gaps in mathlib, I think.