## 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):

https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/topological_groups.lean#L102

#### 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 (-;

also an option

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

what is is_ring_of_definition?

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

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

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

#### 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