Smallest neighborhood of a point

Stream: Is there code for X?

[Yaël Dillies]

Do we have the intersection of all neighborhoods of a point as a definition? If not, is there a standard name for it?

[Yaël Dillies]

or neighborhoods of a set, I'm not picky

[Yaël Dillies]

If not, I'll call it exterior for now.

[Eric Rodriguez]

where is this useful?

[Yaël Dillies]

It's useful in the theory of Alexandrov-discrete topological spaces. See #6962. Exactly what I want is

variable {α : Type*} [TopologicalSpace α] {s : Set α}

lemma isOpen_iff_forall_specializes : IsOpen s ↔ ∀ x y, x ⤳ y → y ∈ s → x ∈ s := by
  refine' ⟨λ hs x y hxy ↦ hxy.mem_open hs, λ hs ↦ _⟩
  sorry

[Kevin Buzzard]

There's the concept of a specialization and generalization of a point in a topological space: see e.g. stacks project. Is the intersection of the neighbourhoods of x just the set of generalizations of x?

[Yaël Dillies]

That's more or less what I'm proving, yeah.

[Anatole Dedecker]

(deleted)

[Anatole Dedecker]

I think it’s sometimes called the kernel of a filter, that should be the definition. exterior doesn’t feel like a very good name to me.

[Yaël Dillies]

I currently have

def exterior (s : Set α) : Set α := ⋂₀ {t : Set α | IsOpen t ∧ s ⊆ t}

What's your proposed definition exactly?

[Anatole Dedecker]

The intersection of all elements of a filter. In your case, this would be the kernel of docs#nhdsSet

[Yaël Dillies]

So you would not emphasize the analogy with interior?

[Anatole Dedecker]

In the case of a set that makes more sense (for a point it seemed weird, but you could say that it’s the exterior of a singleton). But for the general concept (for filters) I don’t think it makes sense

[Anatole Dedecker]

Yaël Dillies said:

It's useful in the theory of Alexandrov-discrete topological spaces. See #6962. Exactly what I want is

variable {α : Type*} [TopologicalSpace α] {s : Set α}

lemma isOpen_iff_forall_specializes : IsOpen s ↔ ∀ x y, x ⤳ y → y ∈ s → x ∈ s := by
  refine' ⟨λ hs x y hxy ↦ hxy.mem_open hs, λ hs ↦ _⟩
  sorry

By the way, this is false right? Or do you have additional assumptions?

[Yaël Dillies]

Of course I forgot to include AlexandrovDiscrete α :sweat_smile:

[Anatole Dedecker]

Aaaaah okay, in that case I understand why exterior is better (since it’s actually open). I think ultimately we will want the general filter definition, but as a temporary def or abbreviation exterior is fine.

[Yaël Dillies]

So this is the world you want to live in?

namespace Filter
variable {α : Type*}

def ker (f : Filter α) : Set α := ⋂ s ∈ f, s

-- Insert delightful Yaël API here

end Filter

variable {α : Type*} [TopologicalSpace α] {s : Set α} {x y : α}
open scoped Topology

def exterior (s : Set α) : Set α := (𝓝ˢ s).ker

lemma specializes_iff_exterior_subset : x ⤳ y ↔ exterior {x} ⊆ exterior {y} := sorry

[Anatole Dedecker]

Yes, although in the case of a point I’m not sure if the normal form should be exterior {x} or (nhds x).ker

[Johan Commelin]

The specialization order exists in mathlib.

[Johan Commelin]

Let me try to find it.

[Yaël Dillies]

Johan, I know, but it's defined with closure {y} ⊆ closure {x}. There's still something to be proven!

[Johan Commelin]

Mathlib/Topology/Inseparable.lean
62:def Specializes (x y : X) : Prop := 𝓝 x ≤ 𝓝 y

[Johan Commelin]

I'm not claiming that there's nothing to be proven :grinning:

[Yaël Dillies]

Here's a sneak peak of where I'm at:

def topToPreord : TopCat ⥤ PreordCat := sorry

def alexDiscEquivPreord : AlexDisc ≌ PreordCat := sorry