Group filter bases

Stream: maths

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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]

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]

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]

@Patrick Massot What do you think? :up:

[Kevin Buzzard]

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]

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

[Patrick Massot]

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]

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]

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".