Zulip Chat Archive

Stream: maths

Topic: fundamental system of neighborhoods


view this post on Zulip Johan Commelin (Oct 04 2018 at 11:24):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Oct 04 2018 at 12:35):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 04 2018 at 12:46):

Ok, so I want to write (nhds 0) = "the smallest filter containing {myset}". Is that right?

view this post on Zulip Johan Commelin (Oct 04 2018 at 12:46):

That would mean that {myset} is a fundamental system of neighbourhoods around 0.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Oct 04 2018 at 12:54):

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

view this post on Zulip Patrick Massot (Oct 04 2018 at 12:56):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:00):

@Patrick Massot Why do you ask pure 0 ≤ Z? Why not equality?

view this post on Zulip 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))

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:00):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:14):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:14):

It looks really scary

view this post on Zulip 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 ...

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:20):

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

view this post on Zulip Johannes Hölzl (Oct 04 2018 at 13:20):

also an option

view this post on Zulip Johannes Hölzl (Oct 04 2018 at 13:21):

what is is_ring_of_definition?

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:21):

Also nasty (-;

view this post on Zulip 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))

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:25):

Should we put a has_mul on set A if A has has_mul?

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:26):

if set A is a monoid, then I could just write U^n and T * U.

view this post on Zulip 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

view this post on Zulip Johannes Hölzl (Oct 04 2018 at 13:28):

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

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:28):

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

view this post on Zulip Johannes Hölzl (Oct 04 2018 at 13:28):

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

view this post on Zulip Johan Commelin (Oct 04 2018 at 13:29):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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+TS + T

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 04 2018 at 14:55):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 04 2018 at 14:58):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 04 2018 at 15:01):

What is wrong with the monoid instance?

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Oct 04 2018 at 15:02):

Well, it doesn't generalize as much as this

view this post on Zulip Mario Carneiro (Oct 04 2018 at 15:03):

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

view this post on Zulip Mario Carneiro (Oct 04 2018 at 15:04):

I think has_sub has a conflict


Last updated: May 09 2021 at 11:09 UTC