SecondCountableTopology for WithTop

Stream: Is there code for X?

[Rémy Degenne]

I am putting the order topology on WithTop (in a scope) and I would like to prove that it is second-countable when the order topology on the original type is second-countable.
That is, I want the sorry in the code block below. If someone knows better than me how to use those objects and can come up with a proof that would be great!
The sorry is followed by a bunch of defs/lemmas about the topology that are mostly copied from the ENNReal case and that I am leaving there in case they are useful for the proof. The SecondCountableTopology instance for ENNReal is proved through an argument that is specific for that type (and would not work for ENat for example).

import Mathlib

open Filter Order TopologicalSpace
open scoped Topology

namespace WithTopOrderTopology

variable {ι : Type*} [Preorder ι]

scoped instance : TopologicalSpace (WithTop ι) := Preorder.topology _

scoped instance : OrderTopology (WithTop ι) := ⟨rfl⟩

scoped instance [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] :
    SecondCountableTopology (WithTop ι) := by
  sorry -- THE SORRY IS HERE ---------------------------------------------

end WithTopOrderTopology

namespace WithTop

open scoped WithTopOrderTopology

variable {ι : Type*}

noncomputable
abbrev ut [Nonempty ι] : WithTop ι → ι := WithTop.untopD (Classical.arbitrary ι)

variable [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι]

lemma isEmbedding_coe : Topology.IsEmbedding ((↑) : ι → WithTop ι) := by
  refine WithTop.coe_strictMono.isEmbedding_of_ordConnected ?_
  rw [WithTop.range_coe]
  exact Set.ordConnected_Iio

lemma isOpenEmbedding_coe : Topology.IsOpenEmbedding ((↑) : ι → WithTop ι) :=
  ⟨isEmbedding_coe, by rw [WithTop.range_coe]; exact isOpen_Iio⟩

lemma nhds_coe {r : ι} : 𝓝 (r : WithTop ι) = (𝓝 r).map (↑) :=
  (isOpenEmbedding_coe.map_nhds_eq r).symm

