Model Theory: Space of n-types formalized

Stream: mathlib4

[Anish Rajeev]

Hi, I'm Anish, an undergraduate math major @ CMU

I recently formalized the Stone Space of n-types (types in Model Theory, not Type Theory) and showed it is a Baire space (by showing it is T2 and compact). My plan is to use this fact to prove the Omitting Types Theorem, (by talking about an omittable set of types as meager). I was wondering if this would be a good fit for mathlib? I've linked the repository below. I'm refactoring the code right now to fit all the mathlib guidelines, but the actual logic is correct.

TLDR : Was wondering if this formalization of the n-type space and proof of Hausdorff + compactness is a good fit for mathlib

https://github.com/anishrajeev/ModelTheoryFun/blob/main/ModelTheoryFun/Stone.lean

[Aaron Liu]

You show in disjoint_open_sets that the space of types is totally separated, I feel like it would be better to show they are T0 (for any pair of types, there is an open set containing one but not the other) and zero-dimensional (there is a basis of clopen sets), this implies totally separated.

[Anish Rajeev]

I can change this, sure. Two questions, though:
1) Any particular reason that way is better than just registering the space as Totally Separated? Just curious for when I write more lean in the future
2) I checked on loogle and didn't spot a zero dimensional class; Is that something you want me to define? I can define it and prove the T0 + zero dimensional -> totally separated, but would prefer to do it after I finish proving the Omitting Types Theorem

[Yongxi Lin (Aaron)]

I think Aaron Liu is referring to this theorem: totallySeparatedSpace_of_t0_of_basis_clopen.

[Aaron Anderson]

This would be great to add (once the code is stylistically ready, and a few things are generalized).

[Aaron Anderson]

I have worked on similar things in the past, but I never quite got to the level of PRing to mathlib - I'd be happy to review any PRs on this subject.

[Anish Rajeev]

Yongxi Lin (Aaron) said:

I think Aaron Liu is referring to this theorem: totallySeparatedSpace_of_t0_of_basis_clopen.

Oh I see, that makes sense. I just updated the codebase to prove T0 and zero dim -> totally separated as suggested.
Aaron Anderson said:

This would be great to add (once the code is stylistically ready, and a few things are generalized).

Good to hear! I'll make a PR after cleaning it up

[Jonas van der Schaaf]

I'm sorry to say this, but I made a pull request (#32215) last week that did this as well :sad:. I do think that your proof is much nicer though, a version of this should probably be merged.

[Anish Rajeev]

Oh no I came to put the link to my PR here and just saw this message! My PR is #32546. Is there some action I should take to merge them together somehow? I think I have the additional property of total separation on the space that I think can be added at least? Sorry, this is my first time adding anything to open source, so I'm a little unfamiliar with the whole process.

[Anish Rajeev]

Also, for future reference so we don't end up stepping on each others toes, what is your future plans with the type space? I ideally wouldn't want both of us to end up working on the same thing independently

[Jonas van der Schaaf]

I don't have any concrete plans at the moment, so feel free to do whatever you want.

I think that your compactness proof is definitely the nicer one and should be merged. Totally separatedness I think can be done much cleaner, you don't need all the T0 stuff, you can just directly provide two separating clopens (some formula is in one type but not in the other), look at totallySeparatedSpace_iff_exists_isClopen for example.

[Jonas van der Schaaf]

I will mark my pull request as WIP in the meantime. There was also some discussion earlier as to what the best way to add this to mathlib is, because at the moment the model theory library isn't allowed to import files from topology

[Ruben Van de Velde]

I think the most helpful thing you both could do is review each other's work on github and try to figure out which parts of each PR are best suited for mathlib

[Ruben Van de Velde]

For the import issue, please adjust Mathlib/Tactic/Linter/DirectoryDependency.lean in your PR so it passes CI and gets on the #queueboard , and leave it to the reviewer to decide what to do about it

[Jonas van der Schaaf]

