Zulip Chat Archive

Stream: new members

Topic: Hello


Harry Gindi (Nov 10 2018 at 18:35):

Hiya, some of you probably know me from mathoverflow. I was curious how things are going in here.

Johan Commelin (Nov 10 2018 at 18:35):

Hey, welcome! Good to see you.

Johan Commelin (Nov 10 2018 at 18:35):

Things are going pretty good here (-;

Harry Gindi (Nov 10 2018 at 18:36):

I'm a complete noob on the whole theorem proving thing, but I feel like it's something worth learning

Johan Commelin (Nov 10 2018 at 18:36):

One of our biggest problems is lack of (wo)man-power

Harry Gindi (Nov 10 2018 at 18:36):

I'd like to eventually work on the library for simplicial sets, but I'm completely worthless at programming

Johan Commelin (Nov 10 2018 at 18:37):

Right. The first thing you need to learn is that you should ask lots of questions here :lol:

Johan Commelin (Nov 10 2018 at 18:37):

You don't need that much programming experience. Coincidentally, I did some stuff on simplicial sets a couple of months ago.

Johan Commelin (Nov 10 2018 at 18:38):

In the mean time, Scott wrote a very very nice category library.

Harry Gindi (Nov 10 2018 at 18:38):

Does it have Grothendieck constructions

Johan Commelin (Nov 10 2018 at 18:38):

I've been meaning to update my stuff, but haven't done so yet.

Johan Commelin (Nov 10 2018 at 18:38):

It only has the basics so far. We are in the process of adding limits and colimits.

Harry Gindi (Nov 10 2018 at 18:38):

If it does, maybe it's already time to introduce the Theta construction that I use in my research

Harry Gindi (Nov 10 2018 at 18:38):

Ah, ok!

Johan Commelin (Nov 10 2018 at 18:39):

For example: we don't have abelian categories yet.

Harry Gindi (Nov 10 2018 at 18:39):

If there's a simplicial library and a category theory library, you might be able to use simplicial objects in Cat to get monoidal categories

Johan Commelin (Nov 10 2018 at 18:39):

No fundamental obstructions. Just that there are only 3 people working on this in their spare time.

Harry Gindi (Nov 10 2018 at 18:39):

via Segal's observation

Harry Gindi (Nov 10 2018 at 18:39):

Also, are Abelian categories really that fundamental for theorem proving?

Johan Commelin (Nov 10 2018 at 18:40):

Practice seems to show that theorem provers need a delicate balance between hands-on constructions and big theoretical hammers.

Johan Commelin (Nov 10 2018 at 18:40):

Not for theorem proving, but they are for applying theorem provers to (some, eg my) mathematical research.

Harry Gindi (Nov 10 2018 at 18:41):

mhm, do you know where I can get bootstrapped with experience to start contributing?

Johan Commelin (Nov 10 2018 at 18:41):

First you need to install a Lean environment.

Johan Commelin (Nov 10 2018 at 18:41):

What editor do you use to type LaTeX and the likes?

Harry Gindi (Nov 10 2018 at 18:41):

vscode

Johan Commelin (Nov 10 2018 at 18:41):

Great!

Johan Commelin (Nov 10 2018 at 18:41):

There is a Lean extension for VScode

Harry Gindi (Nov 10 2018 at 18:42):

Is the Windows lean environment crippled?

Johan Commelin (Nov 10 2018 at 18:42):

Install it, and open an empty Lean file. It will then ask if you want it to install Lean for you.

Harry Gindi (Nov 10 2018 at 18:42):

oh, that's neat!

Johan Commelin (Nov 10 2018 at 18:42):

I think it was fixed. I am not sure. I haven't touched Windows in 10 years.

Andrew Ashworth (Nov 10 2018 at 18:42):

If you like textbooks I would recommend Theorem Proving in Lean

Johan Commelin (Nov 10 2018 at 18:42):

Maybe it is about to be fixed.

Harry Gindi (Nov 10 2018 at 18:43):

If it's not working, I have the Win10 Linux emulator installed

Harry Gindi (Nov 10 2018 at 18:43):

that's why I'm asking

Andrew Ashworth (Nov 10 2018 at 18:43):

Lean on Windows works great

Kenny Lau (Nov 10 2018 at 18:44):

@Harry Gindi here is my (controversal) instructions on how to get Lean on windows

Andrew Ashworth (Nov 10 2018 at 18:44):

There are some issues with setting $PATH correctly. However, if you are the kind of person to have WSL installed, I'm sure you'll be able to fix it

Harry Gindi (Nov 10 2018 at 18:45):

Thanks!

Kenny Lau (Nov 10 2018 at 18:45):

oh wait, you said you're working in Linux, never mind then

Harry Gindi (Nov 10 2018 at 18:45):

Both work, Kenny. WSL is slow though

Harry Gindi (Nov 10 2018 at 18:46):

Disk I/O is extremely bad

Harry Gindi (Nov 10 2018 at 18:46):

then again, so is mingw64 =D

Kenny Lau (Nov 10 2018 at 18:46):

what do you mean?

Harry Gindi (Nov 10 2018 at 18:47):

iirc disk i/o on cygwin and msys is benchmarked just as slow as WSL

Harry Gindi (Nov 10 2018 at 18:47):

it's the main reason why things are so slow.

Harry Gindi (Nov 10 2018 at 18:48):

I was really active on the WSL github for like two years, and performance is on-par with linux now except for disk i/o

Johan Commelin (Nov 10 2018 at 18:49):

@Harry Gindi Once you have Lean installed, you will want to fork https://github.com/leanprover-community/mathlib/
Then you need to run leanpkg build in that directory. After that, get yourself some tea. Your computer will be warming your room for about an hour.

Harry Gindi (Nov 10 2018 at 18:49):

but I also used msys2 before, and it was even slower

Kenny Lau (Nov 10 2018 at 18:49):

then what's the best one?

Harry Gindi (Nov 10 2018 at 18:49):

Kenny Lau, meh, nothing's great. The best thing you could do probably is run a VM

Harry Gindi (Nov 10 2018 at 18:49):

if you're concerned about performance

Harry Gindi (Nov 10 2018 at 18:49):

Thanks Johan!

Andrew Ashworth (Nov 10 2018 at 18:50):

I compile Lean with MSYS2, disk i/o is far from the limiting factor when it comes to performance

Kenny Lau (Nov 10 2018 at 18:50):

and you need to rewarm your room for an hour every time you update mathlib, isn't Lean wonderful!

Harry Gindi (Nov 10 2018 at 18:51):

Andrew Ashworth, then maybe performance on WSL is better than msys2 on everything but disk I/O

Kenny Lau (Nov 10 2018 at 18:51):

@Harry Gindi ping

Harry Gindi (Nov 10 2018 at 18:51):

hello!

Kenny Lau (Nov 10 2018 at 18:51):

Harry Gindi, not ping

Harry Gindi (Nov 10 2018 at 18:51):

I'm aware, I'm just using the web UI

Andrew Ashworth (Nov 10 2018 at 18:51):

is it now? I can't imagine there being a huge difference

Harry Gindi (Nov 10 2018 at 18:52):

Andrew, they did benchmarks on phoronix, and on cpu-only tasks, WSL performs at 95-100% of native

Harry Gindi (Nov 10 2018 at 18:52):

once it hits disk i/o, it crashes to like 20%

Harry Gindi (Nov 10 2018 at 18:53):

it has to do with the fact that NTFS doesn't use inodes and therefore can't cache them effectively

Harry Gindi (Nov 10 2018 at 18:54):

also, windows defender, and a bunch of other things just kill it on disk i/o

Harry Gindi (Nov 10 2018 at 18:54):

anyway, going to get this lean system installed

Harry Gindi (Nov 10 2018 at 18:54):

does arch have a lean-git AUR package?

Harry Gindi (Nov 10 2018 at 18:55):

Looks like it does

Andrew Ashworth (Nov 10 2018 at 18:55):

ah, I was aware of that. I think you can compile Lean with visual studio and get a totally native binary, if i recall correctly

Andrew Ashworth (Nov 10 2018 at 18:55):

i've never investigated it though, so ymmv

Harry Gindi (Nov 10 2018 at 18:55):

blech, I have an arch installation on this pc

Andrew Ashworth (Nov 10 2018 at 18:56):

disk access is not an issue at 20% or 100% anyway

Harry Gindi (Nov 10 2018 at 18:56):

but every time I decide to jump into linux, I get sidetracked

Harry Gindi (Nov 10 2018 at 18:56):

I end up staying up all night messing around with it, it's unhealthy for me

Johan Commelin (Nov 10 2018 at 18:56):

Don't use that arch thing.

Harry Gindi (Nov 10 2018 at 18:56):

oh, it's bad?

Harry Gindi (Nov 10 2018 at 18:57):

or are you saying don't use arch in general :D

Johan Commelin (Nov 10 2018 at 18:57):

The VScode Lean extension is better. It sets up a useful wrapper called elan.

Johan Commelin (Nov 10 2018 at 18:57):

No, I run arch as OS :lol: So that's fine.

Harry Gindi (Nov 10 2018 at 18:57):

the arch thing is just a lean system, I thought

Harry Gindi (Nov 10 2018 at 18:58):

anyway gonna work on this tomorrow morning

Harry Gindi (Nov 10 2018 at 18:58):

cheers all

Kevin Buzzard (Nov 10 2018 at 20:00):

@Kenny Lau I think https://github.com/leanprover/mathlib/blob/master/docs/elan.md is a better place to direct computer-savvy Windows users to than your link

Kenny Lau (Nov 10 2018 at 20:08):

fair

Scott Morrison (Nov 10 2018 at 21:30):

Yes --- please, please, everyone should now be using elan, no messing around with $PATH, no installing complicated things like msys2 or WSL, just go with the bare minimum provided by "git bash" and its installer, then work entirely inside VS Code.

Kevin Buzzard (Nov 10 2018 at 21:30):

@Harry Gindi ^^ that

Scott Morrison (Nov 10 2018 at 21:33):

Also, welcome @Harry Gindi. :-)

