comm_semiring structure on constructible subsets

Stream: Is there code for X?

[Damiano Testa]

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]

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]

I think Alex did it at LFTCM

[Adam Topaz]

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

[Damiano Testa]

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

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

[Damiano Testa]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Damiano Testa]

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!

[Adam Topaz]

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

[Damiano Testa]

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]

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

[Adam Topaz]

Sure!

[Damiano Testa]

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

[Adam Topaz]

gist might be better

[Damiano Testa]

Here it is!

[Alex J. Best]

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]

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]

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

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

[Damiano Testa]

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]

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

[Adam Topaz]

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]

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

[Johan Commelin]

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

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

[Johan Commelin]

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]

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!

[Damiano Testa]

:pray:

[Aaron Anderson]

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]

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

[Adam Topaz]

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

[Johan Commelin]

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]

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]

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

[Adam Topaz]

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?

[Damiano Testa]

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

[Riccardo Brasca]

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]

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]

import order.boolean_algebra
import data.set

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

That works for me @Johan Commelin

[Adam Topaz]

I guess the boolean_algebra to comm_semiring instance is missing?

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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

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]

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

[Eric Wieser]

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

[Damiano Testa]

I just did: thanks for the suggestion!

[Damiano Testa]

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

[Kevin Buzzard]

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]

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]

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

[Damiano Testa]

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]

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]

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]

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

[Mario Carneiro]

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

[Damiano Testa]

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]

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

[Yakov Pechersky]

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]

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

[Mario Carneiro]

because these aren't axioms, they are constructors

[Mario Carneiro]

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

[Mario Carneiro]

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

[Damiano Testa]

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]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Kevin Buzzard]

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]

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

[Damiano Testa]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Mario Carneiro]

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

[Kevin Buzzard]

A class is just a structure

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

So the type class system knows about it

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Mathematically a class and a structure are the same

[Damiano Testa]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

And the simplifier will look for simp tags

[Damiano Testa]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Johan Commelin]

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]

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

[Damiano Testa]

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]

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]

Ah, I see! Thanks!

[Damiano Testa]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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]

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]

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

[Damiano Testa]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

Why "fil"?

[Damiano Testa]

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