Subspace Topology

Stream: Is there code for X?

[Callum Cassidy-Nolan]

I'm formalizing some questions from an undergraduate class in Topology, in my book the subspace topology is defined like this:

image.png

I was looking around in https://leanprover-community.github.io/mathlib_docs/topology/basic.html, but I didn't see it. Do we have this one?

[Oliver Nash]

Yes, we have this (we have a large amount of point-set topology). See for example docs#is_open_induced_iff

[Oliver Nash]

We should perhaps add reference containing the phrase "subspace topology" to docs#topological_space.induced to make this more discoverable.

[Patrick Massot]

Oliver is right of course, but this may be insufficient information. Callum, you should give us an example statement you want to formalize so that you can see how to use the subspace topology.

[Callum Cassidy-Nolan]

My goal is to prove that

if I have (X, Tx), (Y, Ty),

and having A subset X and B of Y then

the subspace topology on A x B coming from the product topology (X x Y, T),
is the same as the product topology on A x B coming from (X, Tx) and (Y, Ty)

[Johan Commelin]

Do you know how to turn that into a Lean statement? (Without bothering about the proof.)

[Patrick Massot]

This will be very painful to state because it's too concrete. Even comparing the subtype corresponding to a product of two subsets and the product of the two subtype is painful

[Patrick Massot]

I don't even know how to do that subtype thing without looking it up

[Johan Commelin]

Right, so to be more explicit, I think you want to construct a homeo between A × B and A.prod B.

[Callum Cassidy-Nolan]

Johan Commelin said:

Right, so to be more explicit, I think you want to construct a homeo between A × B and A.prod B.

This sounds right , but we haven't really discussed homeo's yet, for the proof of that one I was able to get a proof by showing that the basis which generate each topology were the same. Maybe that would be possible here as well?

[Patrick Massot]

This isn't a topology problem. It's a problem about set and subtype

[Adam Topaz]

To formulate the assertion as you stated it, you would have to do some calculation in the lattice of topologies of $A \times B$, which is possible, but a bit annoying.

[Adam Topaz]

And like Patrick is saying, at some point you would have to identify $A \times B$ with its image (a subset) in $X \times Y$

[Patrick Massot]

You can use

[Patrick Massot]

import topology.constructions

variables {X Y : Type*} [topological_space X] [topological_space Y]{A : set X} {B : set Y}

def foo : A ×ˢ B → A × B :=
λ x, (⟨(x : X × Y).1, x.property.1⟩, ⟨(x : X × Y).2, x.property.2⟩)

[Patrick Massot]

in order to at least compare types

[Callum Cassidy-Nolan]

Patrick Massot said:

This isn't a topology problem. It's a problem about set and subtype

Could you help me understand this problem a little more?

[Adam Topaz]

In your message, you consider $A \times B$ both as a type in itself, constructed as a product of $A$ and $B$, and as a subset of $X \times Y$. In Lean, they are different in the sense that they are terms of different types:

import data.set.prod

variables {X Y : Type*} {A : set X} {B : set Y}

#check (A × B) -- ↥A × ↥B : Type (max u_1 u_2)
#check (A ×ˢ B) -- A ×ˢ B : set (X × Y)

Patrick's code block gives a suggestion for how one would identify them.

[Junyan Xu]

docs#equiv.set.prod is the bijection underlying the homeomorphism .

[Junyan Xu]

and we do have docs#homeomorph.set.prod

[Patrick Massot]

Sorry, I got distracted by my Lean 4 compiling issues. I wanted to say that a more abstract statement would be much easier to state and prove.

import topology.constructions

variables {X Y : Type*} [TX : topological_space X] [TY : topological_space Y]
          {X' Y' : Type*} (f : X' → X) (g : Y' → Y)

open topological_space filter

notation `prod_top` := @prod.topological_space _ _

example : induced (prod.map f g) (prod_top TX TY) = prod_top (induced f TX) (induced g TY):=
begin
  apply eq_of_nhds_eq_nhds,
  rintros ⟨x', y'⟩,
  simp [nhds_prod_eq, nhds_induced, comap_prod, comap_comap, prod.map_fst', prod.map_snd', filter.prod]
end

[Patrick Massot]

Maybe you won't like the proof but at least the statement should make sense.

[Adam Topaz]

Here is an alternative proof of Patrick's lemma that's slightly closer to what I assume you have in mind:

example : induced (prod.map f g) (prod_top TX TY) = prod_top (induced f TX) (induced g TY):=
show induced _ (_ ⊓ _) = _ ⊓ _, by simpa only [induced_inf, induced_compose]

[Adam Topaz]

But this requires knowing ahead of time that the product topology is defined as an inf, so it breaks the API barrier

[Patrick Massot]

My proof also breaks that barrier. But this is unavoidable since it proves a basic foundational property of the product topology.

[Patrick Massot]

This lemma should be in mathlib

[Yury G. Kudryashov]

See docs#homeomorph.set.prod

[Kevin Buzzard]

That was quick!

[Jireh Loreaux]

we've had it, it's not new

[Adam Topaz]

Patrick's lemma is a bit different though

[Yury G. Kudryashov]

It is called docs#inducing.prod_mk and should be renamed to inducing.prod_map

[Adam Topaz]

Ah great!