Zulip Chat Archive

Stream: Is there code for X?

Topic: comm_semiring structure on constructible subsets


view this post on Zulip Damiano Testa (Dec 01 2020 at 15:53):

Dear All,

I am wondering whether

  1. constructible subsets of a topological space are in Lean (I could not find them);
  2. if they are, is there is a comm_semiring structure on them?

In case you are wondering what I mean by constructible subsets, they are the subsets generated by open sets by iterations of
a) taking unions,
b) taking intersections,
c) taking complements.

view this post on Zulip Adam Topaz (Dec 01 2020 at 15:56):

The constructible topology should be easy to define using an inductive proposition. In fact, I remember seeing the construction at some point, but I can't remember where right now.

view this post on Zulip Johan Commelin (Dec 01 2020 at 15:56):

I think Alex did it at LFTCM

view this post on Zulip Adam Topaz (Dec 01 2020 at 15:57):

https://github.com/leanprover-community/lftcm2020/blob/master/src/exercises_sources/wednesday/topological_spaces.lean

view this post on Zulip Damiano Testa (Dec 01 2020 at 15:57):

@Adam Topaz your answer makes me think that I should have stressed that constructible sets are closed under finitely many of the operations written above. Is the constructible topology this, or does it allow, for instance, infinite intersections of open sets?

view this post on Zulip Adam Topaz (Dec 01 2020 at 15:58):

https://github.com/leanprover-community/lftcm2020/blob/c07fa2bd7968e5d1faf32d59745d14d702e5548c/src/exercises_sources/wednesday/topological_spaces.lean#L117

view this post on Zulip Damiano Testa (Dec 01 2020 at 15:58):

@Johan Commelin and @Adam Topaz
Thank you for the pointer! I will take a look at the link!

view this post on Zulip Adam Topaz (Dec 01 2020 at 15:59):

Take a look at the second one with the precise line...

view this post on Zulip Adam Topaz (Dec 01 2020 at 15:59):

But I don't think the ring structure is there.

view this post on Zulip Damiano Testa (Dec 01 2020 at 16:00):

Adam Topaz said:

Take a look at the second one with the precise line...

Indeed! This is exactly the definition I had in mind, thanks!

view this post on Zulip Adam Topaz (Dec 01 2020 at 16:01):

Ping @Alex J. Best just in case :smile:

view this post on Zulip Damiano Testa (Dec 01 2020 at 16:04):

So, it turns out that I unknowingly did quite a few of those steps and went on to prove the ring structure. However, in quite a clumsy way. Would anyone be interested in seeing what I did and help me get it into better shape?

view this post on Zulip Damiano Testa (Dec 01 2020 at 16:05):

(Not only clumsy, but really getting my hands dirty and not using much of automation...)

view this post on Zulip Adam Topaz (Dec 01 2020 at 16:06):

Sure!

view this post on Zulip Damiano Testa (Dec 01 2020 at 16:07):

Great: should I link a gist? Or do you prefer me to paste it here (I have ~250 lines of code)

view this post on Zulip Adam Topaz (Dec 01 2020 at 16:07):

gist might be better

view this post on Zulip Damiano Testa (Dec 01 2020 at 16:11):

Here it is!

view this post on Zulip Alex J. Best (Dec 01 2020 at 16:11):

I only did it for the exercise session, so all I wrote is what's there (i.e almost nothing). I think Antoine Chambert-Loir also said I should assume locally noetherian or something too to match the literature.

view this post on Zulip Damiano Testa (Dec 01 2020 at 16:12):

I have never really used instances, I tried using them, but could not get them to work...

Also, I had a hard time getting the const X terms to print nicely, and they do not...

view this post on Zulip Adam Topaz (Dec 01 2020 at 16:27):

@Damiano Testa I have a meeting in a few minutes, so I can't take a very close look right now, but here is one quick suggestion.
I think the class const would make more sense in the following form:

class constr {X : Type*} [topological_space X] (C : set X) := (is_constr : is_constructible C)

view this post on Zulip Adam Topaz (Dec 01 2020 at 16:28):

The type of all constructible subsets can then be made using, e.g. docs#category_theory.bundled (or something like that)

view this post on Zulip Damiano Testa (Dec 01 2020 at 16:31):

Ok, I will look into this! I also think that I prefer to replace the by , so I may do a few such cosmetic changes! However, I may also not have a lot of time right now, since it is 5.30pm here, right now

view this post on Zulip Damiano Testa (Dec 01 2020 at 16:31):

In any case, already thank you very much for the suggestions!

view this post on Zulip Adam Topaz (Dec 01 2020 at 16:43):

On second thought, I'm not sure whether constr as above should be a class, only because is_open is not a class.

view this post on Zulip Damiano Testa (Dec 01 2020 at 16:48):

