# Zulip Chat Archive

## Stream: maths

### Topic: fundamental system of neighborhoods

#### Johan Commelin (Oct 04 2018 at 11:24):

Do we have the notion of a *fundamental system of neighborhoods of 0* for topological groups?

#### Kevin Buzzard (Oct 04 2018 at 12:30):

This would be a basis for the filter `nhds 0`

, right? Or are you asking for more?

#### Johan Commelin (Oct 04 2018 at 12:35):

It probably is. I just don't know enough about filters to be sure...

#### Kevin Buzzard (Oct 04 2018 at 12:42):

I read some blog post about filters recently. Here are two examples of filters on a topological space X. Choose x in X. Then (1) the set of all subsets of X containing x is a filter (the principal filter). But much more interesting (2) the set of all subsets V of X such that x is in the interior of V -- this is also a filter. This is the filter of neighbourhoods of x and it comes up a lot. For example one can formalise the notion that a map of topological spaces f:X -> Y is continuous at a point x using this neighbourhood filter (more naive attempts at a definition, such as "pre-image of an open set containing f(x) is open" are hopelessly poorly behaved and wrong; the filter language is perfect for this). If F is a filter and V is in F then any set containing V is also in F, so you could imagine a filter being generated by a subset and the construction basically being that you throw in any set that contains one of your basis sets; if your basis is well-behaved then this will be a filter. I think this is the notion you want. Any V whose interior contains 0 will contain as a subset some element of your fundamental system.

#### Johan Commelin (Oct 04 2018 at 12:46):

Ok, so I want to write `(nhds 0) = "the smallest filter containing {myset}"`

. Is that right?

#### Johan Commelin (Oct 04 2018 at 12:46):

That would mean that `{myset}`

is a fundamental system of neighbourhoods around 0.

#### Kevin Buzzard (Oct 04 2018 at 12:49):

I think that's right. It probably goes something like this (and you could easily check in Lean!) If B is a bunch of subsets of X (maybe B has to be non-empty), and if the intersection of any two elements of B contains an element of B, then I think that the set F of all subsets of X with the property that they contain an element of B, should be a filter. I'm thinking of B as a fund system of nhds of x and `F = nhds x`

. Hopefully someone will correct me if I've missed something.

#### Kevin Buzzard (Oct 04 2018 at 12:51):

I'm pretty sure that arbitrary intersection of filters is a filter, so one can always look at the filter generated by a random collection of subsets of X, but in the basis case it's simpler because you only have to look at sets containing a basis element, rather than sets containing a finite intersection of basis elements. These were just my thoughts after reading the definition, I don't know some reference where this is all treated succinctly and clearly, although I would imagine that there will be one somewhere.

#### Johannes Hölzl (Oct 04 2018 at 12:51):

The smallest filter containing `s`

is `filter.generate s`

(https://github.com/leanprover/mathlib/blob/master/order/filter.lean#L241)

#### Kevin Buzzard (Oct 04 2018 at 12:52):

But it would be easier to prove stuff about the smallest filter containing s if s had some nice properties to start with, because then you wouldn't need all the cases in the inductive definition.

#### Johannes Hölzl (Oct 04 2018 at 12:52):

Note that the order on filter is flipped, i.e. the arbitrary set-intersection of the sets of filters is the supremum on filters.

#### Kevin Buzzard (Oct 04 2018 at 12:54):

Thanks Johannes for that important reminder! I'm sure there's some logic to it but it always makes me very nervous about filters. There is I think both top and bottom filters, but I am always a bit confused about whether the empty set is allowed to be an element of a filter, and whether the empty collection is a filter. Conventions maybe differ in different places?

#### Kevin Buzzard (Oct 04 2018 at 12:54):

In particular I never seem to know what is top and bot :-)

#### Patrick Massot (Oct 04 2018 at 12:56):

#### Johannes Hölzl (Oct 04 2018 at 12:57):

the empty set is not a filter, the filter containing the empty set is the bottom filter

#### Johan Commelin (Oct 04 2018 at 13:00):

@Patrick Massot Why do you ask `pure 0 ≤ Z`

? Why not equality?

#### Johan Commelin (Oct 04 2018 at 13:00):

I've got the very ugly

(filter.generate {U' : set A | ∃ n : pnat, U' = {x | ∃ y : A, y^(n:ℕ) = x}} = (nhds 0))

#### Kevin Buzzard (Oct 04 2018 at 13:00):

Note that if a filter contains the empty set then it contains all sets, and because of this backwards convention this is the one at the bottom

#### Johan Commelin (Oct 04 2018 at 13:00):

I hope that is the same thing as: $\{ U^n | n \ge 1 \}$ forms a neighbourhood basis of `0`

.

#### Johannes Hölzl (Oct 04 2018 at 13:06):

`Z`

is supposed to be the neighborhood filter around `0`

. `Z = pure 0`

would be wrong, it would result in the discrete topology.

#### Johannes Hölzl (Oct 04 2018 at 13:11):

@Johan Commelin there are some rules to work with `generate`

. The best is to use `le_antisymm`

, one side is reduced with `sets_iff_generate `

to the inclusion that all generated elements are neighborhoods. For the other direction it depends on your topology which base element you can select

#### Johan Commelin (Oct 04 2018 at 13:14):

Hmm, I'll have to try and figure out if I can make sense of that.

#### Johan Commelin (Oct 04 2018 at 13:14):

I need to prove

