## Stream: Is there code for X?

### Topic: comm_semiring structure on constructible subsets

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

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

#### Johan Commelin (Dec 01 2020 at 15:56):

I think Alex did it at LFTCM

#### Adam Topaz (Dec 01 2020 at 15:57):

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

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

#### Adam Topaz (Dec 01 2020 at 15:58):

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

#### Damiano Testa (Dec 01 2020 at 15:58):

Thank you for the pointer! I will take a look at the link!

#### Adam Topaz (Dec 01 2020 at 15:59):

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

#### Adam Topaz (Dec 01 2020 at 15:59):

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

#### Damiano Testa (Dec 01 2020 at 16:00):

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

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

#### Adam Topaz (Dec 01 2020 at 16:01):

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

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

#### Damiano Testa (Dec 01 2020 at 16:05):

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

Sure!

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

#### Adam Topaz (Dec 01 2020 at 16:07):

gist might be better

Here it is!

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

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

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


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

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

#### Damiano Testa (Dec 01 2020 at 16:31):

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

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

#### Damiano Testa (Dec 01 2020 at 16:48):

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

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

#### Damiano Testa (Dec 01 2020 at 17:07):

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

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

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

:pray:

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

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

#### Adam Topaz (Dec 01 2020 at 17:27):

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

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

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

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

#### Adam Topaz (Dec 01 2020 at 17:30):

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?

#### Damiano Testa (Dec 01 2020 at 17:30):

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

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

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

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

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

#### Adam Topaz (Dec 01 2020 at 17:35):

I guess the boolean_algebra to comm_semiring instance is missing?

#### Reid Barton (Dec 01 2020 at 17:35):

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

#### Reid Barton (Dec 01 2020 at 17:36):

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

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

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

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

#### Eric Wieser (Jan 13 2021 at 10:53):

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

#### Damiano Testa (Jan 13 2021 at 10:55):

I just did: thanks for the suggestion!

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


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

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

#### Yakov Pechersky (Jan 14 2021 at 08:14):

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

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

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

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

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

#### Mario Carneiro (Jan 14 2021 at 08:18):

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

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

#### Mario Carneiro (Jan 14 2021 at 08:19):

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

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

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

#### Mario Carneiro (Jan 14 2021 at 08:19):

because these aren't axioms, they are constructors

#### Mario Carneiro (Jan 14 2021 at 08:20):

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

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

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

#### Mario Carneiro (Jan 14 2021 at 08:21):

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

#### Mario Carneiro (Jan 14 2021 at 08:21):

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

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

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

#### Damiano Testa (Jan 14 2021 at 08:24):

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

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

#### Mario Carneiro (Jan 14 2021 at 08:24):

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

#### Damiano Testa (Jan 14 2021 at 08:24):

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

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

#### Damiano Testa (Jan 14 2021 at 08:25):

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

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

#### Kevin Buzzard (Jan 14 2021 at 08:25):

A class is just a structure

#### Kevin Buzzard (Jan 14 2021 at 08:25):

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

#### Mario Carneiro (Jan 14 2021 at 08:25):

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

#### Kevin Buzzard (Jan 14 2021 at 08:26):

So the type class system knows about it

#### Mario Carneiro (Jan 14 2021 at 08:26):

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

#### Kevin Buzzard (Jan 14 2021 at 08:26):

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

#### Kevin Buzzard (Jan 14 2021 at 08:27):

Mathematically a class and a structure are the same

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

#### Kevin Buzzard (Jan 14 2021 at 08:27):

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

#### Kevin Buzzard (Jan 14 2021 at 08:28):

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

#### Kevin Buzzard (Jan 14 2021 at 08:28):

And the simplifier will look for simp tags

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

#### Mario Carneiro (Jan 14 2021 at 08:29):

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

#### Mario Carneiro (Jan 14 2021 at 08:30):

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

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

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

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

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

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

#### Damiano Testa (Jan 14 2021 at 08:53):

Ah, I see! Thanks!

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

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

#### Kevin Buzzard (Jan 14 2021 at 15:32):

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

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

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

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

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

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

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

#### Damiano Testa (Jan 14 2021 at 15:41):

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

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

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

Why "fil"?

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