topological space docs

Stream: maths

[Kevin Buzzard]

Ok so after a ropey start (see my heq thread earlier) I made it through the topological_space.lean file today and wrote some docs on it: https://github.com/kbuzzard/mathlib/blob/docs-topspaces/docs/theories/topological_spaces.md . I needed to read this file for my work on schemes -- in particular I had to finally understand what a filter was and what they had to do with topological spaces.

[Patrick Massot]

You are a bit unfair with filters. You should at least explain that they allow to cover uniformly the cases of sequences and maps from topological spaces. And then slightly more exotic stuff like one-sided limits at some real. That's why Bourbaki invented them.

[Patrick Massot]

They also allow to mimic using sequential continuity and compactness for non-metric spaces

[Mario Carneiro]

One way to motivate them is to consider the ~16 variations on L'hopital's theorem that arise with lots of permutations of limits to different places in the domain and codomain

[Kevin Buzzard]

I was just grumpy about them because they have actively stopped me doing what should be trivial stuff for a couple of days, because I didn't know what \Glb meant

[Kevin Buzzard]

when I actually ploughed through the file and a lot of the imports, and set pp.all on occasionally etc etc and finally got to the bottom of things and discovered that F <= G iff G subseteq F

[Kevin Buzzard]

then it all began to make sense

[Patrick Massot]

This is what this definition if compactness is about: a space is compact if every sequence has a converging subsequence,made true for all spaces

[Mario Carneiro]

The description of topological basis is also a bit grumpy; the point as I mentioned before is to say "a topological basis is a collection of sets satisfying these two axioms" and then fold in the connection to generating a topology

[Kevin Buzzard]

I'm sure it's a very cute way to think about things

[Kevin Buzzard]

yeah, I had to get up early this morning, I've been in a grumpy mood all day :-)

[Patrick Massot]

I'm defending filters here but zulip and gitter can testify I went through the same frustrations

[Mario Carneiro]

In fact I think the "filters are a complete lattice" angle should probably be emphasized more, since it underlies many of the filter-theoretic definitions

[Mario Carneiro]

A filter which is not bottom is called a proper filter fyi

[Kevin Buzzard]

Mario, the reason I don't buy your explanation is that there is a standard definition of a basis of a topological space, which we all learn, and which is on Wikipedia, and which is not what is implemented, so all your protestations that it's a better way of doing it are cancelled out by the fact that every mathematician will be confused by the way it's done. I have flagged the relevant lemma which saves us.

[Mario Carneiro]

but it is that definition...

[Patrick Massot]

I think Mario had the right idea when I faced that:we keep filters but add lemmas translating to usual stuff in usual situations

[Kevin Buzzard]

[explanation of why bases are done like that]

[Kevin Buzzard]

Yes, I explictly flag the lemmas saying "oh look, compactness looks insane, here's the lemma you need"

[Kevin Buzzard]

"bases look insane, here's the lemma you need"

[Kevin Buzzard]

That's the philosophy of the docs

[Mario Carneiro]

https://en.wikipedia.org/wiki/Base_(topology)

A base is a collection B of subsets of X satisfying these two properties:
1. The base elements cover X.
2. Let B1, B2 be base elements and let I be their intersection. Then for each x in I, there is a base element B3 containing x and contained in I.

[Kevin Buzzard]

Now I can use topological spaces in Lean, and this morning I couldn't.

[Kevin Buzzard]

Right.

[Kevin Buzzard]

Whereas you have generate_open

[Kevin Buzzard]

it's the generate_open that makes it unusable

[Patrick Massot]

I'm sure you could also explain why filters are useful

[Mario Carneiro]

Any topological basis is a basis for the topology it generates

[Kevin Buzzard]

the lemma you proved and I flagged makes the definition usable

[Mario Carneiro]

you can always satisfy that clause with refl

[Kevin Buzzard]

My point is simply that if you want to prove that (a,b) x (c,d) is a basis of open sets for the standard topology on R^2, you cannot possibly do that from the definition

[Kevin Buzzard]

but it's easy from the lemma

[Mario Carneiro]

Yes you can

[Kevin Buzzard]

_you_ can

[Kevin Buzzard]

a mathematician can't

[Kevin Buzzard]

becuase they have no clue how to use generate_open

[Mario Carneiro]

Those are two different goals though

[Mario Carneiro]

you are trying to prove that some basis is a basis for something else, rather than just proving it's a basis

[Patrick Massot]

My wife says I must stop participating but please be nice :smiley:

[Kevin Buzzard]

In maths, the proof goes "insert argument to prove that if x is in an open set U in R^2 then ther's some (a,b) x (c,d) in U containing x and now we're done