Harry Gindi (Nov 10 2018 at 21:33):

Got it, thanks!

Harry Gindi (Nov 10 2018 at 21:34):

Also hello, Kevin and Scott, it's been a while since I saw you on MO

Kevin Buzzard (Nov 10 2018 at 21:34):

Here is a roadmap to getting started. First read through all of Theorem Proving In Lean and do all the exercises. Then choose a project to work on, and work on it.

Kevin Buzzard (Nov 10 2018 at 21:34):

The projects I chose were: (1) do all the exercises in the undergraduate class I was teaching at the time and then (2) define schemes and prove that an affine scheme is a scheme.

Kevin Buzzard (Nov 10 2018 at 21:35):

Do not underestimate how difficult all of this is at this point.

Harry Gindi (Nov 10 2018 at 21:35):

It seems like it'll be really annoying, don't worry =)

Harry Gindi (Nov 10 2018 at 21:36):

I think maybe a good project to work on would be weak factorization systems once I learn stuff

Kevin Buzzard (Nov 10 2018 at 21:36):

Working with isomorphisms is difficult. Working with categories is even more difficult, for several reasons -- some associated with dependent type theory (it is difficult to transport structure along isomorphisms at this point, although things will change one day), some associated with universe issues (mathematicians being sloppy about universes, basically) and other things too