To be honest, class, structure, inductive look all very similar to me...

view this post on Zulip Johan Commelin (Dec 01 2020 at 17:07):

@Damiano Testa We had a session at LFTCM about structures and classes. By now, you might be able to get more out of it.

view this post on Zulip Damiano Testa (Dec 01 2020 at 17:07):

Ah, thanks @Johan Commelin : I will watch it!

view this post on Zulip Johan Commelin (Dec 01 2020 at 17:07):

If you have questions, I'm happy to explain more (if you want, we can do a short video call at some point)

view this post on Zulip Damiano Testa (Dec 01 2020 at 17:08):

Thanks for the offer! I will give it a go on my own, but I may ask some lingering questions, once I am through with the video and tried it a little bit on my own!

view this post on Zulip Damiano Testa (Dec 01 2020 at 17:08):

:pray:

view this post on Zulip Aaron Anderson (Dec 01 2020 at 17:21):

Is the semiring structure you’re talking about essentially the Boolean algebra structure, or else one we could define from any Boolean algebra?

view this post on Zulip Damiano Testa (Dec 01 2020 at 17:25):

It is indeed the Boolean algebra: unions and intersections of sets, happen to map constructible sets to themselves.

view this post on Zulip Adam Topaz (Dec 01 2020 at 17:27):

Does mathlib have the boolean algebra structure on set X for any X?

view this post on Zulip Johan Commelin (Dec 01 2020 at 17:28):

Damiano Testa said:

To be honest, class, structure, inductive look all very similar to me...

There is also the Lean 4 documentation that was written a couple of days ago, which I found concise, clear, well-written, to the point.
https://github.com/leanprover/lean4/blob/master/doc/typeclass.md

Of course the syntax differs a little bit from Lean 3, but I don't think that will be a big problem.

view this post on Zulip Damiano Testa (Dec 01 2020 at 17:29):

Great: I will take a look! I actually prefer to have something to read through, before watching a video and trying it out on my example!

view this post on Zulip Johan Commelin (Dec 01 2020 at 17:30):

rg "comm_ring \(set" doesn't give me any hits, so I think it's not there

view this post on Zulip Adam Topaz (Dec 01 2020 at 17:30):

Adam Topaz said:

Does mathlib have the boolean algebra structure on set X for any X?

I guess it does. So maybe we should define constructible sets as the boolean subalgebra of set X generated by opens?

view this post on Zulip Damiano Testa (Dec 01 2020 at 17:30):

Adam Topaz said:

Does mathlib have the boolean algebra structure on set X for any X?

This reminds me the Friday challenge with 37={37}...

view this post on Zulip Riccardo Brasca (Dec 01 2020 at 17:30):

I am in the process of learning this stuff too, watching the videos. I spent something like 15 minutes trying to figure out what was the difference between the structure is_even_cube_above_100 and the proposition with the two ... and of course he explains this 3 minutes later, so be sure to watch the whole video before starting to think that you do not understand something!

view this post on Zulip Damiano Testa (Dec 01 2020 at 17:31):

Johan Commelin said:

rg "comm_ring \(set" doesn't give me any hits, so I think it's not there

I may be wrong, but comm_ring might assume the existence of opposites for add, so would not work with the Boolean algebra, I think

view this post on Zulip Adam Topaz (Dec 01 2020 at 17:32):

import order.boolean_algebra
import data.set

example (α : Type*) : boolean_algebra (set α) := by apply_instance

That works for me @Johan Commelin

view this post on Zulip Adam Topaz (Dec 01 2020 at 17:35):

I guess the boolean_algebra to comm_semiring instance is missing?

view this post on Zulip Reid Barton (Dec 01 2020 at 17:35):

AFAIK mathlib doesn't have a definition of Boolean subalgebra, though

view this post on Zulip Reid Barton (Dec 01 2020 at 17:36):

https://github.com/rwbarton/lean-omin/blob/master/src/for_mathlib/boolean_subalgebra.lean

view this post on Zulip Kevin Buzzard (Dec 01 2020 at 17:37):

@Damiano Testa if you want to learn about structures, then I cannot recommend highly enough making a PR for boolean subalgebras. Several Imperial students have got a lot out of bundling various subobjects (submonoids, subgroups and subrings were all bundled by Imperial beginners-at-the-time).

view this post on Zulip Damiano Testa (Dec 01 2020 at 17:39):

I will give it a try, although in this case, it seems that Reid already has done quite a bit of work on this!

view this post on Zulip Damiano Testa (Jan 13 2021 at 10:51):

Dear All,

I found some time to work on this and my progress so far is in the gist below. If anyone would like to chime in to give suggestions and improvements on how to work with the file below, I would be _really_ grateful!

