Zulip Chat Archive

Stream: new members

Topic: Show that the discrete topology is t2


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Oct 10 2020 at 21:40):

Do you understand how to unfold a definition?

view this post on Zulip Kevin Buzzard (Oct 10 2020 at 21:40):

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

view this post on Zulip Kevin Buzzard (Oct 10 2020 at 21:40):

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

view this post on Zulip Kenny Lau (Oct 10 2020 at 21:41):

don't unfold definitions!

view this post on Zulip Kevin Buzzard (Oct 10 2020 at 21:41):

and the tactic which proves true is trivial

view this post on Zulip Patrick Massot (Oct 10 2020 at 21:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 10 2020 at 21:42):

oh sorry I missed the part where you defined discrete

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Oct 10 2020 at 21:42):

Does "trivial" work anyway?

view this post on Zulip Kevin Buzzard (Oct 10 2020 at 21:43):

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

view this post on Zulip Saul Glasman (Oct 10 2020 at 21:43):

Ah, trivial does work! Thank you

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 10 2020 at 21:45):

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

view this post on Zulip Kevin Buzzard (Oct 10 2020 at 21:45):

Right

view this post on Zulip Kenny Lau (Oct 10 2020 at 21:45):

because in maths ee has 5 definitions

view this post on Zulip Patrick Massot (Oct 10 2020 at 21:45):

Where do you see that exercise?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 10 2020 at 21:46):

so you know that you're trying to prove trivial

view this post on Zulip Patrick Massot (Oct 10 2020 at 21:46):

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

view this post on Zulip Saul Glasman (Oct 10 2020 at 21:48):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 10 2020 at 21:51):

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

view this post on Zulip Saul Glasman (Oct 10 2020 at 21:53):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Oct 10 2020 at 21:58):

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Oct 10 2020 at 22:03):

Fixed :grinning: sorry!

view this post on Zulip 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