Kevin Buzzard (Nov 10 2018 at 21:37):

But there is no better recommendation than "start on something and whenever you get stuck, ask here"

Kevin Buzzard (Nov 10 2018 at 21:37):

The first thing you will probably have to ask is a question of the form "here's a link to a pdf, I want to make definition 2.3 of that paper in Lean, where do I even start?". There will be an answer.

Harry Gindi (Nov 10 2018 at 21:38):

WFS would be useful if anyone wants to go full bore and do model categories, and it can be done with monads for algebraic weak factorization systems

Harry Gindi (Nov 10 2018 at 21:38):

I'm guessing that monads work well?

Kevin Buzzard (Nov 10 2018 at 21:38):

Listen, honestly, categories are really like jumping in at the deep end

Harry Gindi (Nov 10 2018 at 21:38):

ah

Kevin Buzzard (Nov 10 2018 at 21:38):

groups work well

Kevin Buzzard (Nov 10 2018 at 21:38):

but it is not impossible, and you have to jump in somewhere

Harry Gindi (Nov 10 2018 at 21:39):

I mean, my research is in category theory

Harry Gindi (Nov 10 2018 at 21:39):

but I'll see how hard it is

Kevin Buzzard (Nov 10 2018 at 21:39):

well, when I arrived here a year ago people were already talking about formalising categories, and one year later they still haven't managed to do adjoint functors.

Kevin Buzzard (Nov 10 2018 at 21:40):

This is basically for two reasons: (1) universes make this harder than you think and (2) lack of manpower or personpower or whatever it should be called nowadays

Harry Gindi (Nov 10 2018 at 21:40):

I would have assumed that monads might be easier than adjunctions, but maybe this is a mistake

Kevin Buzzard (Nov 10 2018 at 21:40):

I'm also exaggerating a little. But dependent type theory is perhaps not set up with category theory in mind

Kevin Buzzard (Nov 10 2018 at 21:41):

On the other hand, "difficult" is certainly not the same as "impossible"

Harry Gindi (Nov 10 2018 at 21:41):

Do presheaves of sets make sense?

Kevin Buzzard (Nov 10 2018 at 21:41):

and there is no actual obstruction to doing adjoints and a whole bunch more. It's just that people really like (a) working in the maximal generality and (b) writing automation as they go

Kevin Buzzard (Nov 10 2018 at 21:41):

they call them presheaves of types here

Kevin Buzzard (Nov 10 2018 at 21:42):

but I defined these in a hands-on way when doing schemes, no problem

Harry Gindi (Nov 10 2018 at 21:42):

Neat, I'll have to look at what you've done already before I try to jump in

Kevin Buzzard (Nov 10 2018 at 21:42):

I did not use the category theory machinery though, I just wrote down the axioms for a functor in that specific case rather than relying on a general theory (which at that time was not there anyway)

Kevin Buzzard (Nov 10 2018 at 21:42):

My code sucks though

Kevin Buzzard (Nov 10 2018 at 21:43):

