Stream: new members

Topic: Show that the discrete topology is t2

Saul Glasman (Oct 10 2020 at 21:38):

Hi all,

This is one of the exercises from the "topological spaces" section of the LFTCM workshop, solution not provided, and I think I'm missing something about how to use typeclasses. In the exercises file, the t2 typeclass is defined the same way as in mathlib

class t2_space (X : Type) [topological_space X] := ...
(why not class t2_space (X: Type) extends topological_space X?)

but the discrete topology is defined as an explicit term of toplogical_space X rather than its own typeclass as in mathlib:

def discrete (X : Type) : topological_space X :=
{ is_open := λ U, true, -- everything is open
univ_mem := trivial,
union := begin intros B h, trivial, end,
inter := begin intros A hA B hB, trivial, end }


To show that the discrete topology is t2, I want to start with

instance t2_discrete (X: Type): @t2_space X (discrete X) := {
t2 := by {
intros x y hxy,
use [{x}, {y}],
simp,
???
}
}


and the next thing I have to prove is is_open {x}. I feel like Lean should already know this, since the underlying topological space is discrete, but I don't know how to say that - can anyone help?

Kevin Buzzard (Oct 10 2020 at 21:40):

Do you understand how to unfold a definition?

Kevin Buzzard (Oct 10 2020 at 21:40):

Try unfold is_open and you'll replace the is_open function by its definition

Kevin Buzzard (Oct 10 2020 at 21:40):

and it seems to me that is_open {x} is by definition equal to true

Kenny Lau (Oct 10 2020 at 21:41):

don't unfold definitions!

Kevin Buzzard (Oct 10 2020 at 21:41):

and the tactic which proves true is trivial

Patrick Massot (Oct 10 2020 at 21:41):

Note that this file is about rebuilding the theory from scratch, not about using mathlib.

Kevin Buzzard (Oct 10 2020 at 21:41):

If you know all about topological spaces and are asking intelligent questions about how to do stuff like that in Lean Kenny, then you are me 3 years ago

Saul Glasman (Oct 10 2020 at 21:42):

Right, I'm really just justifying my question by saying I can't just look at how mathlib does it to find the answer

Kevin Buzzard (Oct 10 2020 at 21:42):

and when I started to understand that I could unfold everything, this whole Lean business started making a lot more sense to me

Kenny Lau (Oct 10 2020 at 21:42):

oh sorry I missed the part where you defined discrete

Saul Glasman (Oct 10 2020 at 21:42):

That doesn't seem to unfold... I have seen the unfold tactic in use but I don't think I really understand what Lean considers "unfoldable"

Kevin Buzzard (Oct 10 2020 at 21:42):

Does "trivial" work anyway?

Kevin Buzzard (Oct 10 2020 at 21:43):

I mean, I unfolded it in my head :-)

Saul Glasman (Oct 10 2020 at 21:43):

Ah, trivial does work! Thank you

Kevin Buzzard (Oct 10 2020 at 21:44):

This idea of what is true by definition and what is true because of a theorem is completely alien to mathematicians. For example, in the natural number game, n+0=n is true by definition, but 0+n=n is true because of a theorem (induction on n).

Kevin Buzzard (Oct 10 2020 at 21:45):

So it's a weird implemention-dependent notion, right? Mathematicians can't see any difference between 0+n=n and n+0=n

Kenny Lau (Oct 10 2020 at 21:45):

yes, and I think the Lean term "definition" should be translated as the mathematical term "implementation"

Right

Kenny Lau (Oct 10 2020 at 21:45):

because in maths $e$ has 5 definitions

Patrick Massot (Oct 10 2020 at 21:45):

Where do you see that exercise?

Kevin Buzzard (Oct 10 2020 at 21:46):

So you want to prove is_open {x} but you can trace the definition of is_open back and see that it's lambda U, trivial -- this could have been done in all manner of ways but it was done in this way

Kevin Buzzard (Oct 10 2020 at 21:46):

so you know that you're trying to prove trivial

Patrick Massot (Oct 10 2020 at 21:46):

I found it, it's a "bonus exercise".

Saul Glasman (Oct 10 2020 at 21:48):

Yeah sorry, it's not explicitly sketched out but it's mentioned in a comment

Patrick Massot (Oct 10 2020 at 21:49):

This somehow explain why it's not really properly laid out. The surrounding setup makes it painful.

Patrick Massot (Oct 10 2020 at 21:51):

Oh wow, the definition of T2 is not correct in this file!

Saul Glasman (Oct 10 2020 at 21:53):

It doesn't have x \ne y, right?

Patrick Massot (Oct 10 2020 at 21:55):

But again the main problem is the setup mixing classes and this definition of discrete as a def. The definition itself is fine as an example of a topological structure, but not for serious use later.

Patrick Massot (Oct 10 2020 at 21:57):

So the right setup is to have, either as a def or a class:

def discrete {X : Type*} [topological_space X] : Prop :=  ∀ U : set X, is_open U


and then use that as your assumption in t2_discrete {X : Type} [topological_space X] (hX : ∀ U : set X, is_open U) : t2_space X := (which can be an instance if you made discrete a class, or a lemma in any case)

Patrick Massot (Oct 10 2020 at 21:58):

In the proof you'll probably want to use singleton_inter_eq_empty.

Alex J. Best (Oct 10 2020 at 21:58):

Patrick Massot said:

Oh wow, the definition of T2 is not correct in this file!

:flushed:

Patrick Massot (Oct 10 2020 at 21:59):

Could you open an issue at the LFTCM repository? I need to go to bed now, but I'll fix that tomorrow if Alex doesn't beat me to it.

Alex J. Best (Oct 10 2020 at 22:03):

Fixed :grinning: sorry!

Patrick Massot (Oct 10 2020 at 22:06):

I think we also need a fix addressing the issue that the file doesn't really setups things in a way that makes this bonus exercise nice. The easy fix is to remove the exercise. Another fix is to define discrete as I explained above.

Last updated: May 08 2021 at 18:17 UTC