Zulip Chat Archive

Stream: maths

Topic: from "exists" to sets


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jul 16 2020 at 12:35):

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

view this post on Zulip Reid Barton (Jul 16 2020 at 12:35):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 16 2020 at 17:01):

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

view this post on Zulip 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