fundamental system of neighborhoods

Stream: maths

[Johan Commelin]

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

[Kevin Buzzard]

This would be a basis for the filter nhds 0, right? Or are you asking for more?

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

The smallest filter containing s is filter.generate s (https://github.com/leanprover/mathlib/blob/master/order/filter.lean#L241)

[Kevin Buzzard]

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]

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]

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]

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

[Patrick Massot]

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

[Johannes Hölzl]

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

[Johan Commelin]

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

[Johan Commelin]

I've got the very ugly

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

[Kevin Buzzard]

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]

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

[Johannes Hölzl]

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]

@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]

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

[Johan Commelin]

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]

It looks really scary

[Johannes Hölzl]

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]

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

[Johannes Hölzl]

also an option

[Johannes Hölzl]

what is is_ring_of_definition?

[Johan Commelin]

Also nasty (-;

[Johan Commelin]

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]

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]

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]

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

[Johan Commelin]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Johan Commelin]

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

[Johannes Hölzl]

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

[Johan Commelin]

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

[Johannes Hölzl]

The <$> and <*> are from the applicative functor structor on set. Their function is to lift arbitrary functions to sets.

[Johan Commelin]

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]

you can certainly add the monoid (set A) locally. I'm not sure if we want to have this setup generally

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

What is wrong with the monoid instance?

[Mario Carneiro]

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

[Mario Carneiro]

Well, it doesn't generalize as much as this

[Mario Carneiro]

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

[Mario Carneiro]

I think has_sub has a conflict