because it was the code I wrote to learn how to do mathematics in dependent type theory

Kevin Buzzard (Nov 10 2018 at 21:43):

I am currently refactoring all of it with an MSc student

Harry Gindi (Nov 10 2018 at 21:43):

so when you defined schemes, did you follow e.g. Toën?

Harry Gindi (Nov 10 2018 at 21:44):

working with functors of points the whole way?

Harry Gindi (Nov 10 2018 at 21:44):

or is that exactly the kind of non-kosher thing that implicitly uses universes

Kevin Buzzard (Nov 10 2018 at 21:44):

I followed the stacks project

Kevin Buzzard (Nov 10 2018 at 21:44):

https://github.com/kbuzzard/lean-stacks-project/blob/master/src/tag009I.lean

Kevin Buzzard (Nov 10 2018 at 21:44):

there's presheaves of types on a basis of open sets of a top space

Kevin Buzzard (Nov 10 2018 at 21:44):

But nowadays we would not write it like that

Kevin Buzzard (Nov 10 2018 at 21:45):

we'd use the category theory machinery, which seems to be just about ready to do that sort of thing.

Kevin Buzzard (Nov 10 2018 at 21:45):

As of about last week

Harry Gindi (Nov 10 2018 at 21:45):

neat!

Harry Gindi (Nov 10 2018 at 21:45):

I heard that some simplicial set machinery was developed up-thread

Harry Gindi (Nov 10 2018 at 21:46):

was this done entirely without model structures using e.g. Ex^∞?

Kevin Buzzard (Nov 10 2018 at 21:47):

In that code I linked to, I am literally saying that a presheaf of types is a function F which takes a basis element to a type, plus a restriction F(U)->F(V), plus the axioms that res from U to U is id and res of res is res. So I am avoiding explicit usage of any category theory formalism.

Kevin Buzzard (Nov 10 2018 at 21:47):

You'll have to ask @Johan Commelin where he put his simplicial set stuff. That was also written before categories were available, I believe.

Harry Gindi (Nov 10 2018 at 21:47):

mhm

Harry Gindi (Nov 10 2018 at 21:47):

alright let's not but the cart before the horse, I've gotta do the exercises and stuff

Harry Gindi (Nov 10 2018 at 21:48):

cheers, this seems exciting

Kevin Buzzard (Nov 10 2018 at 21:48):

it's the future

Kevin Buzzard (Nov 10 2018 at 21:48):

but I might have died before it becomes really important

Kevin Buzzard (Nov 10 2018 at 21:48):

I have no idea of the time frame before it becomes (a) useful (b) powerful (c) better than us

Harry Gindi (Nov 10 2018 at 21:48):

ascended to robothood

Kevin Buzzard (Nov 10 2018 at 21:48):

but currently we are still a long way from (a)

Kevin Buzzard (Nov 10 2018 at 21:49):

"proof assistants" currently do nothing but make mathematician's lives harder, for the most part.

Harry Gindi (Nov 10 2018 at 21:49):

like any assistant they must be trained =p

Harry Gindi (Nov 10 2018 at 21:49):

otherwise all they do is spill coffee on you

Kevin Buzzard (Nov 10 2018 at 21:50):

right. And my view (and I do say this firmly with my tongue in my cheek and slightly provocatively, but there is a grain of truth in it) is that currently the main problem is that for the most part they are being trained to do mathematics by computer scientists, which is in my opinion not driving development in the right directions.

Harry Gindi (Nov 10 2018 at 21:51):

I'm going to try to get my friend in the US involved on this

Kevin Buzzard (Nov 10 2018 at 21:51):

There are a few mathematicians here who are trying to change all this, mostly by saying things such as "mathematicians will not be able to use your software unless you make stuff like (x+y)^3=x^3+3x^2y+3xy^2+y^3 easy to do"

Harry Gindi (Nov 10 2018 at 21:51):

he did a math undergrad and he's doing a CS Ph.D., but he hates CS

Harry Gindi (Nov 10 2018 at 21:52):

this might be a nice change of pace for him

Kevin Buzzard (Nov 10 2018 at 21:52):

https://xenaproject.wordpress.com/2018/06/13/ab3/

Harry Gindi (Nov 10 2018 at 21:52):

is anyone doing analysis-related stuff?

Kevin Buzzard (Nov 10 2018 at 21:52):

Yes, but it's happening very slowly

Harry Gindi (Nov 10 2018 at 21:52):

because he always liked analysis

Harry Gindi (Nov 10 2018 at 21:52):

alright, I'll try to cajole him into helping =)

Kevin Buzzard (Nov 10 2018 at 21:53):

and in my opinion there is a problem with the development plan we have

Kevin Buzzard (Nov 10 2018 at 21:53):

In fact Harry to be honest basic freshman one variable analysis would be a perfect project to learn Lean with

