English
If a group G acts properly on X, then there is a canonical instance giving a continuous action of G on X.
Русский
Если группа G действует корректно на X, то существует канонический экземпляр, задающий непрерывное действие G на X.
LaTeX
$$$\\text{ContinuousSMul } G X$$$
Lean4
/-- A group `G` acts properly on a topological space `X` if and only if for all ultrafilters
`𝒰` on `X × G`, if `𝒰` converges to `(x₁, x₂)` along the map `(g, x) ↦ (g • x, x)`,
then there exists `g : G` such that `g • x₂ = x₁` and `𝒰.fst` converges to `g`. -/
@[to_additive /-- An additive group `G` acts properly on a topological space `X` if and only if
for all ultrafilters `𝒰` on `X`, if `𝒰` converges to `(x₁, x₂)`
along the map `(g, x) ↦ (g • x, x)`, then there exists `g : G` such that `g • x₂ = x₁`
and `𝒰.fst` converges to `g`. -/
]
theorem properSMul_iff_continuousSMul_ultrafilter_tendsto :
ProperSMul G X ↔
ContinuousSMul G X ∧
(∀ 𝒰 : Ultrafilter (G × X),
∀ x₁ x₂ : X,
Tendsto (fun gx : G × X ↦ (gx.1 • gx.2, gx.2)) 𝒰 (𝓝 (x₁, x₂)) →
∃ g : G, g • x₂ = x₁ ∧ Tendsto (Prod.fst : G × X → G) 𝒰 (𝓝 g)) :=
by
refine ⟨fun h ↦ ⟨inferInstance, fun 𝒰 x₁ x₂ h' ↦ ?_⟩, fun ⟨cont, h⟩ ↦ ?_⟩
· rw [properSMul_iff, isProperMap_iff_ultrafilter] at h
rcases h.2 h' with ⟨gx, hgx1, hgx2⟩
refine ⟨gx.1, ?_, (continuous_fst.tendsto gx).mono_left hgx2⟩
simp only [Prod.mk.injEq] at hgx1
rw [← hgx1.2, hgx1.1]
· rw [properSMul_iff, isProperMap_iff_ultrafilter]
refine ⟨by fun_prop, fun 𝒰 (x₁, x₂) hxx ↦ ?_⟩
rcases h 𝒰 x₁ x₂ hxx with ⟨g, hg1, hg2⟩
refine ⟨(g, x₂), by simp_rw [hg1], ?_⟩
rw [nhds_prod_eq, 𝒰.le_prod]
exact ⟨hg2, (continuous_snd.tendsto _).comp hxx⟩
