Don't understand the definition of neighborhoods filter

Stream: maths

[Ching-Tsun Chou]

I'm trying to understand the definition of neighborhoods filter:

https://github.com/leanprover-community/mathlib4/blob/ba7312b5aafeb13465bb9283536208f2158e6150/Mathlib/Topology/Defs/Filter.lean#L119-L123

How can I find the definition of the indexed infinitum used here? It seems to me that to match definition with the comment preceding it, supremum should be used instead of infimum.

Another question is: what does "irreducible_def" mean?

[Ruben Van de Velde]

For the last question, you can think of it as def

[Kevin Buzzard]

If you think of a filter as a "generalised set", then the neighbourhood filter of a point s is the intersection of all the usual open sets containing s. If you think of a filter via its usual implementation as a set of sets, then on the set of sets level you are taking suprema and all of your intuitions are backwards. To talk about a simpler example, if F and G are filters then F <= G in Lean means that all the sets in G are in F. The motivation is that if F=P(S) and G=P(T) are principal filters, then you want F <= G to mean S \subseteq T, so in the sets of sets model you have that a set is in G iff it contains T which implies it contains S which implies it's in F.

[Kevin Buzzard]

import Mathlib.Data.Analysis.Topology

variable (X : Type) [TopologicalSpace X]

open scoped Filter -- to get notation working

def nhds' (x : X) : Filter X :=
  ⨅ s ∈ { s : Set X | x ∈ s ∧ IsOpen s }, 𝓟 s

/-
ctrl-click on the ⨅ symbol (or cmd-click on a mac I think)

Get sent to


/-- Indexed infimum. -/
notation3 "⨅ "(...)", "r:60:(scoped f => iInf f) => r


Deduce that `⨅` is notation for `iInf`.

-/

#check iInf -- ctrl-click on this

/-

def iInf [InfSet α] (s : ι → α) : α :=
  sInf (range s)


So we learn that an `iInf` is something which an `InfSet` has
-/

-- So why are filters an InfSet?
#synth InfSet (Filter X) -- Filter.instInfSet

#check Filter.instInfSet -- ctrl-click on this to see the definition. It uses `Filter.sInf`,
-- so control-click on that to find

/-


protected def sInf (s : Set (Filter α)) : Filter α := sSup (lowerBounds s)


This definition looks like a perfectly normal definition of greatest lower bound, so really
the question is: what is the actual *order* on `Filter X`?
-/

variable (F G : Filter X) in
#check F ≤ G -- ctrl-click on ≤ , discover it's called `LE.le`

#check LE.le -- comes from `LE` class

#synth LE (Filter X) -- Preorder.toLE
#synth Preorder (Filter X) -- PartialOrder.toPreorder
#synth PartialOrder (Filter X) -- Filter.instPartialOrder

#check Filter.instPartialOrder
/-
instance : PartialOrder (Filter α) where
  le f g := ∀ ⦃U : Set α⦄, U ∈ g → U ∈ f
  le_antisymm a b h₁ h₂ := filter_eq <| Subset.antisymm h₂ h₁
  le_refl a := Subset.rfl
  le_trans a b c h₁ h₂ := Subset.trans h₂ h₁
-/

-- Bingo! Indeed `f ≤ g` means `U ∈ g → U ∈ f`

[Ching-Tsun Chou]

@Kevin Buzzard : Thanks for the explanation. I think I found the definition of the partial order on filters:

https://github.com/leanprover-community/mathlib4/blob/ba7312b5aafeb13465bb9283536208f2158e6150/Mathlib/Order/Filter/Defs.lean#L173-L177

As you pointed out, it is backward w.r.t. the usual set inclusion.

[Kevin Buzzard]

Modelling a filter as a set of sets is an implementation detail, and the implementation is misleading when it comes to inequalities. My intuition says that filters are like subsets, indeed subsets are a special case (via principal filters), and a smaller subset should correspond to a smaller filter. But with the implementation as sets of sets, if you focus on how many sets are in your set of sets, this intuition is broken. So it's the implementation leading you astray.

[Ching-Tsun Chou]

Right. Thinking about the principal filters is a good way to figure out the correct ordering direction.

[Kyle Miller]

Filter X is the "pro-completion" of Set X, which roughly means "suppose you restrict yourself to just finite intersections and but still allow infinite unions from Set X — now generate a lattice that allows infinite intersections". The function 𝓟 : Set X -> Filter X is the embedding into the pro-completion.

It's a convenient fact that elements of the pro-completion of Set X can be represented as sets of sets. It turns out that for f : Filter X, then f is determined by the collection of all s : Set X such that f ≤ 𝓟 s, so we may as well represent f as the collection of such s. (This is some sort of Yoneda presheaf thing.)

[Kyle Miller]

I think this gives some idea for why filters are natural for topology: topologies are closed under finite intersections and infinite unions, but if we want to at least abstractly work with infinite intersections, we can use filters rather than sets.

[Kyle Miller]

The neighborhood filter at a point doesn't remember the topology of the whole space, but it knows exactly what constitutes a neighborhood of x: 𝓝 x ≤ 𝓟 s iff s is a neighborhood of x (i.e., if there exists an open set U containing x such that U is a subset of s). docs#mem_nhds_iff

[Patrick Massot]

A lot of this is explained in #mil.

[Ching-Tsun Chou]

I was wrong: it is pointed out in #mil:

In other words, given G H: Filter Y, we have G ≤ H ↔ ∀ V : Set Y, V ∈ H → V ∈ G.

Sorry!