Proving that group_filter_basis induces a group topology

Stream: maths

[Sebastian Monnet]

A docs#group_filter_basis on a group $G$ is a collection $\mathcal{B}$ of subsets of $G$ satisfying some axioms. For each element $x \in G$, we define the neighbourhoods of $x$ to be

$\mathcal{N}(x) = \{N \subseteq G : xD \subseteq N \text{ for some } D \in \mathcal{B}\}.$

Then we define a topology on $G$ by making $U\subseteq G$ open if and only if for all $x \in U$, we have $U \in \mathcal{N}(x)$. In other words, $U$ is open if and only if for all $x \in U$, there exists $D_x \in \mathcal{B}$ with $xD_x \subseteq U$. docs#group_filter_basis.is_topological_group tells us that this topology makes $G$ into a topological group. The proof in mathlib uses filters, but I would like to prove the theorem (not in Lean) using standard open set definitions.

Currently, I'm stuck trying to show that multiplication is continuous. In order to do this, we need to show that for all $x,y \in G$ and open $W$ containing $xy$, there are open sets $x \in U$ and $y \in V$ such that $U \cdot V \subseteq W$. So let $xy \in W$ be open. Then by definition of the topology, there is some $D \in \mathcal{B}$ with $xyD \subseteq W$. By docs#group_filter_basis.mul', there is some $D' \in \mathcal{B}$ with $D'\cdot D'\subseteq D$, and by docs#conj', there is also some $D'' \in \mathcal{B}$ with $y^{-1}D''y \subseteq D'$. Then we have

$xD''\cdot yD' = xyy^{-1}D''yD' \subseteq xyD'\cdot D' \subseteq xy D.$

So at this point, all I need is some open $x \in U \subseteq xD''$ and $y \in V \subseteq yD'$. However, I am struggling to find such $U$ and $V$. I thought about defining the interiors of these sets as $N^\circ = \{x \in N : N \in \mathcal{N}(x)\}$, but I wasn't able to show that these are open using the axioms of a group filter basis.

Can anyone help me prove this?

[Patrick Massot]

The crucial thing you are probably missing is that $\mathcal{N}$ satisfies the second part of the assumptions in docs#topological_space.nhds_mk_of_nhds. This is proved in https://github.com/leanprover-community/mathlib/blob/77e76ee5bcac94fe8b67d64b72ee59176761ea77/src/topology/algebra/filter_basis.lean#L152

[Patrick Massot]

That being said, you seem to be doing pretty masochistic work in wanting to use group filter bases but not filters...

[Sebastian Monnet]

Patrick Massot said:

That being said, you seem to be doing pretty masochistic work in wanting to use group filter bases but not filters...

So would you say that my proof strategy is doomed to be unpleasant unless I invoke results proved using filters? My intuition was that there must be a short proof of such a simple fact

[Patrick Massot]

Filters are simple!

[Patrick Massot]

But you can definitely write a proof inlining everything there is to know here. I indicated the missing argument.

[Sebastian Monnet]

Ah yes, you're right. That argument was exactly what I was looking for

[Sebastian Monnet]

Thank you*