from "exists" to sets

Stream: maths

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

@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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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