I think the answer is pretty clearly merge a cleaned up version of Anish' proof

[Jonas van der Schaaf]

For the TotallySeparatedSpace, I think a proof like this is much simpler

[Anish Rajeev]

I think I agree with you on that being much nicer

[Aaron Liu]

I wanted the proof with docs#totallySeparatedSpace_of_t0_of_basis_clopen because having a basis of clopen sets is a stronger property you can separate out into another lemma

[Jonas van der Schaaf]

It's equivalent in this case, and mathlib has an instance which infers it. It's also essentially proven in the file I sent because my typesWith_clopen proves that the basis I constructed only has clopen sets.

[Anish Rajeev]

There was also some discussion earlier as to what the best way to add this to mathlib is

I saw some discussion about this earlier in a thread. I think it deserves to be in the model theory library, but also will defer to the actual mathematicians. I think another way is to formalize and prove these properties of the Stone Space in the topology directory, and then register the type space as an instance of it? Still would have to refer to the topology directory though I think, so not sure if that solves the problem but feels more right maybe

[Jonas van der Schaaf]

Anish Rajeev said:

There was also some discussion earlier as to what the best way to add this to mathlib is

I saw some discussion about this earlier in a thread. I think it deserves to be in the model theory library, but also will defer to the actual mathematicians. I think another way is to formalize and prove these properties of the Stone Space in the topology directory, and then register the type space as an instance of it? Still would have to refer to the topology directory though I think, so not sure if that solves the problem but feels more right maybe

Oh the problem was already solved, the solution is to do as Ruben said earlier.

[Anish Rajeev]

Oh i see

[Jonas van der Schaaf]

I’ve also done some golfing on your proof to get this one. I’m also relatively new here so I don’t know if it’s better, but it’s shorter for sure.

[Jonas van der Schaaf]

Anish Rajeev said:

Oh no I came to put the link to my PR here and just saw this message! My PR is #32546. Is there some action I should take to merge them together somehow? I think I have the additional property of total separation on the space that I think can be added at least? Sorry, this is my first time adding anything to open source, so I'm a little unfamiliar with the whole process.

Here's my proposal: I remove the proof of compactness from my pull request. I do think I will keep the definition of the topological structure in the pull request (if only for the proof that the basis is a basis).

You can then clean up your proof and rebase it on master to merge it. This means that the pull requests are more compartmentalized anyway.

[Anish Rajeev]

That sounds good with me

[Dagur Asgeirsson]

Do I understand correctly that the plan is to remove a bunch of stuff from #32215 and then make #32546 depend on what's left of #32215? Or will they be independent?

[Anish Rajeev]

Hi sorry, got busy there with finals but I'm back now; This is what I understood to be the case yes. #32215 would have the definition of the topological space along the proof that the basis is a basis and that the space is totally separated, while #32546 would depend on #32215 and prove compactness. I'm confused why #32215 is marked as a draft though?

[Dagur Asgeirsson]

Ok, I've marked #32215 as open (no longer draft) and awaiting-author, and #32546 as dependent on #32215

[Jonas van der Schaaf]

I've removed the compactness proof, and added some more small quality of life lemmas. You should be able to slot your proof into this not @Anish Rajeev .

[Jonas van der Schaaf]

Dagur Asgeirsson said:

Ok, I've marked #32215 as open (no longer draft) and awaiting-author, and #32546 as dependent on #32215

I have done the work I stated and I think my pull request could be merged (if you have no remarks yourself).

[Dagur Asgeirsson]

@Anish Rajeev could you review #32215?

[Anish Rajeev]

Ok I just updated #32546 to prove compactness for the space defined in #32215, I think it also should be good for being merged

[Anish Rajeev]

Yes I can review it

[Jonas van der Schaaf]

@Anish Rajeev I’m fairly sure you can replace Fin n by an arbitrary type and still have your code compile. Could you make this change?

[Anish Rajeev]

Good call, just fixed that