Hello

Stream: new members

[Harry Gindi]

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

[Johan Commelin]

Hey, welcome! Good to see you.

[Johan Commelin]

Things are going pretty good here (-;

[Harry Gindi]

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

[Johan Commelin]

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

[Harry Gindi]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Harry Gindi]

Does it have Grothendieck constructions

[Johan Commelin]

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

[Johan Commelin]

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

[Harry Gindi]

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

[Harry Gindi]

Ah, ok!

[Johan Commelin]

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

[Harry Gindi]

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]

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

[Harry Gindi]

via Segal's observation

[Harry Gindi]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Harry Gindi]

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

[Johan Commelin]

First you need to install a Lean environment.

[Johan Commelin]

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

[Harry Gindi]

vscode

[Johan Commelin]

Great!

[Johan Commelin]

There is a Lean extension for VScode

[Harry Gindi]

Is the Windows lean environment crippled?

[Johan Commelin]

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

[Harry Gindi]

oh, that's neat!

[Johan Commelin]

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

[Andrew Ashworth]

If you like textbooks I would recommend Theorem Proving in Lean

[Johan Commelin]

Maybe it is about to be fixed.

[Harry Gindi]

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

[Harry Gindi]

that's why I'm asking

[Andrew Ashworth]

Lean on Windows works great

[Kenny Lau]

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

[Andrew Ashworth]

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]

Thanks!

[Kenny Lau]

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

[Harry Gindi]

Both work, Kenny. WSL is slow though

[Harry Gindi]

Disk I/O is extremely bad

[Harry Gindi]

then again, so is mingw64 =D

[Kenny Lau]

what do you mean?

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

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]

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

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

[Kenny Lau]

then what's the best one?

[Harry Gindi]

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

[Harry Gindi]

if you're concerned about performance

[Harry Gindi]

Thanks Johan!

[Andrew Ashworth]

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

[Kenny Lau]

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

[Harry Gindi]

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

[Kenny Lau]

@Harry Gindi ping

[Harry Gindi]

hello!

[Kenny Lau]

Harry Gindi, not ping

[Harry Gindi]

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

[Andrew Ashworth]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

anyway, going to get this lean system installed

[Harry Gindi]

does arch have a lean-git AUR package?

[Harry Gindi]

Looks like it does

[Andrew Ashworth]

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]

i've never investigated it though, so ymmv

[Harry Gindi]

blech, I have an arch installation on this pc

[Andrew Ashworth]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Johan Commelin]

Don't use that arch thing.

[Harry Gindi]

oh, it's bad?

[Harry Gindi]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Harry Gindi]

the arch thing is just a lean system, I thought

[Harry Gindi]

anyway gonna work on this tomorrow morning

[Harry Gindi]

cheers all

[Kevin Buzzard]

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

fair

[Scott Morrison]

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]

@Harry Gindi ^^ that

[Scott Morrison]

Also, welcome @Harry Gindi. :-)

[Harry Gindi]

Got it, thanks!

[Harry Gindi]

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

[Kevin Buzzard]

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]

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]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

I'm guessing that monads work well?

[Kevin Buzzard]

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

[Harry Gindi]

ah

[Kevin Buzzard]

groups work well

[Kevin Buzzard]

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

[Harry Gindi]

I mean, my research is in category theory

[Harry Gindi]

but I'll see how hard it is

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Harry Gindi]

Do presheaves of sets make sense?

[Kevin Buzzard]

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]

they call them presheaves of types here

[Kevin Buzzard]

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

[Harry Gindi]

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

[Kevin Buzzard]

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]

My code sucks though

[Kevin Buzzard]

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

[Kevin Buzzard]

I am currently refactoring all of it with an MSc student

[Harry Gindi]

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

[Harry Gindi]

working with functors of points the whole way?

[Harry Gindi]

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

[Kevin Buzzard]

I followed the stacks project

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

But nowadays we would not write it like that

[Kevin Buzzard]

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

[Kevin Buzzard]

As of about last week

[Harry Gindi]

neat!

[Harry Gindi]

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

[Harry Gindi]

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

[Kevin Buzzard]

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]

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]

mhm

[Harry Gindi]

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

[Harry Gindi]

cheers, this seems exciting

[Kevin Buzzard]

it's the future

[Kevin Buzzard]

but I might have died before it becomes really important

[Kevin Buzzard]

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

[Harry Gindi]

ascended to robothood

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Harry Gindi]

like any assistant they must be trained =p

[Harry Gindi]

otherwise all they do is spill coffee on you

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Harry Gindi]

this might be a nice change of pace for him

[Kevin Buzzard]

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

[Harry Gindi]

is anyone doing analysis-related stuff?

[Kevin Buzzard]

Yes, but it's happening very slowly

[Harry Gindi]

because he always liked analysis

[Harry Gindi]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Harry Gindi]

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

[Kevin Buzzard]

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]

Is that even possible?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Harry Gindi]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Eventually we'll have them on Banach manifolds or something

[Harry Gindi]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

they will not want to work on a Banach manifold

[Harry Gindi]

it's not even meaningful on a banach manifold

[Harry Gindi]

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

[Kevin Buzzard]

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]

sure, yes

[Kevin Buzzard]

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]

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

[Harry Gindi]

and that identification is not obvious without additional structure

[Kevin Buzzard]

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

[Harry Gindi]

I get ya!

[Harry Gindi]

I fully agree with this

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

cheers!

[Cris Perdue]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Eric Wieser]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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 $X$ of $X$" -- 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]

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]

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]

Sounds good. Thanks for the all the help!