Show that the discrete topology is t2

Stream: new members

[Saul Glasman]

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]

Do you understand how to unfold a definition?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

don't unfold definitions!

[Kevin Buzzard]

and the tactic which proves true is trivial

[Patrick Massot]

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

[Kevin Buzzard]

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]

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]

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]

oh sorry I missed the part where you defined discrete

[Saul Glasman]

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]

Does "trivial" work anyway?

[Kevin Buzzard]

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

[Saul Glasman]

Ah, trivial does work! Thank you

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

Right

[Kenny Lau]

because in maths $e$ has 5 definitions

[Patrick Massot]

Where do you see that exercise?

[Kevin Buzzard]

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]

so you know that you're trying to prove trivial

[Patrick Massot]

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

[Saul Glasman]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Saul Glasman]

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

[Patrick Massot]

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]

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]

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

[Alex J. Best]

Patrick Massot said:

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

:flushed:

[Patrick Massot]

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]

Fixed :grinning: sorry!

[Patrick Massot]

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.