Open subgroups of a topological groups #
This files builds the lattice
OpenSubgroup G of open subgroups in a topological group
and its additive version
OpenAddSubgroup. This lattice has a top element, the subgroup of all
elements, but no bottom element in general. The trivial subgroup which is the natural candidate
bottom has no reason to be open (this happens only in discrete groups).
Note that this notion is especially relevant in a non-archimedean context, for instance for
Main declarations #
OpenSubgroup.isClosed: An open subgroup is automatically closed.
Subgroup.isOpen_mono: A subgroup containing an open subgroup is open. There are also versions for additive groups, submodules and ideals.
OpenSubgroup.comap: Open subgroups can be pulled back by a continuous group morphism.
- Prove that the identity component of a locally path connected group is an open subgroup. Up to now this file is really geared towards non-archimedean algebra, not Lie groups.
The type of open subgroups of a topological additive group.
The type of open subgroups of a topological group.