[Kevin Buzzard]

in Lean the proof from the definition of basis goes "that, and then we have to prove something about generate_open"

[Kevin Buzzard]

except now we don't because of the lemma

[Mario Carneiro]

You have a preconceived topology in that example

[Kevin Buzzard]

yes, the one the mathematicans use :-)

[Mario Carneiro]

I'm talking about proving that some collection of sets is a basis full stop

[Kevin Buzzard]

I know

[Kevin Buzzard]

but that's a silly notion

[Mario Carneiro]

That's the one wikipedia discusses

[Kevin Buzzard]

there's no generate_open there

[Kevin Buzzard]

it's the generate_open which makes the definition a complete pain to work with

[Kevin Buzzard]

and it's the lemma that saves us

[Kevin Buzzard]

so I highlight the lemma

[Kevin Buzzard]

that's all

[Kevin Buzzard]

the lemmas are all there

[Mario Carneiro]

The generate_open is dischargable by refl, like I said

[Kevin Buzzard]

I'm saying the definitions are silly, but that's OK because the lemmas are there

[Kevin Buzzard]

yeah but I don't really know what that means

[Kevin Buzzard]

and I know what the lemma means

[Mario Carneiro]

If S satisfies axioms 1 and 2, then it is a basis for (generate_open S)

[Kevin Buzzard]

and a generic mathematician will come along

[Kevin Buzzard]

with a proof of the two things in wikipedia

[Kevin Buzzard]

and will want to prove that they have a basis

[Kevin Buzzard]

and so they can use the lemma

[Mario Carneiro]

okay I get it you think the notion is useless

[Kevin Buzzard]

right

[Kevin Buzzard]

but I'm not saying it shouldn't be there

[Kevin Buzzard]

I'm just explaining why I had to write the docs

[Mario Carneiro]

but the docs are

[Kevin Buzzard]

and why they came out grumpy :-)

[Kevin Buzzard]

that is an absurd definition of compact as well.

[Kevin Buzzard]

It should be a theorem not a definition.

[Kevin Buzzard]

But again it doesn't matter

[Kevin Buzzard]

anyway, I am not grumpy any more :-)

[Mario Carneiro]

I'm not sure how much I want to defend this... I think Johannes thought the filter stuff would make everything neat and concise

[Kevin Buzzard]

it doesn't matter

[Kevin Buzzard]

I'm just taking a contrary position for a laugh really

[Kevin Buzzard]

I'm really happy now

[Kevin Buzzard]

I can work topological spaces

[Mario Carneiro]

I personally have a preference for standard point-set definitions

[Kevin Buzzard]

and I'm hoping that other people with the same background as me (i.e. basically two courses in topology and that's it) can do the same

[Mario Carneiro]

but there are enough lemmas around to get rid of any filter claims you come across

[Kevin Buzzard]

yeah, that's why Hausdorff is called t2 probably ;-)

[Mario Carneiro]

t2 is shorter :)

[Kevin Buzzard]

I'm really happy with the lemmas. I was preparing a list of lemmas which you should have proved

[Kevin Buzzard]

and it came out empty in the end

[Kevin Buzzard]

Occasionally it would have size 1 or 2

[Kevin Buzzard]

and then I'd find them :-)

[Kevin Buzzard]

Props to @Johannes Hölzl too.

[Mario Carneiro]

yeah he gets the credit for most of this work

[Kevin Buzzard]

It's a really nice complete library

[Kevin Buzzard]

even though some definitions are theorems and some theorems are definitions ;-)

[Kevin Buzzard]

I guess you guys can barely tell the difference

[Kevin Buzzard]

you probably think I'm talking about unfolding or something

[Mario Carneiro]

it will teach you to forget about definitions and worry more about interfaces

[Kevin Buzzard]

OK, enough CS baiting. Thank you for your library!

[Kevin Buzzard]

I need to learn what this word interface means

[Mario Carneiro]

does API mean something to you?

[Kevin Buzzard]

not really

[Kevin Buzzard]

this is some way of talking to the theorems

[Kevin Buzzard]

or something

[Kevin Buzzard]

Are my docs some sort of attempt to make an API for mathematicians trying to use topological spaces in Lean?

[Mario Carneiro]

it's the idea that you encapsulate the underlying definition, somehow make it inaccessible, and then only use theorems that express properties of it

[Kevin Buzzard]

encapsulate is another mystery

[Kevin Buzzard]

these are all very CS words

[Kevin Buzzard]

I understand that a mathematician will come along with a proof that every cover has a finite subcover and will want to deduce that their space is compact

