English
A surjective morphism of topological groups is open when the source is sigma-compact and the target is a Baire space (for instance locally compact).
Русский
Гомоморфизм между топологическими группами, являющийся сюръективным, открывается, если источник σ-компактен, а цель — пространство Баири (например локально компактная).
LaTeX
$$$\\text{If } f:G\\to H \\text{ is surjective and continuous, with } G \\text{ σ-compact and } H \\text{ Baire},\\; f\\ \\text{is open}.$$$
Lean4
/-- 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). -/
@[to_additive]
theorem isOpenMap_of_sigmaCompact {H : Type*} [Group H] [TopologicalSpace H] [BaireSpace H] [T2Space H]
[ContinuousMul H] (f : G →* H) (hf : Function.Surjective f) (h'f : Continuous f) : IsOpenMap f :=
by
let A : MulAction G H := MulAction.compHom _ f
have : ContinuousSMul G H := continuousSMul_compHom h'f
have : IsPretransitive G H := isPretransitive_compHom hf
have : f = (fun (g : G) ↦ g • (1 : H)) := by simp [A, MulAction.compHom_smul_def]
rw [this]
exact isOpenMap_smul_of_sigmaCompact _