lemma tfae_i_to_ii : (∃ U T : set A, T ⊆ U ∧ set.finite T ∧ (filter.generate {U' : set A | ∃ n : pnat, U' = {x | ∃ y : A, y^(n:ℕ) = x}} = (nhds 0)) ∧ {y : A | ∃ (t ∈ T) (u ∈ U), y = t * u} = {y : A | ∃ (t ∈ U) (u ∈ U), y = t * u} ∧ {y : A | ∃ (t ∈ U) (u ∈ U), y = t * u} ⊆ U) → (∃ (A₀ : set A) [h : is_subring A₀], by haveI := h; exact is_ring_of_definition A₀) := begin rintro ⟨U, T, Tsub, Tfin, hnhds, hTU, hU2⟩, sorry end

#### Johan Commelin (Oct 04 2018 at 13:14):

It looks really scary

#### Johannes Hölzl (Oct 04 2018 at 13:18):

Uh, the `haveI`

is super ugly. One more reason to not use type classes too often...

I think I would prefer if you use `@is_ring_of_definition ...`

#### Johan Commelin (Oct 04 2018 at 13:20):

Hmm... we should just have bundled subrings (-;

#### Johannes Hölzl (Oct 04 2018 at 13:20):

also an option

#### Johannes Hölzl (Oct 04 2018 at 13:21):

what is `is_ring_of_definition`

?

#### Johan Commelin (Oct 04 2018 at 13:21):

Also nasty (-;

#### Johan Commelin (Oct 04 2018 at 13:22):

def is_ring_of_definition (A₀ : set A) [is_subring A₀] : Prop := is_open A₀ ∧ (∃ (J : set A₀) [hJ : is_ideal J] (gen : set A₀), (set.finite gen ∧ span gen = J) ∧ (by haveI := topological_subring A₀; haveI := hJ; exact is_ideal_adic J))

#### Johan Commelin (Oct 04 2018 at 13:22):

def is_ideal_adic (J : set A) [is_ideal J] : Prop := (∀ n, is_open (pow_ideal J n)) ∧ (∀ S : set A, (0 : A) ∈ S → is_open S → ∃ n, pow_ideal J n ⊆ S) def is_adic (A₀ : set A) [is_subring A₀] : Prop := ∃ (J : set A₀) [hJ : is_ideal J], (by haveI := topological_subring A₀; haveI := hJ; exact is_ideal_adic J)

#### Johan Commelin (Oct 04 2018 at 13:25):

But, I'm not looking for help with the maths. I'm just wondering how the assumptions could be formulated in a nicer way.

#### Johan Commelin (Oct 04 2018 at 13:25):

Should we put a `has_mul`

on `set A`

if `A`

has `has_mul`

?

#### Johan Commelin (Oct 04 2018 at 13:26):

if `set A`

is a monoid, then I could just write `U^n`

and `T * U`

.

#### Johannes Hölzl (Oct 04 2018 at 13:27):

First thing: I wouldn't use the existential quantifier in the assumption, have all the things in there directly as assumption

#### Johannes Hölzl (Oct 04 2018 at 13:28):

`{y : A | ∃ (t ∈ U) (u ∈ U), y = t * u} = (*) <$> U <*> T`

#### Johan Commelin (Oct 04 2018 at 13:28):

Hmm, in fact it is an iff, but I only stated one implication.

#### Johannes Hölzl (Oct 04 2018 at 13:28):

`(*) <$> T <*> U = (*) <$> U <*> U ∧ (*) <$> U <*> U ⊆ U`

#### Johan Commelin (Oct 04 2018 at 13:29):

Not sure if that improves readability.... what do you think of my `monoid (set A)`

suggestion?

#### Johannes Hölzl (Oct 04 2018 at 13:29):

The `<$>`

and `<*>`

are from the applicative functor structor on `set`

. Their function is to lift arbitrary functions to sets.

#### Johan Commelin (Oct 04 2018 at 13:30):

I don't think a random mathematician will care about that. When they read Kevin's perfectoid paper, they will want to see code that they roughly understand

#### Johannes Hölzl (Oct 04 2018 at 13:31):

you can certainly add the `monoid (set A)`

locally. I'm not sure if we want to have this setup generally

#### Mario Carneiro (Oct 04 2018 at 14:40):

Ooh, this is nice. I know the mathematicians here are going to freak, but I really like that the CS version of abstract nonsense has given us a way to easily talk about lifting functions to sets like $S + T$

#### Johan Commelin (Oct 04 2018 at 14:50):

What does "Ooh, this is nice" mean? As in: just use it, even if it is completely unreadable?

#### Mario Carneiro (Oct 04 2018 at 14:55):

Basically yes. Treat it like an idiom or set phrase to say this

#### Mario Carneiro (Oct 04 2018 at 14:57):

When Simon first showed me the `f <$> x <*> y`

idiom for applying functions to monadic values I was mystified, but now I quite like it since it looks so much like regular function application

#### Mario Carneiro (Oct 04 2018 at 14:58):

(It is equivalent to the monadic block `do a <- x, b <- y, return (f a b)`

)

#### Mario Carneiro (Oct 04 2018 at 14:59):

Until I saw this thread I thought that we would basically have to define a function `lift2 f A B`

for doing this, and it would be even less nice to read

#### Johan Commelin (Oct 04 2018 at 15:01):

What is wrong with the `monoid`

instance?

#### Mario Carneiro (Oct 04 2018 at 15:01):

That said, there are also other semi-slick ways of talking about this, like `uncurry (+) '' (A × B)`

#### Mario Carneiro (Oct 04 2018 at 15:02):

Well, it doesn't generalize as much as this

#### Mario Carneiro (Oct 04 2018 at 15:03):

It may also cause a problem when we have a conflicting meaning for multiplication of sets

#### Mario Carneiro (Oct 04 2018 at 15:04):

I think `has_sub`

has a conflict

Last updated: May 09 2021 at 11:09 UTC