Zulip Chat Archive

Stream: Is there code for X?

Topic: Closure Operators / Matroids


view this post on Zulip Aaron Anderson (Aug 08 2020 at 00:27):

There are a zillion examples of closure operators across mathlib at the moment, but the only uniting generalization that I can find is that of Galois insertions. Has anybody thought about unifying these into a theory of closure operators, and then proving extra theorems about closure operators that give rise to matroids?

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:28):

https://github.com/adamtopaz/comb_geom

view this post on Zulip Aaron Anderson (Aug 08 2020 at 00:29):

I gotta say though, even coming from the model theory world that still calls them pregeometries, Rota was wrong, matroids won

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:29):

But @Colter MacDonald and I did this when we beginners with lean, so some things can probably be made better

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:33):

I was under the impression that matroids were the independent sets associated to a pregeometey.

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:33):

So they're essentially equivalent in content, but structurally different

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:34):

But I never really used the word matroid, so I'm probably wrong

view this post on Zulip Bryan Gin-ge Chen (Aug 08 2020 at 00:35):

I have a repo with some stuff on (finite) matroids here too, where I prove the equivalence between the independent set, circuit and basis formulations. The fintype2 branch is most up-to-date.

view this post on Zulip Bryan Gin-ge Chen (Aug 08 2020 at 00:35):

I've been thinking of redoing the whole thing from scratch maybe with sets instead.

view this post on Zulip Aaron Anderson (Aug 08 2020 at 00:35):

Depending on who you're reading, a finitary matroid is either a pregeometry or a finite pregeometry

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:37):

What's a matroid then? A set with a closure operator on subsets satisfying blah blah blah?

view this post on Zulip Aaron Anderson (Aug 08 2020 at 00:39):

Yeah, it's a set with one of at least 3 equivalent structures, one of which is the closure operator on subsets satisfying all of the axioms of a pregeometry except for the one that matroid theorists call "finite character", which is that the closure of a set equals the union of the closures of its finite subsets

view this post on Zulip Aaron Anderson (Aug 08 2020 at 00:40):

Obviously that one doesn't matter when you only deal with finite matroids...

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:41):

Ok. So the main reason I'm interested in formalizing this is because I would like to eventually see things like the group chunk theorem formalized, at least in ACF.

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:41):

For now I would settle for the fundamental theorem of projective geometry.

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:42):

This is why I chose to use the closure operator definition.

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:45):

It's all equivalent anyway

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:46):

You need finite character to have a well behaved dimension, right?

view this post on Zulip Aaron Anderson (Aug 08 2020 at 00:46):

My interests are also mainly in pregeometries in model theory rather than the combinatorics of matroids

view this post on Zulip Aaron Anderson (Aug 08 2020 at 00:51):

but I'm also interested in consolidating duplicate code

view this post on Zulip Aaron Anderson (Aug 08 2020 at 00:53):

@Bryan Gin-ge Chen, do you think it's at all feasible to consolidate duplicate code about closures in topology, various kinds of substructures in algebra, and convex hulls, into one piece of code about closure operators?

view this post on Zulip Bryan Gin-ge Chen (Aug 08 2020 at 00:57):

It's an appealing idea and I would say it's worth investigating. I don't think I have enough experience to predict whether it would be feasible or not...

Maybe @Mario Carneiro would be able to point out some potential things to look out for?

view this post on Zulip Adam Topaz (Aug 08 2020 at 00:59):

I think pregeometries are certainly useful for consolidating code around dimension, bases, etc.

view this post on Zulip Adam Topaz (Aug 08 2020 at 01:00):

E.g. why should we separately define the dimension / basis of a vector space, and the transcendence degree, transcendence base of a field extension?

view this post on Zulip Aaron Anderson (Aug 08 2020 at 01:17):

On further examination, it looks like a Galois insertion is pretty much a factorization of a closure operator into two functions...

view this post on Zulip Aaron Anderson (Aug 08 2020 at 01:19):

So these things probably can all be unified pretty well, but sometimes the function called “closure” is the closure operator, and sometimes you have to compose it with coe, and I don’t see us getting around that

view this post on Zulip Bryan Gin-ge Chen (Aug 08 2020 at 01:20):

Can you say a little more about why coe will be needed?

view this post on Zulip Aaron Anderson (Aug 08 2020 at 01:23):

Topological closure is a traditional closure operator, it takes in a set and outputs a set

view this post on Zulip Aaron Anderson (Aug 08 2020 at 01:24):

Meanwhile, subgroup.closure outputs a bundled subgroup

view this post on Zulip Bryan Gin-ge Chen (Aug 08 2020 at 01:24):

Ah, right.

view this post on Zulip Adam Topaz (Aug 08 2020 at 01:38):

Oh I see what youre looking for in a closure operator.

view this post on Zulip Adam Topaz (Aug 08 2020 at 01:41):

I thought Galois insertions exist for precisely this reason

view this post on Zulip Adam Topaz (Aug 08 2020 at 01:45):

(these things don't satisfy exchange)

view this post on Zulip Mario Carneiro (Aug 08 2020 at 04:25):

In metamath we have the notion of a Moore collection, which generalizes all sorts of closure operations

view this post on Zulip Mario Carneiro (Aug 08 2020 at 04:27):

there is a slightly stronger notion of an algebraic closure system which is satisfied by basically all algebra closure operations like the (submonoid, subgroup, subring, submodule) span of a set

view this post on Zulip Mario Carneiro (Aug 08 2020 at 04:27):

you can use it to define what a sub-X is as well, and it's a complete lattice and a bunch of other cool things follow

view this post on Zulip Mario Carneiro (Aug 08 2020 at 04:28):

it's like a topology but without the intersection axiom

view this post on Zulip Aaron Anderson (Aug 08 2020 at 06:45):

I’ve already been working with an idea very like that algebraic closure system. I’ve been more or less copying the subgroup code to work with subStructures a la flypitch

view this post on Zulip Aaron Anderson (Jan 01 2021 at 02:06):

@Bhavik Mehta , do you have plans for any of the above in the nearish future?

view this post on Zulip Bhavik Mehta (Jan 01 2021 at 02:09):

Not really! I'll add that any Galois connection induces a closure operator, and in my closure operator PR I've got that the closed elements have a galois insertion to the underlying set, but I don't know anything about matroids or pregeometries. This tells me that Moore collections are special cases of closure operators (specifically on the powerset preorder), but again I don't plan to add this

view this post on Zulip Bhavik Mehta (Jan 01 2021 at 02:11):

The only real reason I wanted closure operators was to show that universal closure operators on a presheaf category are the same thing as Grothendieck topoi

view this post on Zulip Aaron Anderson (Jan 01 2021 at 02:14):

Ok! I might look into bundling closures of substructures or sets in topological spaces as closure operators.


Last updated: May 07 2021 at 21:10 UTC