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 smul_singleton_mem_nhds_of_sigmaCompact {G : Type u_1} {X : Type u_2} [TopologicalSpace G] [TopologicalSpace X] [Group G] [TopologicalGroup G] [MulAction G X] [SigmaCompactSpace G] [BaireSpace X] [T2Space X] [ContinuousSMul G X] [MulAction.IsPretransitive G X] {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 vadd_singleton_mem_nhds_of_sigmaCompact {G : Type u_1} {X : Type u_2} [TopologicalSpace G] [TopologicalSpace X] [AddGroup G] [TopologicalAddGroup G] [AddAction G X] [SigmaCompactSpace G] [BaireSpace X] [T2Space X] [ContinuousVAdd G X] [AddAction.IsPretransitive G X] {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 isOpenMap_smul_of_sigmaCompact {G : Type u_1} {X : Type u_2} [TopologicalSpace G] [TopologicalSpace X] [Group G] [TopologicalGroup G] [MulAction G X] [SigmaCompactSpace G] [BaireSpace X] [T2Space X] [ContinuousSMul G X] [MulAction.IsPretransitive G X] (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 isOpenMap_vadd_of_sigmaCompact {G : Type u_1} {X : Type u_2} [TopologicalSpace G] [TopologicalSpace X] [AddGroup G] [TopologicalAddGroup G] [AddAction G X] [SigmaCompactSpace G] [BaireSpace X] [T2Space X] [ContinuousVAdd G X] [AddAction.IsPretransitive G X] (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 MonoidHom.isOpenMap_of_sigmaCompact {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [SigmaCompactSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] [BaireSpace H] [T2Space H] [ContinuousMul H] (f : G →* H) (hf : Function.Surjective ⇑f) (h'f : Continuous ⇑f) : IsOpenMap ⇑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).

theorem AddMonoidHom.isOpenMap_of_sigmaCompact {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [SigmaCompactSpace G] {H : Type u_3} [AddGroup H] [TopologicalSpace H] [BaireSpace H] [T2Space H] [ContinuousAdd H] (f : G →+ H) (hf : Function.Surjective ⇑f) (h'f : Continuous ⇑f) : IsOpenMap ⇑f