Stream: maths

Topic: from "exists" to sets

Kevin Buzzard (Jul 16 2020 at 12:32):

I was very surprised with how much I had to struggle here. Making topological spaces from first principles for pedagogical reasons. The axiom for infinite unions uses sUnion. When I went to prove that a subset was open iff it was locally open, I really got bogged down with classical.some. I just ran into Jeremy in a breakout room and told him my woes, and he encouraged me to press on. I've done it. The difficulty is that if V is locally open then to create my set of subsets I need to use classical.some, which I always feel is intimidating for beginners. Am I missing a trick? Is there some infrastructure which can help me here?

import tactic

open set

class topological_space (X : Type) :=
(is_open        : set X → Prop)
(is_open_univ   : is_open univ)
(is_open_inter  : ∀ (U V : set X), is_open U → is_open V → is_open (U ∩ V))
(is_open_sUnion : ∀ (𝒞 : set (set X)), (∀U ∈ 𝒞, is_open U) → is_open (⋃₀ 𝒞))

namespace topological_space

variables {X : Type} [topological_space X]

lemma open_iff_locally_open (V : set X) :
is_open V ↔ ∀ x : X, x ∈ V → ∃ U : set X, x ∈ U ∧ is_open U ∧ U ⊆ V :=
begin
split,
{ intro hV,
intros x hx,
use [V, hx, hV] },
{ intro h,
let 𝒞 : set (set X) := {U : set X | ∃ (x : X) (hx : x ∈ V), U = classical.some (h x hx)},
have h𝒞 : ∀ U ∈ 𝒞, ∃ (x : X) (hx : x ∈ V), x ∈ U ∧ is_open U ∧ U ⊆ V,
{ intros U hU,
rcases hU with ⟨x, hx, rfl⟩,
use [x, hx],
exact classical.some_spec (h x hx) },
convert is_open_sUnion 𝒞 _,
{ ext x, split,
{ intro hx,
rw mem_sUnion,
use classical.some (h x hx),
split,
use [x, hx],
have h := classical.some_spec (h x hx),
exact h.1 },
{ intro hx,
rw mem_sUnion at hx,
rcases hx with ⟨U, hU, hxU⟩,
rcases h𝒞 U hU with ⟨_, _, _, _, hUV⟩,
apply hUV,
exact hxU }},
{ intros U hU,
rcases (h𝒞 U hU) with ⟨_, _, _, hU, _⟩,
exact hU },
},
end

end topological_space


Kevin Buzzard (Jul 16 2020 at 12:34):

I guess my question is whether there is a better definition for 𝒞, the set of sets I need to apply is_open_sUnion.

Reid Barton (Jul 16 2020 at 12:35):

The usual "trick" is to take all the sets which could be chosen

Reid Barton (Jul 16 2020 at 12:35):

i.e. here all the sets which are open and contained in V

Reid Barton (Jul 16 2020 at 12:35):

their union is open and contained in V and, by h, contains every point of V, so equals V

Kevin Buzzard (Jul 16 2020 at 14:19):

lemma open_iff_locally_open' (V : set X) :
is_open V ↔ ∀ x : X, x ∈ V → ∃ U : set X, x ∈ U ∧ is_open U ∧ U ⊆ V :=
begin
split,
{ intro hV,
intros x hx,
use [V, hx, hV] },
{ intro h,
let 𝒞 : set (set X) := {U : set X | is_open U ∧ U ⊆ V},
convert is_open_sUnion 𝒞 _,
{ ext x,
split,
{ intro hx,
rcases h x hx with ⟨U, h1, h2, h3⟩,
rw mem_sUnion,
use U,
use [h2, h3, h1] },
{ rw mem_sUnion,
rintro ⟨U, ⟨h, hUV⟩, hxU⟩,
exact hUV hxU }},
{ rintro U ⟨hU, hUV⟩,
exact hU }}
end


Kevin Buzzard (Jul 16 2020 at 16:47):

@Reid Barton can you pull off a similar trick to prove that a compact subspace of a Hausdorff space is closed? The proof I know involves showing that the complement is open, because if C compact, x \notin C is fixed (and we're looking for an open neighbourhood in the complement of C) and y \in C, then we can choose x \in V(y) and y \in W(y) disjoint; the union of the W(y) covers C so there's a finite subcover, and the corresponding finite intersection of the V's is open and disjoint from C. But when I apply Hausdorffness infinitely often I'm using AC.

Reid Barton (Jul 16 2020 at 16:52):

I guess you can look at all those open sets W whose complement contains an open neighborhood of x. This is a cover of C (because for every y in C, there exists blah blah--this doesn't use choice) and then after passing to a finite subcover, you can pick the finitely many open neighborhoods V of x.

Reid Barton (Jul 16 2020 at 16:53):

But maybe more natural is to form the family indexed by all pairs (V, W) where V and W are disjoint open neighborhoods of x and y respectively, which assigns to such a pair W.

Reid Barton (Jul 16 2020 at 16:54):

Sorry, I mean the family of all pairs (V, W) such that V is an open neighborhood of x, and W is an open set disjoint from V.

Reid Barton (Jul 16 2020 at 16:55):

Proving it's a cover of C doesn't require choice, and then from a finite subcover (as in, a finite subset of the indexing set) you directly obtain the Vs

Reid Barton (Jul 16 2020 at 17:01):

I think I might have learned this exact argument from Mario actually.

Kevin Buzzard (Jul 16 2020 at 17:58):

Kenny is at Xena and he told me a version involving y but this is even better :-)

Last updated: May 18 2021 at 08:14 UTC