My final goal is to define a boolean_algebra/comm_semiring structure generated by the open subsets of a topological space. In particular, I am not so interested in having the singletons of X to be part of the boolean algebra. Eventually, this would help with constructible subsets of a topological space.

Thanks!


Gist:
https://gist.github.com/adomani/a1228c1f9726a999c8460ebf445d8871

view this post on Zulip Eric Wieser (Jan 13 2021 at 10:53):

Could you rename the gist to have a .lean extension so that it syntax-highlights?

view this post on Zulip Damiano Testa (Jan 13 2021 at 10:55):

I just did: thanks for the suggestion!

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:04):

I am trying to make the arguments clearer and the linter wanted a inhabited instance. I provided one, but I do not understand why it works: can someone give me a pointer as to why the code below compiles and pleases the linter?

Thanks!

import data.set.lattice

variables {X : Type*} {fil : set X  Prop}

inductive uc_closure (fil : set X  Prop) : set X  Prop
| uc_empty : uc_closure 
| uc_fil   :  {f}, fil f  uc_closure f
| uc_union :  {C D}, uc_closure C  uc_closure D  uc_closure (C  D)
| uc_compl :  {C}, uc_closure C  uc_closure C

/--- `uc_type` is the SubType of `set X` consisting of the subsets
spelled out by `uc_closure fil`. -/
def uc_type (fil : set X  Prop) := {s : set X // uc_closure fil s}

--  I thought that, for all `R`and all choices of `fil : set X → Prop`,  I would have had to given an example of `uc_type fil`
-- but it seems that I did not.  Moreover, Lean is happy only with checking the axiom uc.empty?
instance uc_type.inhabited : inhabited (uc_type fil) :=
⟨⟨_, uc_closure.uc_empty⟩⟩

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:13):

The inhabited linter just wants to see an explicit example of a term of your type. If you've made a family of types it just wants to see a term of one of them. Is that your question?

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 08:13):

Your inhabited instance ignored the provided fil, so it says, no matter what fil I get, there's always the closure over the empty set.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 08:14):

Especially because uc_closure.uc_empty doesn't actually use a fil argument.

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:15):

Ah, I see! It is the first time that I work with inhabited, so my doubt was really basic. So, inhabited just wants to know that there is one value of all the parameters of the construction that produces a non-empty type, correct? What I have provided is the example on the empty type, if I understood correctly.

Thanks!

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:17):

Kevin and Yakov, I think that indeed what confused me was that I had to specify fil to the instance, but then I proved something that did not work with an arbitrary fil. Now it is clearer!

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:17):

Yes it's really easy to please. You could probably even make it happy by telling it an explicit fil on nat and writing down an explicit term of uc_type for that fil

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:17):

You actually want to prove that the type is inhabited for all settings of the parameters, in this case fil

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:18):

in your case this is easy because you have a constructor that says as much

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:18):

Mario, I thought that this was the case, but I think that the proof only uses an "empty" fil. I think that I am still missing something...

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:19):

No, the proof shows that the empty set is in the closure of any fil

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 08:19):

Damiano Testa said:

one value of all the parameters of the construction that produces a non-empty type

Rather, no matter the value of the parameters, one can always produce a term of the type.

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:19):

Ah, but what if the remaining axioms were contradictory? Why did I not have to check that, then?

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:19):

because these aren't axioms, they are constructors

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:20):

it's an inductive type, so any constructor will do

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:20):

if it was a structure then you would have to set all the fields to be something coherent, which might be harder

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:21):

Ok, so, regardless of what X and fil are, the empty set is always a term of the resulting type. Now this makes much more sense! Thanks and sorry for the silly questions!

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:21):

for example proving that group A is inhabited is not at all trivial

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:21):

(actually it's only true if A is inhabited)

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:22):

This seems to be clearing up a more fundamental confusion of mine on the distinction between inductive types and structures/classes.

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:22):

a structure is sugar for an inductive type with one constructor and a bunch of arguments to that constructor

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:24):

So this means that it is possible to eliminate all structures, if you have inductive types?

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:24):

My experience with the inhabited linter is that it's happy even if you construct a term of a specialisation of your type family. Is this not the case?

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:24):

Not just that, they are actually inductive types under the hood

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:24):

(not that I would want to, but structure is just one special kind of inductive type?)

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:25):

There is a rec_on and no_confusion and all the other things you find on inductive types

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:25):

Ok, whereas a class is something like defining a mathematical object by generators and relations?

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:25):

and I think if you ask lean if it's an inductive type it will say yes

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:25):

A class is just a structure

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:25):

The only extra thing is that it's tagged with an attribute

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:25):

A class is a structure with an annotation on it, class = @[class] structure

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:26):

So the type class system knows about it

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:26):

the other part of that being instance = @[instance] def

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:26):

