# Open mapping theorem for morphisms of topological groups #

We prove that a continuous surjective group morphism from a sigma-compact group to a locally compact
group is automatically open, in `MonoidHom.isOpenMap_of_sigmaCompact`

.

We deduce this from a similar statement for the orbits of continuous actions of sigma-compact groups
on Baire spaces, given in `isOpenMap_smul_of_sigmaCompact`

.

Note that a sigma-compactness assumption is necessary. Indeed, let `G`

be the real line with
the discrete topology, and `H`

the real line with the usual topology. Both are locally compact
groups, and the identity from `G`

to `H`

is continuous but not open.

Consider a sigma-compact additive group acting continuously and transitively on a
Baire space. Then the orbit map is open around zero. It follows in
`isOpenMap_vadd_of_sigmaCompact`

that it is open around any point.

Consider a sigma-compact group acting continuously and transitively on a Baire space. Then
the orbit map is open around the identity. It follows in `isOpenMap_smul_of_sigmaCompact`

that it
is open around any point.

Consider a sigma-compact additive group acting continuously and transitively on a Baire space. Then the orbit map is open. This is a version of the open mapping theorem, valid notably for the action of a sigma-compact locally compact group on a locally compact space.

Consider a sigma-compact group acting continuously and transitively on a Baire space. Then the orbit map is open. This is a version of the open mapping theorem, valid notably for the action of a sigma-compact locally compact group on a locally compact space.

A surjective morphism of topological groups is open when the source group is sigma-compact and the target group is a Baire space (for instance a locally compact group).