Kevin Buzzard (Nov 10 2018 at 21:53):

because the maths is basically very well known and well understood, and putting it into a theorem prover would be a formidable challenge for a beginner, however there would be plenty of people around to help

Kevin Buzzard (Nov 10 2018 at 21:54):

The problem is that the general position here is "do everything in the correct generality" which means "the maximal generality"

Harry Gindi (Nov 10 2018 at 21:54):

break out a copy of Bourbaki's 'analysis in one real variable' haha

Kevin Buzzard (Nov 10 2018 at 21:55):

so instead of developing a basic theory of analysis of functions of one real variable, everyone wants to do stuff on normed spaces and Banach spaces etc etc and then prove all the single-variable theorems in one fell swoop by specialising to this case

Harry Gindi (Nov 10 2018 at 21:55):

Is that even possible?

Kevin Buzzard (Nov 10 2018 at 21:55):

In my mind a good analogy here is what happened with polynomials

Kevin Buzzard (Nov 10 2018 at 21:55):

A computer scientist developed a fabulous library of polynomials in an arbitrary number of variables (in fact for an arbitrary set of variables)

Kevin Buzzard (Nov 10 2018 at 21:56):

but when mathematicians wanted to actually use it to prove basic stuff like quadratic reciprocity or finite fields or whatever

Harry Gindi (Nov 10 2018 at 21:56):

