# Documentation

Mathlib.Topology.Algebra.Group.OpenMapping

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

theorem vadd_singleton_mem_nhds_of_sigmaCompact {G : Type u_1} {X : Type u_2} [] [] [] [] [] [] [] {U : Set G} (hU : U nhds 0) (x : X) :
U +ᵥ {x} nhds x

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.

theorem smul_singleton_mem_nhds_of_sigmaCompact {G : Type u_1} {X : Type u_2} [] [] [] [] [] [] [] [] {U : Set G} (hU : U nhds 1) (x : X) :
U {x} nhds x

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.

theorem isOpenMap_vadd_of_sigmaCompact {G : Type u_1} {X : Type u_2} [] [] [] [] [] [] [] (x : X) :
IsOpenMap fun (g : G) => g +ᵥ x

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.

theorem isOpenMap_smul_of_sigmaCompact {G : Type u_1} {X : Type u_2} [] [] [] [] [] [] [] [] (x : X) :
IsOpenMap fun (g : G) => g x

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.

theorem AddMonoidHom.isOpenMap_of_sigmaCompact {G : Type u_1} [] [] {H : Type u_3} [] [] [] [] [] (f : G →+ H) (hf : ) (h'f : ) :
theorem MonoidHom.isOpenMap_of_sigmaCompact {G : Type u_1} [] [] [] {H : Type u_3} [] [] [] [] [] (f : G →* H) (hf : ) (h'f : ) :

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