English
Under the same hypotheses as above, the orbit map is an open map; i.e., images of open sets are open in X.
Русский
При тех же предположениях орбитное отображение открыто: образ открытого множества по карте g ↦ g•x образует открытую подпространство X.
LaTeX
$$IsOpenMap( g \\mapsto g\\cdot x )$$
Lean4
/-- 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. -/
@[to_additive /-- 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 (x : X) : IsOpenMap (fun (g : G) ↦ g • x) := by
/- We have already proved the theorem around the basepoint of the orbit, in
`smul_singleton_mem_nhds_of_sigmaCompact`. The general statement follows around an arbitrary
point by changing basepoints. -/
simp_rw [isOpenMap_iff_nhds_le, Filter.le_map_iff]
intro g U hU
have : (· • x) = (· • (g • x)) ∘ (· * g⁻¹) := by
ext g
simp [smul_smul]
rw [this, image_comp, ← smul_singleton]
apply smul_singleton_mem_nhds_of_sigmaCompact
simpa using isOpenMap_mul_right g⁻¹ |>.image_mem_nhds hU