[Kevin Buzzard]

so I point them to the lemma which says this

[Kevin Buzzard]

[and make some snarky remark probably about how the definition is something else]

[Mario Carneiro]

Category theory does this a lot, for example: A product of two objects is some object with a universal property, so that you can only use the universal property to prove stuff rather than unfolding whatever the product is "actually" defined to be in a particular category

[Kevin Buzzard]

universal properties I understand

[Kevin Buzzard]

but I don't understand why this is an argument for giving an unrecognisable definition of compact

[Mario Carneiro]

A biconditional is also a "universal property", in a sense

[Kevin Buzzard]

biconditional is a theorem of the form X iff Y?

[Mario Carneiro]

it tells you everything you ever need to know about the definition, without actually telling you what the definition is

[Kevin Buzzard]

I see

[Kevin Buzzard]

but you really need to know where the theorem is

[Mario Carneiro]

yes, that's the public part

[Mario Carneiro]

the definition is the private part

[Kevin Buzzard]

Maybe I saw this in java once

[Kevin Buzzard]

your variables are private

[Kevin Buzzard]

and you make some functions which lets the user change them

[Kevin Buzzard]

or read them

[Kevin Buzzard]

without actually letting them fiddle with them directly

[Kevin Buzzard]

sorry, methods

[Kevin Buzzard]

but I didn't realise this had anything to do with topological spaces at the time

[Mario Carneiro]

One reasonably basic example of a gnarly construction is the Kuratowski pair (a,b) = {{a}, {a, b}}

[Kevin Buzzard]

eew

[Kevin Buzzard]

eew

[Kevin Buzzard]

I see

[Kevin Buzzard]

that's a great example

[Kevin Buzzard]

we just need (a,b) = (c,d) iff a=c and b=d

[Mario Carneiro]

exactly

[Kevin Buzzard]

so we point the user to where that is proved

[Kevin Buzzard]

and they can't see the disgusting truth behind it all

[Mario Carneiro]

and later, we might want to change the definition for some reason to, say, {{0,a}, {1, b}} and that's okay as long as we can still prove the defining property, since no user depended on the specific construction

[Kevin Buzzard]

but the compactness thing is different. We go for Kuratowski because all the choices are horrible and this one is the least horrible

[Kevin Buzzard]

I see

[Kevin Buzzard]

it's not completely different

[Kevin Buzzard]

you are reserving the right to invent some even more weird thing that is better than filters

[Kevin Buzzard]

and then change the definition of compactness

[Kevin Buzzard]

because it compiles better on a quantum computer or whatever

[Mario Carneiro]

or even just the point-set definition

[Kevin Buzzard]

I see. In fact you could just play that trump card and that would shut me up

[Kevin Buzzard]

you should just say "Kevin, you don't understand, the definition we have here works better if your machine has 8 cores"

[Kevin Buzzard]

and I would have no response

[Mario Carneiro]

the real point is that it shouldn't matter what the actual definition is, and if it does you're doing it wrong

[Kevin Buzzard]

This is different to mathematics

[Kevin Buzzard]

If you wrote a maths book with some weird definitions of things

[Kevin Buzzard]

and then proved theorems which said that they were the same as everyone else's definition

[Mario Carneiro]

there's also the pedagogical angle, but that's a different issue

[Kevin Buzzard]

people would be confused as to why you were doing it

[Mario Carneiro]

I don't think that exact thing is unheard of though

[Kevin Buzzard]

and you can't answer "this definition works better if you have 8 brains"

[Mario Carneiro]

your new definition might be suitable to a particular sort of generalization, for example

[Kevin Buzzard]

As you are probably aware, I am extremely interested in the pedagogical angle

[Kevin Buzzard]

and have very little understanding of stuff like run time analysis and other CS-related matters

[Mario Carneiro]

in the pedagogical view, you might redefine the same thing several times depending on the current teaching goals

[Mario Carneiro]

the new definition may not even be the same as earlier ones, although it is usually a generalization or provably equivalent

[Kevin Buzzard]

So ultimately I should not care about your definitions, my main aim is to make sure that the interfaces are there.

[Mario Carneiro]

exactly

[Kevin Buzzard]

OK maybe tomorrow I will degrump it a bit :-)

[Kevin Buzzard]

but now I have to make a birthday present

[Mario Carneiro]

lol it's my birthday so I'll just pretend that's for me ;)

[Kevin Buzzard]

ha ha it's for my son's GF

[Kevin Buzzard]

happy birthday

[Kevin Buzzard]

I'm not entirely sure you'd want a plastic T anyway

[Mario Carneiro]

good mathlib docs are a good present :)

