# Zulip Chat Archive

## Stream: maths

### Topic: product topology

#### 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}

#### Johan Commelin (Jul 24 2018 at 17:10):

This is already in mathlib. Did you know that?

#### Kevin Buzzard (Jul 24 2018 at 17:16):

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

#### Kevin Buzzard (Jul 24 2018 at 17:17):

because it's expecting a close bracket

#### 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}`

#### 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))

#### Kevin Buzzard (Jul 24 2018 at 17:26):

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

#### 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 (α × β))`

#### 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.

#### 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

#### 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.

#### 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?

#### Luca Gerolla (Jul 24 2018 at 21:56):

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

#### 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₂

#### 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 :/

#### 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\times\beta$ for $U\subseteq\alpha$ open, and second all the $\alpha\times V$ for $V\subseteq\beta$ open."

#### 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$.

#### 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\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