Closure Operators / Matroids

Stream: Is there code for X?

[Aaron Anderson]

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?

[Adam Topaz]

https://github.com/adamtopaz/comb_geom

[Aaron Anderson]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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

[Aaron Anderson]

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

[Adam Topaz]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Adam Topaz]

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.

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

It's all equivalent anyway

[Adam Topaz]

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

[Aaron Anderson]

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

[Aaron Anderson]

but I'm also interested in consolidating duplicate code

[Aaron Anderson]

@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?

[Bryan Gin-ge Chen]

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?

[Adam Topaz]

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

[Adam Topaz]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Bryan Gin-ge Chen]

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

[Aaron Anderson]

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

[Aaron Anderson]

Meanwhile, subgroup.closure outputs a bundled subgroup

[Bryan Gin-ge Chen]

Ah, right.

[Adam Topaz]

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

[Adam Topaz]

I thought Galois insertions exist for precisely this reason

[Adam Topaz]

(these things don't satisfy exchange)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

it's like a topology but without the intersection axiom

[Aaron Anderson]

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

[Aaron Anderson]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Aaron Anderson]

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