lemma tendsto_ut [Nonempty ι] {a : WithTop ι} (ha : a ≠ ⊤) :
    Tendsto WithTop.ut (𝓝 a) (𝓝 a.ut) := by
  lift a to ι using ha
  rw [nhds_coe, tendsto_map'_iff]
  exact tendsto_id

lemma continuousOn_ut [Nonempty ι] : ContinuousOn WithTop.ut { a : WithTop ι | a ≠ ⊤ } :=
  fun _a ha ↦ ContinuousAt.continuousWithinAt (WithTop.tendsto_ut ha)

@[fun_prop]
lemma continuous_coe : Continuous ((↑) : ι → WithTop ι) :=
  isEmbedding_coe.continuous

variable (ι) in
noncomputable
def neTopEquiv [Nonempty ι] : { a : WithTop ι | a ≠ ⊤ } ≃ ι where
  toFun x := WithTop.ut x
  invFun x := ⟨x, WithTop.coe_ne_top⟩
  left_inv := fun x => Subtype.eq <| by
    lift (x : WithTop ι) to ι using x.2 with y
    simp
  right_inv x := by simp

variable (ι) in
noncomputable
def neTopHomeomorph [Nonempty ι] : { a : WithTop ι | a ≠ ⊤ } ≃ₜ ι where
  toEquiv := WithTop.neTopEquiv ι
  continuous_toFun := continuousOn_iff_continuous_restrict.1 continuousOn_ut
  continuous_invFun := continuous_coe.subtype_mk _

variable (ι) in
/-- If `ι` has a top element, then `WithTop ι` is homeomorphic to `ι ⊕ Unit`. -/
noncomputable
def sumHomeomorph [OrderTop ι] : WithTop ι ≃ₜ ι ⊕ Unit where
  toFun x := if h : x = ⊤ then Sum.inr () else Sum.inl x.ut
  invFun x := match x with
    | Sum.inl i => (i : WithTop ι)
    | Sum.inr () => ⊤
  left_inv x := by cases x <;> simp
  right_inv x := by cases x <;> simp
  continuous_toFun := by
    have h_fr : frontier ({⊤} : Set (WithTop ι)) = ∅ := by
      simp only [frontier, Set.finite_singleton, Set.Finite.isClosed, IsClosed.closure_eq]
      suffices interior ({⊤} : Set (WithTop ι)) = {⊤} by simp [this]
      rw [interior_eq_iff_isOpen]
      have : {⊤} = Set.Ioi ((⊤ : ι) : WithTop ι) := by ext; simp
      rw [this]
      exact isOpen_Ioi
    refine continuous_if' (by simp [h_fr]) (by simp [h_fr]) (by simp) ?_
    exact Continuous.comp_continuousOn (by fun_prop) continuousOn_ut
  continuous_invFun := continuous_sum_dom.mpr ⟨by fun_prop, by fun_prop⟩

end WithTop

The context for that is that I am refactoring the Mathlib definition of stopping times to allow them to be infinite. Thus I need a topology and the Borel sigma-algebra on the WithTop type.

[Yaël Dillies]

Looks fun, but I don't have time today. Mind asking again on friday? ...unless someone scoops me of course :grinning:

[Aaron Liu]

This sounds fun

[Sébastien Gouëzel]

I'm working on it.

[Sébastien Gouëzel]

Here it is. First half:

import Mathlib

open Filter Order TopologicalSpace Set
open scoped Topology

namespace TopologicalSpace

/-- In a second countable topological space, any open set is a countable union of elements in a
given topological basis. -/
lemma IsTopologicalBasis.exists_countable_biUnion_of_isOpen
    {α : Type*} [TopologicalSpace α] [SecondCountableTopology α] {t : Set (Set α)}
    (ht : IsTopologicalBasis t) {u : Set α} (hu : IsOpen u) :
    ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a := by
  have A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u :=
    fun x hx ↦ ht.exists_subset_of_mem_open hx hu
  choose! a hat xa au using A
  obtain ⟨T, T_count, hT⟩ : ∃ T : Set u, T.Countable ∧ ⋃ i ∈ T, a i = ⋃ (i : u), a i := by
    apply isOpen_iUnion_countable _
    rintro ⟨x, hx⟩
    exact ht.isOpen (hat x hx)
  refine ⟨(fun (x : u) ↦ a x) '' T, ?_, T_count.image _, ?_⟩
  · simp only [image_subset_iff]
    rintro ⟨x, xu⟩ -
    exact hat x xu
  rw [biUnion_image, hT]
  apply Subset.antisymm
  · intro x hx
    simp
    grind
  · simp
    grind

/-- In a second countable topological space, any topological basis contains a countable subset
which is also a topological basis. -/
lemma IsTopologicalBasis.exists_countable
    {α : Type*} [TopologicalSpace α] [SecondCountableTopology α] {t : Set (Set α)}
    (ht : IsTopologicalBasis t) :
    ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s := by
  have A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a :=
    fun u hu ↦ ht.exists_countable_biUnion_of_isOpen ((isBasis_countableBasis α).isOpen hu)
  choose! s hst s_count hs using A
  refine ⟨⋃ u ∈ countableBasis α, s u, by simpa using hst,
    (countable_countableBasis α).biUnion s_count, ?_⟩
  apply isTopologicalBasis_of_isOpen_of_nhds
  · simp only [mem_iUnion, exists_prop, forall_exists_index, and_imp]
    have := @ht.isOpen
    grind
  · intro x v hx hv
    simp only [mem_iUnion, exists_prop]
    obtain ⟨u, u_mem, xu, uv⟩ : ∃ u ∈ countableBasis α, x ∈ u ∧ u ⊆ v :=
      (isBasis_countableBasis α).isOpen_iff.1 hv _ hx
    have : x ∈ ⋃ a ∈ s u, a := by
      convert xu
      exact (hs u u_mem).symm
    obtain ⟨w, ws, xw⟩ : ∃ w ∈ s u, x ∈ w := by simpa using this
    refine ⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩
    apply Subset.trans (Subset.trans _ (hs u u_mem).symm.subset) uv
    exact subset_iUnion₂_of_subset w ws fun ⦃a⦄ a ↦ a

/-- In a second countable topological space, any family generating the topology admits a
countable generating subfamily. -/
lemma exists_countable_of_generateFrom
    {α : Type*} [ts : TopologicalSpace α] [SecondCountableTopology α] {t : Set (Set α)}
    (ht : ts = generateFrom t) :
    ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s := by
  let t' := (fun f => ⋂₀ f) '' { f : Set (Set α) | f.Finite ∧ f ⊆ t }
  have : IsTopologicalBasis t' := TopologicalSpace.isTopologicalBasis_of_subbasis ht
  obtain ⟨s', s't', s'_count, hs'⟩ : ∃ s' ⊆ t', s'.Countable ∧ IsTopologicalBasis s' :=
    this.exists_countable
  have A : ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u :=
    fun u hu ↦ by simpa [t', and_assoc] using s't' hu
  choose! f f_fin ft hf using A
  refine ⟨⋃ u ∈ s', f u, by simpa using ft, ?_, ?_⟩
  · apply s'_count.biUnion
    intro u hu
    exact Finite.countable (f_fin u hu)
  · apply le_antisymm
    · apply le_generateFrom_iff_subset_isOpen.2
      simp only [iUnion_subset_iff]
      intro u hu v hv
      rw [ht]
      apply isOpen_generateFrom_of_mem
      exact ft u hu hv
    · rw [hs'.eq_generateFrom]
      apply le_generateFrom_iff_subset_isOpen.2
      intro u hu
      rw [← hf u hu, sInter_eq_biInter]
      change IsOpen[generateFrom _] (⋂ i ∈ f u, i)
      apply @Finite.isOpen_biInter _ _ (generateFrom (⋃ u ∈ s', f u)) _ _
      · apply f_fin u hu
      · intro i hi
        apply isOpen_generateFrom_of_mem
        simp
        grind

end TopologicalSpace

[Sébastien Gouëzel]

Second half:

namespace WithTopOrderTopology

variable {ι : Type*} [Preorder ι]

theorem isOpen_Ioi' [TopologicalSpace ι] [ht : OrderTopology ι] (a : ι) : IsOpen (Ioi a) := by
  rw [ht.topology_eq_generate_intervals]
  apply isOpen_generateFrom_of_mem
  simp
  grind

theorem isOpen_Iio' [TopologicalSpace ι] [ht : OrderTopology ι] (a : ι) : IsOpen (Iio a) := by
  rw [ht.topology_eq_generate_intervals]
  apply isOpen_generateFrom_of_mem
  simp
  grind

instance [TopologicalSpace ι] [OrderTopology ι] : TopologicalSpace (WithTop ι) :=
  Preorder.topology _

instance [TopologicalSpace ι] [OrderTopology ι] : OrderTopology (WithTop ι) := ⟨rfl⟩

[Sébastien Gouëzel]

Third half:

scoped instance [ts : TopologicalSpace ι] [ht : OrderTopology ι] [SecondCountableTopology ι] :
    SecondCountableTopology (WithTop ι) := by
  classical
  rcases isEmpty_or_nonempty ι with hι | ⟨⟨x₀⟩⟩
  · infer_instance
  /- Let `c` be a countable set in `ι` such that the topology is generated by the sets `Iio a`
  and `Ioi a` for `a ∈ c`, by second-countability. Let `c'` be a dense set in `ι`, again by
  second-countability. Let `d` in `WithTop ι` be obtained from `c ∪ c'`, by adding `⊤` and a point
  `x₁ : ι` with `Ioi x₁ = ∅` if there is one.
  We will show that the topology on `WithTop ι` is generated by the intervals `Iio a` and `Ioi a`
  for `a ∈ d`, which will conclude the proof by countability of `d`. -/
  obtain ⟨c, c_count, hc⟩ : ∃ (c : Set ι), c.Countable ∧
      ts = generateFrom { s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a } :=
    exists_countable_generateFrom_Ioi_Iio ι
  obtain ⟨c', c'_count, hc'⟩ : ∃ c' : Set ι, c'.Countable ∧ Dense c' :=
    SeparableSpace.exists_countable_dense
  let x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
  let d : Set (WithTop ι) := (↑)'' c ∪ (↑)'' c' ∪ {⊤} ∪ {(x₁ : WithTop ι)}
  suffices H : instTopologicalSpaceWithTopOfOrderTopology
      = generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} by
    refine ⟨{s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}, ?_, by rw [← H]⟩
    have d_count : d.Countable :=
      (((c_count.image _).union (c'_count.image _)).union (by simp)).union (by simp)
    have : {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d := by
      ext; simp; grind
    rw [this]
    exact (d_count.image _).union (d_count.image _)
  -- We should check the easy direction that all the elements in our generating set are open.
  -- This is trivial as these are all intervals.
  apply le_antisymm
  · apply le_generateFrom_iff_subset_isOpen.2
    simp only [setOf_subset_setOf, forall_exists_index, and_imp]
    grind [isOpen_Iio', isOpen_Ioi']
  /- Now, let us check that our sets indeed generates the topology. As the topology is
  generated by the open half-infinite intervals by definition, we should check that open
  half-infinite intervals are covered by finite intersections of our sets. -/
  let basis : Set (Set ι) := {s | ∃ (f g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite
      ∧ s = (⋂ a ∈ f, Ioi a) ∩ (⋂ a ∈ g, Iio a)}
  have h_basis : IsTopologicalBasis basis := isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom c hc
  rw [OrderTopology.topology_eq_generate_intervals (α := WithTop ι)]
  apply le_generateFrom_iff_subset_isOpen.2
  simp only [setOf_subset_setOf, forall_exists_index]
  rintro u a (rfl | rfl)
  -- Consider an interval of the form `Ioi a`. We should cover it by finite intersections of
  -- our sets.
  · induction a with
    | top =>
      -- for `a = ⊤`, this is trivial as `Ioi ⊤` is in our set by design
      apply isOpen_generateFrom_of_mem
      exact ⟨⊤, by simp [d]⟩
    | coe a =>
      -- for `a : ι`, we consider an element `b ∈ Ioi a`, and seek a finite intersection of our
      -- sets containing it and contained in `Ioi a`.
      rw [@isOpen_iff_forall_mem_open]
      intro b hb
      induction b with
      | top =>
        -- if `b = ⊤`, then either `Ioi a` is empty in `ι` and then we use `Ioi (↑x₁)` which is
        -- in our set and reduced to `⊤`
        rcases eq_empty_or_nonempty (Ioi a) with ha | ha
        · refine ⟨Ioi x₁, ?_, ?_, by simp⟩
          · have : Ioi x₁ = ∅ := by
              have h : ∃ x, Ioi x = ∅ := ⟨a, ha⟩
              simp only [x₁, h, ↓reduceDIte]
              exact h.choose_spec
            simp [WithTop.Ioi_coe, this]
          · apply isOpen_generateFrom_of_mem
            simp [d]
        -- If `Ioi a` is not empty in `ι`, it contains a point `b` in the dense set `c'`, and then
        -- we use `Ioi (↑b)` which is in our set, contained in `Ioi (↑a)` and contains `⊤`.
        · obtain ⟨b, bc', hb⟩ : ∃ b ∈ c', b ∈ Ioi a := hc'.exists_mem_open (isOpen_Ioi' a) ha
          refine ⟨Ioi b, ?_, ?_, by simp⟩
          · apply Ioi_subset_Ioi
            simpa using hb.le
          · apply isOpen_generateFrom_of_mem
            exact ⟨b, by simp [d, bc'], Or.inl rfl⟩
      | coe b =>
        -- if `b` comes from `ι`, then in `ι` we can find a finite intersection of our sets
        -- containing `b` and contained in `Ioi a`. We lift it to `WithTop ι`.
        simp only [mem_Ioi, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Ioi a := h_basis.isOpen_iff.1 (isOpen_Ioi' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ ⋂ z ∈ g, Iio z, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp
          | coe w =>
            simp only [mem_Ioi, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              simp [d]
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              simp [d]
              grind
  -- Consider an interval of the form `Iio a`. We should cover it by finite intersections of
  -- our sets.
  · induction a with
    | top =>
      -- for `a = ⊤`, this is trivial as `Iio ⊤` is in our set by design
      apply isOpen_generateFrom_of_mem
      exact ⟨⊤, by simp [d]⟩
    | coe a =>
      -- for `a : ι`, we consider an element `b ∈ Iio a`, and seek a finite intersection of our
      -- sets containing it and contained in `Iio a`.
      rw [@isOpen_iff_forall_mem_open]
      intro b hb
      induction b with
      | top => simp at hb
      | coe b =>
        -- `b` can not be equal to `⊤`, so it comes from `ι`. In `ι` we can find a finite
        -- intersection of our sets containing `b` and contained in `Iio a`. We lift it
        -- to `WithTop ι`, and intersect with `Iio ⊤` (which is also in our set) to exclude `⊤`.
        simp only [mem_Iio, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a := h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}); swap
          · apply isOpen_generateFrom_of_mem
            simp [d]
          apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              simp [d]
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              simp [d]
              grind

[Sébastien Gouëzel]

(I didn't know there was a length limit on Zulip messages :-)

[Rémy Degenne]

Wow! That was clearly not as straightforward as I thought it would be! Thanks a lot!

[Rémy Degenne]

Do you want to open a PR for the first half? I could then PR the second half with the other topological facts I need on WithTop.

[Rémy Degenne]

Or if you prefer to PR the whole thing, it's fine by me!

[Sébastien Gouëzel]

I am preparing a PR.

[Aaron Liu]

I thought it would be easier than that

[Sébastien Gouëzel]

There are two mathematical difficulties here. The first one is that adding one point can break second-countability. Exercise: construct a nice topological space X which is not second-countable but such that X \ {x} is second-countable, for some point x. The second one is that the challenge was given for preorders, not linear orders, which makes things a little bit more unpleasant. All in all, the maths were less trivial than I expected.

Also, we were missing API, as always :-)

[Aaron Liu]

Sébastien Gouëzel said:

Exercise: construct a nice topological space X which is not second-countable but such that X \ {x} is second-countable, for some point x.

I'm guessing the onepoint compactification of the rationals is not first countable at infinity (thought whether this is a nice space is debatable)

[Sébastien Gouëzel]

I'm not sure what the one point compactification of a non locally compact space is. Depending on the precise definition, I guess it won't be T2 (there shouldn't be disjoint open sets containing 0 and infinity, for instance), so it doesn't count as a nice space in my book :-)

[Aaron Liu]

Sébastien Gouëzel said:

I guess it won't be T2 (there shouldn't be disjoint open sets containing 0 and infinity, for instance), so it doesn't count as a nice space in my book :-)

Take an arbitrary free ultrafilter on Nat, and take its docs#nhdsAdjoint at 0. Then the subspace of nonzero is discrete countable, but nhds 0 is the sup of the free ultrafilter and pure 0, which is not countably generated. This space is T2.

[Sébastien Gouëzel]

#29466. I can split it if it makes reviewing easier, just tell me!

[Sébastien Gouëzel]

Here is a completely elementary example. Take countably many copies of the half-line, i.e., $(0,+\infty) \times \{n\}$ for $n : \mathbb{N}$. Glue them along a new point $0$, by declaring that sets of the form $\bigcup_n [0, \epsilon_n) \times \{n\}$ are open whenever $\epsilon$ is a strictly positive sequence. The glued space is not first countable at $0$, as there are too many open sets around it.

[Aaron Liu]

I thought I tried that and it didn't work

[Aaron Liu]

oh only open quotients of second countable spaces are automatically second countable