Zulip Chat Archive

Stream: maths

Topic: Group filter bases


Yury G. Kudryashov (Jan 08 2023 at 04:08):

Hi, I suggest that we migrate from docs#group_filter_basis to

structure group_filter (G : Type*) [group G] extends filter G :=
(one' : 1  to_filter)
(mul' : to_filter * to_filter  to_filter)
(inv' : to_filter⁻¹  to_filter)
(conj' :  x, tendsto (λ y, x * y * x⁻¹) to_filter to_filter)

Yury G. Kudryashov (Jan 08 2023 at 04:11):

The main pro of this approach is that group_filters are in ≃o correspondence with group topologies.

Yury G. Kudryashov (Jan 08 2023 at 04:12):

Two different f g : group_filter_basis G can define the same topology (if they define the same filter) but two different group_filters define different topologies.

Yury G. Kudryashov (Jan 08 2023 at 04:16):

Also, sometimes it's easier to construct a filter, not a filter basis. E.g., instead of docs#seminorm_family.basis_sets and related definitions we can use ⨅ i, (p i).to_filter, where seminorm.to_filter p := ⨅ (r : ℝ) (hr : 0 < ℝ), p.ball (0 : E) r.

Yury G. Kudryashov (Jan 08 2023 at 04:17):

As far as I can tell, these definitions are equivalent to what we have but it's easier to use infi_le, le_infi etc instead of destructing intersections of balls here and there.

Yury G. Kudryashov (Jan 08 2023 at 04:17):

@Patrick Massot What do you think? :up:

Kevin Buzzard (Jan 08 2023 at 13:23):

Do you also propose we delete the definition of a basis of a topological space because two bases can generate the same topology?

Kevin Buzzard (Jan 08 2023 at 13:25):

Oh -- what do you mean by "migrate"? We certainly used group filter bases when putting the topology on an infinite Galois group.

Patrick Massot (Jan 08 2023 at 14:02):

There are definitely cases where the natural thing is the filter basis, for instance for non-archimedean groups. We also have docs#topological_group.of_nhds_one which is closer to what wrote, but assumes you already have a topology (and is used in the proof of group_filter_basis.is_topological_group). That lemma could also be used to prove that group_filter gives rise to topological group. Those are all very close variations. I was worried that including all variations would result in a bloated API, but you can try. But it would be sad to loose the wording "the I-adic topology is the topology having as a basis of neighborhoods of zero the powers of I" and replace it by something much harder to read for beginners without a really clear gain.

Kevin Buzzard (Jan 08 2023 at 19:17):

The topology of an infinite Galois group Gal(L/K) is defined as "basis of nhds of 1 is Gal(L/E) as E runs through intermediate fields finite over K".

Yury G. Kudryashov (Jan 08 2023 at 19:34):

Probably, I badly formulated my proposal. I'll make some proposal with code, then we'll decide what parts of it should be merged. I understand that the answer can be "all of it".


Last updated: Dec 20 2023 at 11:08 UTC