It's like a simp lemna is just a lemma tagged with the simp attribute

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:27):

Mathematically a class and a structure are the same

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:27):

Ok, I probably have to go back and read again classes/structures/inductive types and re-read Kevin's post on no-confusion!

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:27):

Attributes just change the way some tactics or internals use the definition

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:28):

Eg the type class inference square bracket machine will look for class tags

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:28):

And the simplifier will look for simp tags

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:29):

Ah, so the things that are in square brackets are structures labelled with a class tag, right?

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:29):

yes, [group A] only does something because group is marked as @[class]

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:30):

if you did [even n] it wouldn't work

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:31):

Thanks, this is now entering my mind: I believe that it bounced on it several times in the past...

view this post on Zulip Johan Commelin (Jan 14 2021 at 08:36):

the inhabited-linter is there to force us to do some basic checks that we are not making stupid definitions. So when you write an instance to make it happy, it's best to try to make the example as "canonical" as possible. In other words, even if you can give an example for just X = nat, we encourage you to make it for every X, just like you did.

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:38):

... in line with the aspiration that everything is mathlib should be as general as possible, including the specific examples!

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:44):

So, while we are talking about this, does this mean that maybe I should make uc_closure a structure? Or even a class?

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:51):

A structure is nothing more than an inductive type with one constructor. There's no such thing as a structure in some sense, it's just a certain kind of inductive type with some syntax sugar. Your inductive type has four constructors.

view this post on Zulip Damiano Testa (Jan 14 2021 at 08:53):

Ah, I see! Thanks!

view this post on Zulip Damiano Testa (Jan 14 2021 at 15:24):

Dear All,

to get some familiarity with these notions, I showed how you can construct a boolean subalgebra of a boolean algebra. The gist is linked below. If you have any comments, they are more than welcome, as usual!

I will create a PR with this later on, if people think that it might be useful.

Thanks!

https://gist.github.com/adomani/2c60da5448abb9ef27769162eb3038a0

view this post on Zulip Eric Wieser (Jan 14 2021 at 15:29):

It surprises me how different the approach you use there is to how things like docs#subalgebra are defined, in that you build an inductive predicate instead of stating properties of a set

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 15:32):

Yes I agree. Did you look at how it's done for subgroups of groups?

view this post on Zulip Eric Wieser (Jan 14 2021 at 15:33):

structure boolean_subalgebra (B : Type*) [boolean_algebra B] :=
(carrier : set B)
(bot_mem : ( : B)  carrier)
(sup_mem :  a b : B, a  carrier  b  carrier  a  b  carrier)
(compl_mem :  a : B, a  carrier  a  carrier)

would normally be the start

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 15:36):

You want to make the type of subalgebras, and construct the Galois insertion from subsets to subalgebras. This gives you a complete lattice structure on subalgebras. I would strongly recommend looking at how it is done for submonoids, subgroups, subrings etc.

view this post on Zulip Damiano Testa (Jan 14 2021 at 15:38):

I have not looked at anything, other than the manual for seeing the syntax of inductive types... I will take a look at subgroups/sub-other things!

view this post on Zulip Eric Wieser (Jan 14 2021 at 15:40):

I think your is_bool_subalgebra fil x would usually be spelt x \in boolean_subalgebra.closure fil

view this post on Zulip Damiano Testa (Jan 14 2021 at 15:40):

As a general rule, I have embraced the "talking about types instead of sets" idea, which is why I did not think of using an "underlying set". However, as I do not have any experience of how these definitions play out in the long run, I do not insist on maintaining it like this!

I was pleased to see that, when I start with the open subsets of a topological space, I do get the usual constructible sets!

view this post on Zulip Eric Wieser (Jan 14 2021 at 15:41):

Well, B → Prop is the same as set B, so your is_bool_subalgebra fil is simply a computation of that underlying set!

view this post on Zulip Damiano Testa (Jan 14 2021 at 15:41):

Sure, but I do not need to talk about elements...

view this post on Zulip Eric Wieser (Jan 14 2021 at 15:42):

Arguably is_bool_subalgebra fil a is talking about elements because it's defeq to a ∈ is_bool_subalgebra fil

view this post on Zulip Eric Wieser (Jan 14 2021 at 15:45):

"Types instead of sets" is more about using (b : B) instead of (a : A) (ha : a ∈ b) - using (a : A) (ha : p a) isn't morally any different to the set spelling (although both are fine when its convenient!)

view this post on Zulip Reid Barton (Jan 14 2021 at 17:56):

Why "fil"?

view this post on Zulip Damiano Testa (Jan 14 2021 at 20:48):

Because I was thinking of using the elements of a filter at some point... Not a very good reason!


Last updated: May 17 2021 at 15:13 UTC