Zulip Chat Archive

Stream: maths

Topic: product topology


view this post on Zulip Rohan Mitta (Jul 24 2018 at 17:10):

Hi! I'm trying to define the product topology and am running into issues. I may have made a silly mistake somewhere, but it seems to me that "I" should have type set (set (α × β)), but I get a type mismatch error. Any help would be greatly appreciated.

import analysis.topology.continuity
import analysis.topology.topological_space
open set filter lattice classical


def product_top {α : Type*} {β : Type*} (X : topological_space α) (Y : topological_space β) : topological_space (α × β) :=
{is_open := λ (W : set (α × β),  (I : (set_of (λ (b : set (α × β)),  (U : set α) (V : set β), is_open U  is_open V  b = set.prod U V))), W = ⋃₀ I,
 is_open_univ := sorry, is_open_inter := sorry, is_open_sUnion := sorry}

view this post on Zulip Johan Commelin (Jul 24 2018 at 17:10):

This is already in mathlib. Did you know that?

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 17:16):

first error for me is at the comma after alpha x beta

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 17:17):

because it's expecting a close bracket

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 17:20):

Your I seems to have type ↥{b : set (α × β) | ∃ (U : set α) (V : set β), is_open U ∧ is_open V ∧ b = set.prod U V}

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 17:25):

#check λ (α : Type) (β : Type) [topological_space α] [topological_space β], (set_of (λ (b : set (α × β)),
            (U : set α) (V : set β), is_open U  is_open V  b = set.prod U V))

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 17:26):

that has type Π (α β : Type) [_inst_1 : topological_space α] [_inst_2 : topological_space β], set (set (α × β))

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 17:28):

So this term: (set_of (λ (b : set (α × β)), ∃ (U : set α) (V : set β), is_open U ∧ is_open V ∧ b = set.prod U V)) is the term which has type set (set (α × β))

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 17:30):

and in particular that's just a term. OK so when you ask that there exists a term I which has type [that term above], Lean says "wait, that's a term, not a type, how can he want a term of that type? Oh I know I'll turn that set_of term above into a subtype, and then I can be a term of that type.

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 17:37):

Yeah it all makes sense --

#check @set_of
-- set_of : Π {α : Type u_1}, (α → Prop) → set α

set_of eventually produces a term t of type set X for some X, and your I is a term of type t so you're one layer too deep

view this post on Zulip Rohan Mitta (Jul 24 2018 at 20:38):

Thanks, that's made it a lot clearer. I think I'll be able to figure it out from there.

view this post on Zulip Rohan Mitta (Jul 24 2018 at 20:39):

Hi Johan,

This is already in mathlib. Did you know that?

I did not know that. Where can I find it?

view this post on Zulip Luca Gerolla (Jul 24 2018 at 21:56):

Hi Rohan, it's an instance at line 909 of topological_space

view this post on Zulip Luca Gerolla (Jul 24 2018 at 21:57):

instance [t₁ : topological_space α] [t₂ : topological_space β] : topological_space (α × β) :=
induced prod.fst t₁  induced prod.snd t₂

view this post on Zulip Luca Gerolla (Jul 24 2018 at 22:00):

Should be equivalent to the "canonical" product topology you defined, but don't know if that easy to prove :/

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 22:36):

In maths this says "define a topology on α×β\alpha\times\beta to be the smallest topology such that the following sets are all open: first all the U×βU\times\beta for UαU\subseteq\alpha open, and second all the α×V\alpha\times V for VβV\subseteq\beta open."

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 22:41):

The reason it says this is that the induced topology on α×β\alpha\times\beta coming from the projection down to α\alpha that's what prod.fst is) is precisely the one where the open sets are pre-images of opens in α\alpha.

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 22:43):

And the reason that this is the product topology is first that all those sets are open in the product topology, and conversely that in any topology where these sets are all open, the intersection of two such sets is open, and that's precisely U×VU\times V, so any such topology will contain all the sets which are open in the product topology.


Last updated: May 18 2021 at 07:19 UTC