For example, defining C^\infty functions requires you do have partial derivatives, which come from the 1-dimensional case, if I remember correctly (I haven't done analysis in around 8 years =\)

Kevin Buzzard (Nov 10 2018 at 21:56):

they found they really just wanted a much deeper theory of polynomials in one variable

Kevin Buzzard (Nov 10 2018 at 21:57):

so at the end of the day an undergraduate here at Imperial, Chris Hughes, just wrote the theory of polynomials in one variable anyway.

Kevin Buzzard (Nov 10 2018 at 21:57):

And I kind of suspect that the same might happen for differentiable functions.

Kevin Buzzard (Nov 10 2018 at 21:57):

Eventually we'll have them on Banach manifolds or something

Harry Gindi (Nov 10 2018 at 21:57):

oh, you're saying that you agree that the 1-variable case is separate and important

Kevin Buzzard (Nov 10 2018 at 21:57):

but then when someone wants to prove that the derivative of sin is cos (which we do not have at this point)

Kevin Buzzard (Nov 10 2018 at 21:58):

they will not want to work on a Banach manifold

Harry Gindi (Nov 10 2018 at 21:58):

it's not even meaningful on a banach manifold

Harry Gindi (Nov 10 2018 at 21:58):

the derivative of a map of manifolds is a map on tangent bundles

Kevin Buzzard (Nov 10 2018 at 21:58):

I know, I'm just saying that if you write general functions which work in some big generality then you will just end up constantly having to tell these functions to specialise to the case of the real numbers

Harry Gindi (Nov 10 2018 at 21:59):

sure, yes

Kevin Buzzard (Nov 10 2018 at 21:59):

the derivative of a map of manifolds is a map on tangent bundles

right, and you'll then have to identify the tangent space of the reals with the reals etc

Kevin Buzzard (Nov 10 2018 at 21:59):

What I am saying is that in my opinion there is a need for a theory of functions in one real variable

Harry Gindi (Nov 10 2018 at 21:59):

and that identification is not obvious without additional structure

Kevin Buzzard (Nov 10 2018 at 21:59):

I believe that there is a little about functions in one complex variable, somewhere in the modular forms work

Harry Gindi (Nov 10 2018 at 21:59):

I get ya!

Harry Gindi (Nov 10 2018 at 22:00):

I fully agree with this

Harry Gindi (Nov 10 2018 at 22:01):

there's almost always a distinguished most important 1-dimensional case of whatever

Harry Gindi (Nov 10 2018 at 22:01):

imagine if people tried to write the categories library starting with 2-categories

Harry Gindi (Nov 10 2018 at 22:01):

It's also why e.g. Lawvere's ETCC was dead on arrival

Harry Gindi (Nov 10 2018 at 22:02):

anyway, I'm going to give some of this a shot tomorrow morning

Harry Gindi (Nov 10 2018 at 22:02):

cheers!

Cris Perdue (Mar 22 2022 at 00:20):

I am a software developer and longtime aficionado of computerized deduction, taking a scenic excursion from building a web GUI proof assistant "for beginners" (https://prooftoys.org/) to the modern world of Lean.

Panagiotis Angelinos (Feb 21 2024 at 04:48):

Hello all. I'm a new member. I've been interested in Lean for a while. I've recently decided to try my hand at contributing towards mathlib. I am trying to define spectral spaces since it seems most of the hard work has been done already, but I am struggling to figure it out. For example, mathlib already has defined what it means for a topological space to be sober, quasicompact, or quasi-separated, but I do not even know what the syntax in Lean would be to define a quasi-spectral-space (for example) as a sober qcqs space. I am trying to figure this out from looking at various pieces of code and documentation, but I wondered if it was easier to sneakily ask while introducing myself.

Johan Commelin (Feb 21 2024 at 04:59):

Welcome! Can you show a snippet of what you have already tried?

Kevin Buzzard (Feb 21 2024 at 05:00):

Are the things you need classes? (Look up their definition in the source code). If so, you might want to learn about classes and make a new class extending these old ones

Panagiotis Angelinos (Feb 21 2024 at 05:49):

Thanks for the invitation to share some code and the suggestion to look at classes. Here's my snippet so far:

class SpectralSpace (α: Type u) [TopologicalSpace α] extends CompactSpace α,
  QuasiSober α, QuasiSeparatedSpace α, T0Space α where
  qc_open_basis:  {x : α},  {U : Set α},  (S : Set α), x  U  IsOpen U
   IsOpen S  IsCompact S  x  S  S  U

I think this does the trick, but I cobbled it together mostly using hopeful imitation. I think this says a spectral space is sober qcqs (this is what all the extends do) such that the quasi-compact opens form a basis. I would have liked to think of some clever way to extract all the quasi-compact opens and check if it is a basis using some other proposition I found, but I have a feeling Lean doesn't work like that. Also: I thought about including the set of all quasi-compact opens as a datum and including a proposition proving that they generate the topology on the topological space but that seemed far clunkier.

Panagiotis Angelinos (Feb 21 2024 at 05:51):

I'm actually not confident about those chains of implications. I didn't give it the proper thought and I will revisit it.

Johan Commelin (Feb 21 2024 at 06:41):

I think you can express the basis condition more concisely using concepts from the library

Eric Wieser (Feb 21 2024 at 09:10):

I think you might be confusing →and ∧ under the existential, because your statement is trivially true if I pick an S that is not open.

Kevin Buzzard (Feb 21 2024 at 13:12):

My first ever interaction with Johan, back in 2018, was him saying "hi, I heard you defined schemes in Lean, I'm looking at the definition right now, are you sure you aren't confusing → and ∧ under the existential?"

Eric Wieser (Feb 21 2024 at 13:48):

Maybe we should have a linter against ∃ x, ... → P x → ...

Kevin Buzzard (Feb 21 2024 at 14:10):

So I guess this is mathematically correct?

import Mathlib

class SpectralSpace (α : Type*) [TopologicalSpace α] extends CompactSpace α,
    QuasiSober α, QuasiSeparatedSpace α, T0Space α : Prop where
  qc_open_basis:  {U : Set α},  x  U, IsOpen U 
     (S : Set α), IsOpen S  IsCompact S  x  S  S  U

but I guess Johan is suggesting

import Mathlib

class SpectralSpace (α : Type*) [TopologicalSpace α] extends CompactSpace α,
    QuasiSober α, QuasiSeparatedSpace α, T0Space α : Prop where
  qc_open_basis: TopologicalSpace.IsTopologicalBasis {S : Set α | IsOpen S  IsCompact S}

? I still don't understand mathlib's (lack of) conventions regarding Is -- I think this should be called IsSpectralSpace (but I also think CompactSpace should be called IsCompactSpace etc). Note also that I've had to say explicitly that this class is a true-false statement (the : Prop part) because of lean4#2690 .

That's a bit small for a PR though. Every definition in Lean comes with a cost -- one now has to make an API for the definition. What are some basic theorems about spectral spaces? Maybe prove one of them (don't go much over 100 lines for a first PR, I'm talking really basic stuff here). Write a module docstring and make a pull request!

Panagiotis Angelinos (Feb 21 2024 at 14:13):

I was thinking of trying to prove some facts about the constructible topology on spectral spaces, as in the Stacks Project.

Kevin Buzzard (Feb 21 2024 at 14:14):

Perhaps "closed subspace of a spectral space is spectral" or "qc open subspace of a spectral space is spectral"? (are these true? I think so) Of course the first main result you want is Spec(A) is spectral but is this trickier? [on seeing your post appear as I'm writing] yeah, picking stuff off Stacks is also a great approach (please add stacks tags in the Lean code for cross reference purposes)

Panagiotis Angelinos (Feb 22 2024 at 03:54):

After struggling with the constructible topology for a while I decided to aim lower at closed subspaces of spectral spaces are spectral. So far I have used silly copying to get this snippet:

theorem closed_of_spectral_is_spectral [SpectralSpace X] {S: Set X} (hS : IsClosed S) :
    SpectralSpace S := by

I believe this says given a spectral space X, a subset S, and the hypothesis that S is closed, then we prove S is spectral by who knows. I was hoping to find a tactic or something that would turn the goal SpectralSpace S into something like goals for each of the concepts that it extends, and another goal for qc_open_basis. However, I am not finding anything like that, and I am struggling making sense of the documentation.

Kevin Buzzard (Feb 22 2024 at 07:50):

Yeah the typeclass inference system has a bit of a steep learning curve. If you change by to _ and then put your cursor just before the underscore and then click on the blue lightbulb and then click on the option which mentions structures, is that helpful? Or is the issue that the statement doesn't compile?

Panagiotis Angelinos (Feb 22 2024 at 14:28):

Things seem to be compiling ok. The info view is giving me messages like about unsolved goals and so on, so I think that means everything is compiling properly. I think most of my issue is that I am unprepared to actually write out real Lean code because my knowledge of syntax comes from the NNG, some of the learning resources (I didn't read them all), and just looking at other existing bits of code and trying to figure out what it is doing. The helpful blue lightbulb suggested this:

theorem closed_of_spectral_is_spectral [SpectralSpace X] {S: Set X} (hS : IsClosed S) :
    SpectralSpace S where
      isCompact_univ := _
      sober := _
      inter_isCompact := _
      t0 := _
      qc_open_basis := _

which I think now requires me to prove each of these five things separately as subgoals. For isCompact_univ, I was hoping to say something like: we have this theorem IsCompact.of_isClosed_subset that I should be able to apply somehow. But I don't know how to call it, for example. Here is the code for that theorem

/-- A closed subset of a compact set is a compact set. -/
theorem IsCompact.of_isClosed_subset (hs : IsCompact s) (ht : IsClosed t) (h : t  s) :
    IsCompact t :=
  inter_eq_self_of_subset_right h  hs.inter_right ht
#align is_compact_of_is_closed_subset IsCompact.of_isClosed_subset

I think this says, given these three hypotheses, we know the closed subset is compact by some proof, and also this #align statement seems to be here because this was ported over from Lean 3. So, I thought I could apply this theorem to some hypotheses, but I do not have an explicit hypothesis that X is compact (just a hypothesis that it is spectral, which should allow me somehow to grab compactness out of it). I typed in

isCompact_univ := by{
        apply IsCompact.of_isClosed_subset
        }

and now the Lean infoview says:

4 goals
case hs
X: Type u
inst✝¹: TopologicalSpace X
inst: SpectralSpace X
S: Set X
hS: IsClosed S
 IsCompact ?s
case ht
X: Type u
inst✝¹: TopologicalSpace X
inst: SpectralSpace X
S: Set X
hS: IsClosed S
 IsClosed Set.univ
case h
X: Type u
inst✝¹: TopologicalSpace X
inst: SpectralSpace X
S: Set X
hS: IsClosed S
 Set.univ  ?s
case s
X: Type u
inst✝¹: TopologicalSpace X
inst: SpectralSpace X
S: Set X
hS: IsClosed S
 Set S

I don't know how to interpret IsCompact ?s or Set ↑S and I'm not even sure if this is progress or if I've gone down the wrong path.

Kevin Buzzard (Feb 23 2024 at 16:44):

OK so welcome to type theory.

The definition of CompactSpace X is IsCompact (Set.univ : Set X). So what is going on here is that Lean maintains a distinction between "sets and subsets", or, what in Lean would be called types and subsets (or just types and sets). As you've seen in the statement of your theorem above, you have a type X and then you have S : Set X. So what is going on here is that Set X is a type (the type of subsets of X, or the type of sets whose elements are in X if you like), and S : Set X means that S is a term of that type. In particular S is a term, so in particular S is not a type. However it is possible to make a type from S. This type is called ↑S, and a term of this type is a pair consisting of a term x : X and a proof of x ∈ S. This distinction is kept even when talking about "the subset XX of XX" -- you cannot refer to this subset as X because X is a type and subsets are terms, so it needs another name and that name is Set.univ : Set X.

This twist adds an extra layer of complexity to arguments in topology. If you look at the definition of docs#IsCompact then you'll see that it is a predicate on subsets of a topological space. Initially a lot of mathlib was built up in this way, talking about subsets and then if you want to talk about the full type then just apply the predicate to the "universal subset". One place where things really get thorny is taking subsets of a subset, because then you take a subset, promote it from a term to a type by adding an arrow, and then take another subset, and unfortunately the subset of the promoted type is not equal to a subset of the original type (by equal I mean "equal in type theory" -- of course the concepts of a subset and a subset of a subset are mathematically equal but unfortunately we are not doing mathematics here, we are wrestling with foundational nonsense).

The lemma you cite talks about IsCompact, so it's talking about compactness as a property of subsets not of types, and your hypothesis uses CompactSpace, so there is some glue needed to make things work. Either you find the right lemma (where the big space is a CompactSpace) or you muddle through with the lemma you've suggested, which would look like this:

import Mathlib

class SpectralSpace (X : Type*) [TopologicalSpace X] extends CompactSpace X,
    QuasiSober X, QuasiSeparatedSpace X, T0Space X : Prop where
  qc_open_basis:  {U : Set X},  x  U, IsOpen U 
     (S : Set X), IsOpen S  IsCompact S  x  S  S  U

variable (X : Type*) [TopologicalSpace X]

theorem closed_of_spectral_is_spectral [SpectralSpace X] {S: Set X} (hS : IsClosed S) :
  SpectralSpace S where
    isCompact_univ := by
      have h1 : IsCompact (Set.univ : Set X) := by exact? -- translate from CompactSpace to IsCompact
      have h2 := IsCompact.of_isClosed_subset h1 hS (by exact?) -- now you can apply your lemma
      exact? -- now translate back to CompactSpace
    sober := sorry
    inter_isCompact := sorry
    t0 := sorry
    qc_open_basis := sorry

Panagiotis Angelinos (Feb 24 2024 at 02:32):

Thanks so much for the help! This explanation made things much clearer. It seems I now have a correct proof of S being compact, thanks to your suggestions and also those from exact?. I've been working on the rest. Here is what I have so far:

import Mathlib

class SpectralSpace (X : Type*) [TopologicalSpace X] extends CompactSpace X,
    QuasiSober X, QuasiSeparatedSpace X, T0Space X : Prop where
  qc_open_basis:  {U : Set X},  x  U, IsOpen U 
     (S : Set X), IsOpen S  IsCompact S  x  S  S  U

variable (X : Type*) [TopologicalSpace X]

theorem closed_of_spectral_is_spectral [SpectralSpace X] {S: Set X} (hS : IsClosed S) :
  SpectralSpace S where
    isCompact_univ := by
      have h1 : IsCompact (Set.univ : Set X) := by exact isCompact_univ
      have h2 := IsCompact.of_isClosed_subset h1 hS (by exact fun a a  trivial) -- I don't know what fun ⦃a⦄ a ↦ trivial means or does, but it was suggested by exact?
      exact isCompact_iff_isCompact_univ.mp h2
    sober := by
      have h1 : QuasiSober X := by exact SpectralSpace.toQuasiSober
      intro U hU1 hU2
    inter_isCompact := sorry
    t0 := sorry
    qc_open_basis := sorry

This gives me a tactic state of

X: Type u_1
inst✝¹: TopologicalSpace X
inst: SpectralSpace X
S: Set X
hS: IsClosed S
h1: QuasiSober X
U: Set S
hU1: IsIrreducible U
hU2: IsClosed U
  x, IsGenericPoint x U

This is what QuasiSober is defined as in mathlib:

/-- A space is sober if every irreducible closed subset has a generic point. -/
class QuasiSober (α : Type*) [TopologicalSpace α] : Prop where
  sober :  {S : Set α}, IsIrreducible S  IsClosed S   x, IsGenericPoint x S

We have a hypothesis of QuasiSober X which by definition is this predicate 'sober'. (Right? Or is it a proof that the predicate 'sober' is true?). So, I would like to apply this to my hypothesis IsIrreducible U. The syntax for this seems to be
apply h1.sober at hU1 but then I of course get the error message

Failed to find IsIrreducible
  U as the type of a parameter of IsIrreducible ?m.657  IsClosed ?m.657   x, IsGenericPoint x ?m.657.

The reason, from what I understand, is that U is not a term of type Set X but rather a term of Set ↑S! So of course we cannot apply h1.sober directly because it takes in terms of type Set X. I guess U is a pair consisting of a term U : Set X and a proof that U \subset S. Is there a way to get at the "underlying" term U : Set X?

Another reason why I am asking is because I am trying to prove that, if S is a closed subset of a topological space X and T is a closed subset of S, then T is closed in X. I couldn't find a theorem to that effect, which is surprising. It's possible I didn't look well enough. In any case, I tried the following:

theorem closed_of_closed_implies_closed [TopologicalSpace X] {S : Set X} {T : Set S}
  (hS : IsClosed S) (hT : IsClosed T) : IsClosed T := by sorry

but of course this is silly because the first IsClosed T means as a subset of S and the second IsClosed T is supposed to mean as a subset of X, but it doesn't. Somehow, it seems I should be able to refer to the underlying T : Set X so that the second IsClosed T refers to that. Unless there are other ways to deal with these finicky subset of subset things.

Kevin Buzzard (Feb 24 2024 at 06:55):

I'm really sorry, I'm not going to have much time to deal with your questions this weekend. They would be getting a lot more attention if they weren't in #new members and weren't in such a poorly-named thread ("Hello"). Why not start a new thread with a more interesting name in #maths and summarise where you are?

Panagiotis Angelinos (Feb 24 2024 at 13:12):

Sounds good. Thanks for the all the help!


Last updated: May 02 2025 at 03:31 UTC