Properties of Sierpinski Space

Stream: mathlib4

[finegeometer]

Hi,

Mathlib defines the Sierpinski topology on Prop. But this topology has a number of nice properties, which don't seem to be implemented. Specifically:

• Conjunction and disjunction are continuous.
• A space is discrete iff the equality map X × X → Prop is continuous.
• A space is Hausdorff iff the inequality map X × X → Prop is continuous.
• A space is compact iff the universal quantifier C(X, Prop) → Prop is continuous.
• The existential quantifier C(X, Prop) → Prop is always continuous.

(Those last two require defining the natural topology on spaces of continuous functions. Unless I missed something, that doesn't seem to be implemented either.)

Should these things be added to Mathlib? If so, here's some code to get started. It implements the theorems, but I imagine it will need some sort of modification to fit nicely into Mathlib.

-- Inspired by this paper: https://martinescardo.github.io/papers/entcs87.pdf
-- But I proved the theorems myself.

import Mathlib.Topology.Separation.Basic
import Mathlib.Topology.ContinuousMap.Basic
--------------------------------------------------------------------------------
-- Natural topology on a function space.
--------------------------------------------------------------------------------
-- Will need to be renamed appropriately.
def uncurry' [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(X × Y, Z)) (a : X) : C(Y, Z) where
  toFun := fun b => g (a,b)

instance {X : Type u₁} {Y : Type u₂} [TopologicalSpace X] [TopologicalSpace Y] : TopologicalSpace C(X,Y) where
  -- Is this the correct universe level?
  IsOpen U := ∀ (A : Type u₁) [TopologicalSpace A] (g : C(A × X, Y)), IsOpen (uncurry' g ⁻¹' U)
  isOpen_univ := by simp
  isOpen_inter U₁ U₂ hU₁ hU₂ A inst g := by
    rw [Set.preimage_inter]
    exact (hU₁ A g).inter (hU₂ A g)
  isOpen_sUnion Us hUs A inst g := by
    rw [Set.preimage_sUnion]
    apply isOpen_biUnion
    exact fun U hU => hUs U hU A g

-- Will need to be renamed appropriately.
def uncurry [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(X × Y, Z)) : C(X, C(Y, Z)) where
  toFun := uncurry' g
  continuous_toFun.isOpen_preimage _ h := h X g
--------------------------------------------------------------------------------
-- Lemmas to make things easier later.
--------------------------------------------------------------------------------

theorem discrete_iff_isOpen_diagonal [TopologicalSpace X] : DiscreteTopology X ↔ IsOpen (Set.diagonal X) := by
  constructor
  · intro; apply isOpen_discrete
  · intro h; rw [isOpen_prod_iff] at h
    constructor; apply eq_bot_of_singletons_open
    intro x; specialize h x x rfl
    obtain ⟨U₁,U₂,hU₁,hU₂,hx₁,hx₂,h⟩ := h

    suffices U₁ = {x} by rw [<-this]; exact hU₁
    rw [Set.eq_singleton_iff_unique_mem]
    constructor; exact hx₁
    intro y hy; exact @h (y,x) ⟨hy,hx₂⟩

theorem isClosed_iff_isOpen_compl [TopologicalSpace X] (A : Set X) : IsClosed A ↔ IsOpen Aᶜ := by
  constructor
  · exact fun ⟨h⟩ => h
  · exact fun h => ⟨h⟩

theorem Set.biUnion_setOf (I : Set ι) (P : ι → α → Prop) : ⋃ i ∈ I, {x : α | P i x} = {x : α | ∃ i ∈ I, P i x} := by ext; simp
-- Surely there's already a way to do this, and I just couldn't find it?
theorem isOpen_prod_iff_iUnion_rectangles {X : Type u₁} {Y : Type u₂} [TopologicalSpace X] [TopologicalSpace Y] (A : Set (X × Y)) :
  IsOpen A ↔ ∃ (ι : Type (max u₁ u₂)) (U : ι → Set X) (V : ι → Set Y), (∀ i, IsOpen (U i)) ∧ (∀ i, IsOpen (V i)) ∧ A = ⋃ i : ι, U i ×ˢ V i
:= by
  constructor
  · intro h

    rw [isOpen_prod_iff] at h
    have: ∀ a : A, ∃ U V, IsOpen U ∧ IsOpen V ∧ ↑a ∈ U ×ˢ V ∧ U ×ˢ V ⊆ A := by
      rw [Subtype.forall]
      intro ⟨x,y⟩ hxy; specialize h x y hxy
      obtain ⟨U,V,hU,hV,hx,hy,h⟩ := h; exists U,V
    clear h

    obtain ⟨f,this⟩ := Classical.axiomOfChoice this
    obtain ⟨g,h⟩ := Classical.axiomOfChoice this
    clear this; clear this

    exists A, f, g
    constructor
    · exact fun i => (h i).1
    constructor
    · exact fun i => (h i).2.1
    ext a
    rw [Set.mem_iUnion]
    constructor
    · intro ha; exists ⟨a, ha⟩; simp [h ⟨a, ha⟩]
    · exact fun ⟨i, hi⟩ => (h i).2.2.2 hi

  · intro ⟨ι,U,V,hU,hV,eq⟩; cases eq
    apply isOpen_iUnion; intro i
    apply IsOpen.prod (hU i) (hV i)
--------------------------------------------------------------------------------
-- Properties of the Sierpinski space
--------------------------------------------------------------------------------

@[continuity]
theorem continuous_and : Continuous fun (P,Q) => P ∧ Q := by
  have:= (continuous_fst.isOpen_preimage {True} isOpen_singleton_true).inter (continuous_snd.isOpen_preimage {True} isOpen_singleton_true)
  rw [isOpen_iff_continuous_mem] at this
  simp only [Set.preimage_singleton_true, Set.mem_inter_iff, Set.mem_setOf_eq] at this
  exact this

@[continuity]
theorem continuous_or : Continuous fun (P,Q) => P ∨ Q := by
  have:= (continuous_fst.isOpen_preimage {True} isOpen_singleton_true).union (continuous_snd.isOpen_preimage {True} isOpen_singleton_true)
  rw [isOpen_iff_continuous_mem] at this
  simp only [Set.preimage_singleton_true, Set.mem_union, Set.mem_setOf_eq] at this
  exact this

theorem discrete_iff_continuous_eq [TopologicalSpace X] : DiscreteTopology X ↔ Continuous fun (x,y) => (x : X) = y := by
  rw [discrete_iff_isOpen_diagonal, isOpen_iff_continuous_mem]; simp

theorem hausdorff_iff_continuous_neq [TopologicalSpace X] : T2Space X ↔ Continuous fun (x,y) => (x : X) ≠ y := by
  rw [t2_iff_isClosed_diagonal, isClosed_iff_isOpen_compl, isOpen_iff_continuous_mem]; simp

theorem continuous_exists [TopologicalSpace X] (A : Set X) : Continuous fun f : C(X, Prop) => ∃ x ∈ A, f x := by
  suffices IsOpen {f : C(X, Prop) | ∃ x ∈ A, f x} by rw [isOpen_iff_continuous_mem] at this; exact this
  intro W inst g
  change IsOpen {a | ∃ x ∈ A, (uncurry' g a) x}
  rw [<-Set.biUnion_setOf]
  apply isOpen_biUnion
  intro x hx
  rw [isOpen_iff_continuous_mem]
  exact g.continuous_toFun.comp (Continuous.Prod.mk_left x)

theorem compact_iff_continuous_forall {X : Type u} [TopologicalSpace X] (A : Set X) : IsCompact A ↔ Continuous fun f : C(X, Prop) => ∀ x ∈ A, f x := by
  symm
  calc Continuous fun f : C(X, Prop) => ∀ x ∈ A, f x
    _ = Continuous fun f : C(X, Prop) => f ∈ {f | ∀ x ∈ A, f x} := rfl
    _ = IsOpen {f : C(X, Prop) | ∀ x ∈ A, f x} := by rw [<-isOpen_iff_continuous_mem]
    _ = ∀ (W : Type u) [TopologicalSpace W] (g : C(W × X, Prop)), IsOpen {a | ∀ x ∈ A, g (a, x)} := rfl
    _ ↔ ∀ (W : Type u) [TopologicalSpace W] (U : Set (W × X)), IsOpen U → IsOpen {w : W | ∀ x ∈ A, (w,x) ∈ U} := by
      constructor
      · intro h W _ U hU; exact h W (ContinuousMap.mk (Set.Mem U) (by rw [isOpen_iff_continuous_mem] at hU; exact hU))
      · intro h W _ g
        specialize h W (g ⁻¹' {True}) (g.continuous_toFun.isOpen_preimage {True} isOpen_singleton_true)
        rw [Set.preimage_singleton_true] at h; exact h
    _ ↔ IsCompact A := by
      constructor
      · intro h
        apply isCompact_of_finite_subcover
        intro ι U hU cover
        change ∀ x ∈ A, x ∈ ⋃ i, U i at cover; simp only [Set.mem_iUnion] at cover

        specialize h
          (ι → Prop)
          (⋃ i : ι, (Set.singleton i).pi (fun _ => {True}) ×ˢ U i)
          (isOpen_iUnion fun i => IsOpen.prod (isOpen_set_pi (Set.finite_singleton i) (fun _ _ => isOpen_singleton_true)) (hU i))
        rw [isOpen_pi_iff] at h
        specialize h (fun _ => True) (by simp only [Set.mem_iUnion, Set.mem_prod, Set.mem_pi, Set.mem_singleton_iff, eq_iff_iff, iff_true, Set.mem_setOf_eq, implies_true, true_and]; exact cover)
        obtain ⟨I,V,hV,h⟩ := h; exists I
        specialize @h (fun i => i ∈ I.toSet) (by intro i hi; simp only; rw [eq_true hi]; exact (hV i hi).2)
        simp only [Set.mem_iUnion, Set.mem_prod, Set.mem_pi, Set.mem_singleton_iff, eq_iff_iff, iff_true, Finset.mem_coe, Set.mem_setOf_eq] at h

        intro x hx; specialize h x hx
        obtain ⟨i,h₁,h₂⟩ := h; simp only [Set.mem_iUnion]; exists i, h₁ i rfl

      · intro h W inst U hU
        rw [isOpen_iff_forall_mem_open]; intro w hw
        simp only [Set.mem_iUnion, Set.mem_prod, Set.mem_setOf_eq] at hw

        rw [isOpen_prod_iff_iUnion_rectangles] at hU
        obtain ⟨ι,U₁,U₂,hU₁,hU₂,eq⟩ := hU; cases eq

        have:= h.elim_finite_subcover (ι := {i : ι // w ∈ U₁ i}) (fun i => U₂ ↑i) (fun i => hU₂ ↑i)
          (by
            intro a ha; specialize hw a ha
            rw [Set.mem_iUnion]; rw [Set.mem_iUnion] at hw
            obtain ⟨i,h₁,h₂⟩ := hw; exact ⟨⟨i,h₁⟩,h₂⟩)
        obtain ⟨I,h⟩ := this

        exists ⋂ i ∈ I, U₁ i
        constructor
        · intro w' hw' a ha
          specialize h ha
          rw [Set.mem_iUnion] at h; obtain ⟨i,h⟩ := h
          rw [Set.mem_iUnion] at h; obtain ⟨hi,h⟩ := h
          rw [Set.mem_iUnion]; exists i; constructor
          · simp only [Set.mem_iInter] at hw'
            exact hw' i hi
          · exact h
        constructor
        · exact isOpen_biInter_finset fun ⟨i,_⟩ _ => hU₁ i
        · exact Set.mem_biInter fun ⟨_,h⟩ _ => h

[Kevin Buzzard]

Just a nit: I don't think there's a "natural topology" on spaces of continuous functions -- topological spaces are not a cartesian closed category. So probably this shouldn't be a global instance.

[Junyan Xu]

If you import Mathlib.Topology.CompactOpen, the space of continuous functions has the compact-open topology.

[finegeometer]

Kevin Buzzard said:

Just a nit: I don't think there's a "natural topology" on spaces of continuous functions -- topological spaces are not a cartesian closed category. So probably this shouldn't be a global instance.

I got the terminology from Lemma 8.2 of this paper. But if you don't think the terminology is appropriate, I'm happy to call it something else.

Junyan Xu said:

If you import Mathlib.Topology.CompactOpen, the space of continuous functions has the compact-open topology.

I don't know enough about this — when is this the same or different from the topology I defined? And if it is different, how do we handle that?

[Junyan Xu]

Mathlib won't allow two different instances (like TopologicalSpace) on the same type, even if they're equal and just not definitionally equal. So you can either make your instance a local instance, or create a type synonym (e.g. NaturalContinuousMap) and put your instance on it instead. Or if you have strong reasons to believe your instance is more natural, you may start a discussion on Zulip to propose changing the default instance to yours.

[Yury G. Kudryashov]

I don't think that we'll change the instance of TopologicalSpace (C(X, Y)). If you want to deal with a different topology, then you can create def ContinuousMapWithMyTopology (X Y : Type*) [...] := C(X, Y) and equip this space with your instance.

[Kyle Miller]

Interesting, section 10 of that paper gives some strong evidence that this is the "right" topology to put onto the set of continuous functions. There are two pieces to this (1) if there is an exponential, then the "natural topology" is the only topology that you could have put on C(X, Y) and (2) given an extension of Top to a category that has exponentials (such as quasi-topological spaces), then the "real part" of the exponential there is C(X, Y) with the "natural topology".

The compact-open topology is the "natural topology" when X is locally compact.

[Yury G. Kudryashov]

Am I right that if we change the instance, then we'll have UniformSpace C(X, Y) only for locally compact X? I don't know how this interacts with other parts of the library.

[Yury G. Kudryashov]

BTW, do you need "locally compact" or "weakly locally compact"?