[Kevin Buzzard]

OK well seeing as it's your birthday I de-grumped the docs a bit.

[Kevin Buzzard]

even though it's strictly speaking not even your birthday any more where I'm sitting

[Kevin Buzzard]

I'm now about to get onto the job I meant to do today, which was to prove that Spec(R) is compact using some argument involving bases :-)

[Kevin Buzzard]

now I understand the interface better :-)

[Kevin Buzzard]

Thanks as ever, by the way.

[Mario Carneiro]

I forget if the contrapositive form of the compactness definition is there: a collection of closed sets with the finite intersection property has nonempty intersection

[Kevin Buzzard]

I didn't see it

[Kevin Buzzard]

and I almost mentioned it as a theorem which should be there

[Kevin Buzzard]

but then I decided I'd never used it in my life :-)

[Kevin Buzzard]

I almost mentioned it the other day when Simon was asking whether the same was true for an arbitrary set

[Mario Carneiro]

I guess it is somewhat similar to the filter definition

[Kevin Buzzard]

Hmm, I've just realised that I want that a mathlib-basis is a Wikipedia-basis

[Mario Carneiro]

that's just the first two parts of the definition

[Kevin Buzzard]

oh sorry I don't mean that

[Mario Carneiro]

If h1 and h2 are proofs of the two axioms, then <h1, h2, rfl> is a proof it's a mathlib-basis

[Mario Carneiro]

that's what I've been saying

[Kevin Buzzard]

is_topological_basis_of_open_of_nhds

[Kevin Buzzard]

I mean the converse of that

[Kevin Buzzard]

Yes, sorry, I understand now

[Kevin Buzzard]

I was talking nonsense at some points earlier

[Kevin Buzzard]

when I said "wikipedia definition"

[Kevin Buzzard]

I sometimes meant "hypotheses in is_topological_basis_of_open_of_nhds"

[Kevin Buzzard]

:-/

[Mario Carneiro]

mem_nhds_of_is_topological_basis is the easiest way to get converses of that stuff

[Kevin Buzzard]

https://topospaces.subwiki.org/wiki/Basis_for_a_topological_space

[Mario Carneiro]

but there should be a theorem saying that a basis element is open

[Kevin Buzzard]

there's a website (which I've never heard of) giving that as the definition.

[Kevin Buzzard]

This is evidence that I am very fluid with what my definition is :-/

[Kevin Buzzard]

mem_nhds means I might have to get my hands dirty with neighbourhoods maybe :-/

[Mario Carneiro]

which statement are you going for specifically?

[Kevin Buzzard]

if B is a basis then I want that for all U open and for all x in U, there's V in B with x in V in U

[Kevin Buzzard]

because as we all know

[Kevin Buzzard]

50% of the time I will swear blind that this is the definition of a basis in Wikipedia

[Kevin Buzzard]

and I don't want to do induction on generate_open

[Kevin Buzzard]

I want this to be there on a plate

[Kevin Buzzard]

Kenny proved it

[Kevin Buzzard]

in a file called temp.lean :-)

[Kevin Buzzard]

but I was trying to avoid importing this file

[Kevin Buzzard]

because its name looked a bit ominous

[Kevin Buzzard]

I can do this myself

[Kevin Buzzard]

The lemmas I need are all there

[Kevin Buzzard]

I just need to glue them

[Kevin Buzzard]

This morning I didn't know what nhds a was

[Kevin Buzzard]

I have to remember that I'm not scared of it any more

[Mario Carneiro]

I can add these to the file:

lemma is_open_of_is_topological_basis {s : set α} {b : set (set α)}
  (hb : is_topological_basis b) (hs : s ∈ b) : _root_.is_open s :=
is_open_iff_mem_nhds.2 $ λ a as,
(mem_nhds_of_is_topological_basis hb).2 ⟨s, hs, as, subset.refl _⟩

lemma mem_subset_basis_of_mem_open {b : set (set α)}
  (hb : is_topological_basis b) {a:α} (u : set α) (au : a ∈ u)
  (ou : _root_.is_open u) : ∃v ∈ b, a ∈ v ∧ v ⊆ u :=
(mem_nhds_of_is_topological_basis hb).1 $ mem_nhds_sets ou au

[Kevin Buzzard]

It's the easy way of is_open_iff_mem_nhds I need and then I'm done :-)

[Kevin Buzzard]

yeah, what you said

[Kevin Buzzard]

I'd vote for them definitely.

[Kevin Buzzard]

Then I can eschew temp.lean completely

[Mario Carneiro]

I like mem_nhds_of_is_topological_basis because it generalizes well to all sorts of bounded quantification over open sets that comes up in topology, like continuity or compactness that can be stated with basis sets

