Zulip Chat Archive

Stream: new members

Topic: is_open Spec R[x] --> Spec R


Damiano Testa (Aug 28 2020 at 08:30):

Dear All,

I think that I convinced Lean that the morphism Spec R[x] --> Spec R, induced by the natural inclusion C : R --> R[x], is an open map. I am not sure if this is already in mathlib, and I am certain that the version that I have proved will never be acceptable for mathlib! Nevertheless, I am not sure that I can make it into something mathlibbable in any reasonable amount of time! So... what should I do? Is anyone interested in this fact? I am happy to share my code!

Johan Commelin (Aug 28 2020 at 08:51):

Sure, you could paste it into a github gist

Johan Commelin (Aug 28 2020 at 08:52):

You are right that this is not in mathlib

Johan Commelin (Aug 28 2020 at 08:53):

@Damiano Testa I would be very interested in taking a look!

Damiano Testa (Aug 28 2020 at 08:58):

If I understand correctly what gists are, I think that you can find the gist here:

Damiano Testa (Aug 28 2020 at 08:59):

https://gist.github.com/adomani/c08807fb6f5d0e913e156f7e836bd7fa#file-2020-08-24-openmaprx2r-lean

Johan Commelin (Aug 28 2020 at 09:02):

@Damiano Testa Thanks, I'm looking at it right now!

Damiano Testa (Aug 28 2020 at 09:04):

I am of course very happy with any form of comment, especially the negative ones!!

Johan Commelin (Aug 28 2020 at 09:08):

@Damiano Testa Concerning adding this to mathlib... I guess we want to show that a flat morphism of schemes is open, at some point...

Johan Commelin (Aug 28 2020 at 09:08):

So if there is not immediate application of this stuff, I'm not sure if we should add it directly.

Johan Commelin (Aug 28 2020 at 09:08):

But it is of course a very nice display of what someone can do with Lean after a little bit of practice!

Johan Commelin (Aug 28 2020 at 09:10):

Concerning cleaning up:

  1. Some of the lemmas are 1-liners, and can probably be inlined.
  2. The formatting doesn't look like mathlib code. Not sure if you care.
  3. Some of the names are confusing for people with a Lean background. For example, you have a polynomial (iirc) called tt. But tt is always the truth value tt : bool. Of course the code works, but it looks a bit funny to me.

Johan Commelin (Aug 28 2020 at 09:11):

Things like L295 are a nice place to learn about the rintro tactic. It allows you to do the intro + cases + cases in one go.

Damiano Testa (Aug 28 2020 at 09:12):

Johan Commelin said:

So if there is not immediate application of this stuff, I'm not sure if we should add it directly.

Ok, my intended application is as a step towards Chevalley's theorem. I am planning now to prove what happens to closed sets under the map Spec R[x] to Spec R. I agree not to add it to mathlib.

Johan Commelin (Aug 28 2020 at 09:13):

Right, if you manage to prove Chevalley, then we certainly want this in mathlib (-;

Damiano Testa (Aug 28 2020 at 09:14):

Ok, I will clean up my code a bit, following your suggestions and will also try to advance towards Chevalley's theorem

Damiano Testa (Aug 28 2020 at 09:14):

once I know what happens to closed sets under the projection, the rest is packaging everything into an induction

This does not mean that I know how to do it in Lean, though! Ahaha

Johan Commelin (Aug 28 2020 at 09:15):

Ooh, that might be really sweet

Johan Commelin (Aug 28 2020 at 09:15):

Lean is very good at induction (-; You'll probably want to use an inductive type/prop.

Damiano Testa (Aug 28 2020 at 09:15):

Ok, once I have the closed stuff, I will try to learn about inductive types and propositions

Johan Commelin (Aug 28 2020 at 09:16):

If you want to share your screen to get feedback on the cleaning up, I'm sure there will always be someone around who can help you.

Damiano Testa (Aug 28 2020 at 09:16):

screen sharing would be via zulip?

Johan Commelin (Aug 28 2020 at 09:17):

Ooh, any of the 1000 apps that people use these days

Johan Commelin (Aug 28 2020 at 09:17):

I typically use jitsi, but kevin's discord is another option

Damiano Testa (Aug 28 2020 at 09:18):

ok, thanks! sorry for being so slow and needing explanations about anything! I am starting to understand how lean feels...

Damiano Testa (Aug 28 2020 at 09:18):

Johan Commelin said:

I typically use jitsi, but kevin's discord is another option

yes, I have used discord with kevin and kenny

Johan Commelin (Aug 28 2020 at 09:25):

Damiano Testa said:

ok, thanks! sorry for being so slow and needing explanations about anything! I am starting to understand how lean feels...

No worries! We've all been through this phase (-;


Last updated: Dec 20 2023 at 11:08 UTC