## Stream: Is there code for X?

### Topic: Closure Operators / Matroids

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

#### 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

#### 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

#### Adam Topaz (Aug 08 2020 at 00:33):

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

#### Adam Topaz (Aug 08 2020 at 00:33):

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

#### Adam Topaz (Aug 08 2020 at 00:34):

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

#### 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.

#### 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.

#### 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

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

#### 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

#### Aaron Anderson (Aug 08 2020 at 00:40):

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

#### 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.

#### Adam Topaz (Aug 08 2020 at 00:41):

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

#### Adam Topaz (Aug 08 2020 at 00:42):

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

#### Adam Topaz (Aug 08 2020 at 00:45):

It's all equivalent anyway

#### Adam Topaz (Aug 08 2020 at 00:46):

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

#### Aaron Anderson (Aug 08 2020 at 00:46):

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

#### Aaron Anderson (Aug 08 2020 at 00:51):

but I'm also interested in consolidating duplicate code

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

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

#### Adam Topaz (Aug 08 2020 at 00:59):

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

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

#### 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...

#### 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

#### Bryan Gin-ge Chen (Aug 08 2020 at 01:20):

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

#### Aaron Anderson (Aug 08 2020 at 01:23):

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

#### Aaron Anderson (Aug 08 2020 at 01:24):

Meanwhile, subgroup.closure outputs a bundled subgroup

Ah, right.

#### Adam Topaz (Aug 08 2020 at 01:38):

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

#### Adam Topaz (Aug 08 2020 at 01:41):

I thought Galois insertions exist for precisely this reason

#### Adam Topaz (Aug 08 2020 at 01:45):

(these things don't satisfy exchange)

#### 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

#### 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

#### 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

#### Mario Carneiro (Aug 08 2020 at 04:28):

it's like a topology but without the intersection axiom

#### 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

#### Aaron Anderson (Jan 01 2021 at 02:06):

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

#### 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

#### 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

#### 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