Defining the Particular Point Topology

Stream: new members

[Luigi Massacci]

So a per the title, I defined the Particular point topology on a type (I recall someone was looking for it and also there was a discussion about adding the Sierpinksi space to Counterexamples), so here it is. I have a couple questions though:

a) I'm very confused by the whole typeclass (eg: DiscreTeopology, OrderTopology) vs type alias (CofiniteTopology) approach to "generic" topologies. When is one favoured over the other? I went with the latter since this seems closer in spirit to CofiniteTopology, but I don't really get why there's this distinction.
b) Is there any way to improve the definition? That p : X hanging there is a bit ugly but I couldn't find a better way.

import Mathlib.Tactic
import Mathlib.Topology.Filter
import Mathlib.Topology.Order

open Topology TopologicalSpace Set Function Classical Filter

/-- A type synonym equipped with the topology whose open sets are the empty set
and the sets containing a specified point -/
def ParticularPointTopology (X : Type*) (p : X) := X

namespace ParticularPointTopology

instance {X : Type*} (p : X) : Inhabited (ParticularPointTopology X p) where
  default := p

def of : X ≃ ParticularPointTopology X p:=
  Equiv.refl X

variable {X : Type*} (p : X)

instance : TopologicalSpace (ParticularPointTopology X p) where
  IsOpen s := s.Nonempty → p ∈ s
  isOpen_univ := by simp only [univ_nonempty, mem_univ, forall_true_left]
  isOpen_inter s t := by
    rintro hs ht ⟨x, hxs, hxt⟩
    exact ⟨hs ⟨x, hxs⟩, ht ⟨x, hxt⟩⟩
  isOpen_sUnion := by
    rintro s h ⟨x, t, hts, hxt⟩
    exact mem_sUnion_of_mem (h t hts ⟨x, hxt⟩) hts

theorem isOpen_iff {s : Set (ParticularPointTopology X p)} : IsOpen s ↔ s.Nonempty → p ∈ s :=
  Iff.rfl

theorem isOpen_iff' {s : Set (ParticularPointTopology X p)} : IsOpen s ↔ s = ∅ ∨ p ∈ s := by
  simp only [isOpen_iff, nonempty_iff_ne_empty, or_iff_not_imp_left]