[Kevin Buzzard]

I didn't like it until today because of the obscure definition of nhds

[Kevin Buzzard]

but again there was a lemma -- in this case mem_nhds_sets_iff -- which made this clear

[Kevin Buzzard]

or even nhds_sets, which I mention in the docs

[Kevin Buzzard]

I see. I'm mentioning all the results that a mathematician needs for the interface.

[Kevin Buzzard]

eew, exists v \in B -- I have to run classical.some twice to get that v is in B

[Mario Carneiro]

You can use exists.fst for the v \in B hypothesis

[Kevin Buzzard]

That means exists v in B, P (B a set) unravels to exists v in X, exists H : v in B, ...

[Kevin Buzzard]

Why not unravel to exists v in X, v in B and ...

[Mario Carneiro]

You can also use exists v : B, P to pack them both into one

[Kevin Buzzard]

yeah but you wrote v in B not me ;-)

[Mario Carneiro]

because that same translation works for a wide variety of binders

[Kevin Buzzard]

I don't know what a binder is

[Mario Carneiro]

A thing that introduces a bound variable

[Mario Carneiro]

like exists or forall or lambda

[Kevin Buzzard]

somehow I thought that there were only about three of these

[Mario Carneiro]

or Glb or Lub

[Kevin Buzzard]

but you're saying "exists v \in B" is somehow another one

[Mario Carneiro]

or indexed intersection

[Kevin Buzzard]

I see.

[Mario Carneiro]

No, I'm saying that every binder has the translation Q a R b, p a => Q a, Q (_ : a R b), p a where Q is any binder

[Mario Carneiro]

and R is any infix operator

[Kevin Buzzard]

unknown identifier 'exists.fst'

[Mario Carneiro]

should be in logic.basic

[Mario Carneiro]

It's Exists.fst so you can use projections

[Kevin Buzzard]

capital E, got it

[Kevin Buzzard]

you use Q again

[Patrick Massot]

OK well seeing as it's your birthday I de-grumped the docs a bit.

I think it still misses the main point of using filters: you have limits at a point and limits when a real variable or a natural number goes to infinity gathered in a single definition. For instance uniqueness of limit that you mention in your doc is proved for all three (and more) situations at once. This has nothing to do with "non-mathematical points such as running times".

[Kevin Buzzard]

I just don't know anything about how filters are used in practice so am in no position to be able to write those parts of the docs properly. I've never had to use them before and I don't really care about explaining them for this reason; I just wanted to get down the things I needed to know myself.

[Johannes Hölzl]

@Kevin Buzzard just added your documentation, I guess we can add more comments on filters later.
I think one problem why there is not a lot of knowledge about filters (or nets) in math, is that it is obvious and usually something you don't need to think about. But we are in a formal system, so we are either forced to generalize over limits (using filters or nets) or we produce a lot of duplication (as Mario and Patrick mentioned). We can avoid them and define things like compact using open covers etc. But some proofs get much more concise using the fact that you can use the complete lattice (and even category theory) properties properties of filters. Currently it is not always intuitive to work with filters, but maybe with more automation and better syntax notations and support from the parser it may get better.
In the end they are a powerful abstraction, and as most abstractions it takes some time to learn it.

[Kevin Buzzard]

Yeah, Mario convinced me not to worry about what was a definition and what was a theorem, as long as the theorems were all there.

[Sebastien Gouezel]

There is a very expressive way to use filters, with the word eventually.
def eventually {α : Type} (P : α → Prop) (f : filter α) := {x | P x} ∈ f.sets
Then if you want to say that, eventually, some function u defined on nat is nonnegative, you write
eventually (λn, 0 ≤ u n) at_top
If you want to say the same thing around a point x, say (which corresponds to a filter at x), you just write it as
eventually (λy, 0 ≤ f y) (at x)
In this way, you can also write readable definitions of limits, or essentially whatever involves filters. This is the only way I use filters in Isabelle, and I was essentially never stuck.

[Patrick Massot]

@Johannes Hölzl what do you think about adding (and using) this definition?

[Johannes Hölzl]

I'm fine with adding this definition, especially with a corresponding quantifier notation (and also its dual the frequently quantifier). I'm just not sure if we should abandon the f.sets notation or keep both.

[Mario Carneiro]

I want to refactor the filter stuff so that .sets is superfluous, i.e. s \in f means s \in f.sets. I guess we can support eventually if it's a reducible definition, but I don't like the idea of duplicating everything for this purpose

[Johannes Hölzl]

Setting up a has_mem for filter is surely a good idea.