theorem isClosed_iff {s : Set (ParticularPointTopology X p)} : IsClosed s ↔ s = univ ∨ p ∉ s := by
  simp only [← isOpen_compl_iff, isOpen_iff', compl_empty_iff, mem_compl_iff]

theorem nhds_eq (a : (ParticularPointTopology X p)) : 𝓝 a = 𝓟 {a, p} := by
  ext x
  simp [_root_.mem_nhds_iff, isOpen_iff]
  constructor
  intro ⟨t, htx, htp, hta⟩
  refine insert_subset (htx hta) (singleton_subset_iff.mpr (htx (htp (nonempty_of_mem hta))))
  refine fun h ↦ ⟨{a, p}, h, fun _ ↦ mem_insert_of_mem a rfl, mem_insert a {p}⟩

theorem mem_nhds_iff {a : (ParticularPointTopology X p)} {s : Set (ParticularPointTopology X p)} :
    s ∈ 𝓝 a ↔ a ∈ s ∧ p ∈ s := by
    simp [nhds_eq]
    constructor
    refine fun h ↦ ⟨h <| mem_insert a {p}, h <| mem_insert_of_mem a rfl⟩
    rintro ⟨as, ps⟩ x (hx | hx) <;> (rw [hx]; assumption)

theorem empty_interior_of_closed {s : Set (ParticularPointTopology X p)} (hs : IsClosed s) (huniv : s ≠ univ)
  : interior s = ∅ := by
  simp only [isClosed_iff] at hs
  rcases hs with h | h
  · contradiction
  · have : p ∉ interior s := not_mem_subset interior_subset h
    rcases (@isOpen_iff' _ _ (interior s)).mp <| isOpen_interior
    · assumption
    · contradiction

instance : T0Space (ParticularPointTopology X p) where
  t0 x y h:= by
    have : y ∈ {x, p} ∧ p ∈ {x, p} := by
      rw [← (@mem_nhds_iff _ _ _ {x, p}), ← h]; simp [nhds_eq, subset_refl]
    have : x ∈ {y, p} ∧ p ∈ {y, p} := by
      rw [← (@mem_nhds_iff _ _ _ {y, p}), h]; simp [nhds_eq, subset_refl]
    aesop

instance : SeparableSpace (ParticularPointTopology X p) where
  exists_countable_dense := by
    refine ⟨{p}, countable_singleton p, dense_iff_inter_open.mpr ?_⟩
    refine fun U h₁ h₂ ↦ inter_singleton_nonempty.mpr <| ((isOpen_iff _).mp h₁ h₂)

instance : FirstCountableTopology (ParticularPointTopology X p) where
  nhds_generated_countable := by
    refine fun a ↦ ⟨{{a, p}}, ?_⟩
    simp only [countable_singleton, nhds_eq, generate_singleton, and_self]

end ParticularPointTopology

[Ruben Van de Velde]

Certainly that Inhabited instance will never be used, because the p argument cannot be found. Maybe you want to provide it under the assumption that X itself is inhabited?

[Yaël Dillies]

a. The best is to have both. Eg check docs#Topology.IsScott and docs#Topology.WithScott

[Luigi Massacci]

@Yaël Dillies thank you. @Ruben Van de Velde, that seems very reasonable but are you suggesting adding [Inhabited X] to the variable {X : Type*} … declaration, adding it as an hypothesis to def ParticularPointTopology or providing just the instance Inhabited (ParticularPointTopology X p) under the assumption [Inhabited X]? I guess eliminating it altogether might also be a viable option

[Junyan Xu]

Certainly that Inhabited instance will never be used, because the p argument cannot be found. Maybe you want to provide it under the assumption that X itself is inhabited?

ParticularPointTopology X p depends on p so Lean should be able to unify and find p. If it can't it will warn you once you write the instance ...

[Luigi Massacci]

I'm resurrecting this thread since I got around to finishing things. At the the I had the type synonym working, and as an mwe this was the state of things.

import Mathlib.Tactic
import Mathlib.Topology.Filter
import Mathlib.Topology.Order

open Topology TopologicalSpace Set Function Classical Filter

/-- A type synonym equipped with the topology whose open sets are the empty set
and the sets containing a specified point -/

def ParticularPoint (X : Type*) (p : X) := X

namespace ParticularPoint

def of : X ≃ ParticularPoint X p:=
  Equiv.refl X

variable {X : Type*} (p : X) {s : Set (ParticularPoint X p)} (a : (ParticularPoint X p))

instance : TopologicalSpace (ParticularPoint X p) where
  IsOpen s := s.Nonempty → p ∈ s
  isOpen_univ := by simp only [mem_univ, implies_true]
  isOpen_inter s t := by
    rintro hs ht ⟨x, hxs, hxt⟩
    exact ⟨hs ⟨x, hxs⟩, ht ⟨x, hxt⟩⟩
  isOpen_sUnion := by
    rintro s h ⟨x, t, hts, hxt⟩
    exact mem_sUnion_of_mem (h t hts ⟨x, hxt⟩) hts

theorem isOpen_iff  : IsOpen s ↔ s.Nonempty → p ∈ s :=
  Iff.rfl

theorem nhds_eq : 𝓝 a = 𝓟 {a, p} := by
  ext u
  simp [_root_.mem_nhds_iff, isOpen_iff]
  constructor
  intro ⟨t, htu, htp, hta⟩
  refine insert_subset (htu hta) (singleton_subset_iff.mpr (htu (htp (nonempty_of_mem hta))))
  refine fun h ↦ ⟨{a, p}, h, fun _ ↦ mem_insert_of_mem a rfl, mem_insert a {p}⟩

theorem mem_nhds_iff :
    s ∈ 𝓝 a ↔ a ∈ s ∧ p ∈ s := by
    simp [nhds_eq]
    constructor
    refine fun h ↦ ⟨h <| mem_insert a {p}, h <| mem_insert_of_mem a rfl⟩
    rintro ⟨as, ps⟩ x (hx | hx) <;> (rw [hx]; assumption)

instance : T0Space (ParticularPoint X p) where
  t0 x y h:= by
    have : y ∈ {x, p} ∧ p ∈ {x, p} := by
      rw [← (@mem_nhds_iff _ _ {x, p}), ← h]; simp [nhds_eq, subset_refl]
    have : x ∈ {y, p} ∧ p ∈ {y, p} := by
      rw [← (@mem_nhds_iff _ _ {y, p}), h]; simp [nhds_eq, subset_refl]
    aesop

I tried to make it into a typeclass instead, but now I run into problems. First, I need to specify p when using the theorems, but I guess that might be unavoidable. (I tried making it implicit and ran into other troubles). But more importantly I run into this error:

cannot find synthesization order for instance @instT0Space with type
  ∀ {X : Type u_2} (p : X) [inst : TopologicalSpace X] [inst_1 : IsParticularPoint X p], T0Space X
all remaining arguments have metavariables:
  @IsParticularPoint X ?p inst✝¹Lean 4

The code mwe is the following:

import Mathlib.Tactic
import Mathlib.Topology.Filter
import Mathlib.Topology.Order

open Topology TopologicalSpace Set Function Classical Filter

section ParticularPoint

/- A nonempty set `s` is open in the Particular Point topology iff
it contains some particular point p -/
def ParticularPoint (X : Type*) (p : X) : TopologicalSpace X where
  IsOpen s := s.Nonempty → p ∈ s
  isOpen_univ := by simp only [mem_univ, implies_true]
  isOpen_inter s t := by
    rintro hs ht ⟨x, hxs, hxt⟩
    exact ⟨hs ⟨x, hxs⟩, ht ⟨x, hxt⟩⟩
  isOpen_sUnion := by
    rintro s h ⟨x, t, hts, hxt⟩
    exact mem_sUnion_of_mem (h t hts ⟨x, hxt⟩) hts

variable (X : Type*) (p : X) [TopologicalSpace X]

/-- Predicate for a topological space to be equipped with the Particular Point Topology for some point. -/
class IsParticularPoint : Prop where
  topology_eq_particularPoint : ‹TopologicalSpace X› = ParticularPoint X p

instance : @IsParticularPoint X p (ParticularPoint X p) :=
  @IsParticularPoint.mk _ _ (ParticularPoint X p) rfl

namespace IsParticularPoint
variable {X: Type*} (p : X) [TopologicalSpace X] [IsParticularPoint X p] {s : Set X}

lemma topology_eq : ‹_› = ParticularPoint X p := topology_eq_particularPoint

lemma isOpen_iff :
    IsOpen s ↔ s.Nonempty → p ∈ s := by erw [@topology_eq X p _]; rfl

theorem nhds_eq (a : X) : 𝓝 a = 𝓟 {a, p} := by
  ext u
  simp [_root_.mem_nhds_iff, isOpen_iff]
  constructor
  intro ⟨t, htu, htp, hta⟩
  refine insert_subset (htu hta) (singleton_subset_iff.mpr (htu ?_))
  exact (isOpen_iff p).mp htp (Set.nonempty_of_mem hta)
  refine fun h ↦ ⟨{a, p}, h, ?_, mem_insert a {p}⟩
  refine (isOpen_iff p).mpr (fun _ ↦ mem_insert_of_mem a rfl)

theorem mem_nhds_iff {a : X} :
    s ∈ 𝓝 a ↔ a ∈ s ∧ p ∈ s := by
    simp [nhds_eq p]
    constructor
    refine fun h ↦ ⟨h <| mem_insert a {p}, h <| mem_insert_of_mem a rfl⟩
    rintro ⟨as, ps⟩ x (hx | hx) <;> (rw [hx]; assumption)

instance : T0Space X where
  t0 x y h:= by
    have : y ∈ {x, p} ∧ p ∈ {x, p} := by
      rw [← (@mem_nhds_iff _ _ _ _ {x, p}), ← h]; simp [nhds_eq p, subset_refl]
    have : x ∈ {y, p} ∧ p ∈ {y, p} := by
      rw [← (@mem_nhds_iff X p _ _ {y, p}), h]; simp [nhds_eq p, subset_refl]
    aesop

end IsParticularPoint
end ParticularPoint

I tried to do it like docs#Topology.IsScott as you suggested @Yaël Dillies but I'm at a bit of a loss as to what exactly the problem is

[Yaël Dillies]

Surely it should be T0Space (ParticularPoint X p) instead of T0Space X?

[Luigi Massacci]

How could that work? In the second example ParticularPoint X p is a of type TopologicalSpace X. I should probably have renamed it in the first one to WithParticularPoint. Anyway I decided to solve the problem by adding the type synonym and then proving the instance on that. However in docs#Topology.IsScott they managed to do that with just the typeclass. Dunno.

I just added the following:

def WithParticularPoint (X : Type*) (p : X) := X

namespace WithParticularPoint

instance : TopologicalSpace (WithParticularPoint X p) := ParticularPoint X p
instance : IsParticularPoint (WithParticularPoint X p) p := ⟨rfl⟩

end WithParticularPoint

open IsParticularPoint

instance : T0Space (WithParticularPoint X p) where
  t0 x y h:= by
    have : y ∈ {x, p} ∧ p ∈ {x, p} := by
      rw [← (@mem_nhds_iff (WithParticularPoint X p) _ _ _ {x, p}), ← h];
      simp [@nhds_eq (WithParticularPoint X p) p, subset_refl]
    have : x ∈ {y, p} ∧ p ∈ {y, p} := by
      rw [← (@mem_nhds_iff (WithParticularPoint X p) _ _ _ {y, p}), h];
      simp [@nhds_eq (WithParticularPoint X p) p, subset_refl]
    aesop


end ParticularPoint

[Luigi Massacci]

Which is guess is kosher enough?

[Yaël Dillies]

Luigi Massacci said:

I decided to solve the problem by adding the type synonym and then proving the instance on that. However in docs#Topology.IsScott they managed to do that with just the typeclass. Dunno.

That's because the Scott topology doesn't require more data than typeclasses can provide. Your "particular topology" does, since p can't be found by typeclass search.

[Luigi Massacci]

That makes sense