English
If there is a closed embedding f: H → G between groups and a compatible action, then a proper SMul of G on X implies a proper SMul of H on X.
Русский
Если имеется замкнутое вложение f: H → G между группами и совместное действие, то корректное действие G на X влечёт корректное действие H на X.
LaTeX
$$$\\text{ProperSMul } H X$ follows from$ f: H \\to G$ closed embedding and compatibility $f(h)\\cdot x = h\\cdot x$ with$ \\text{ProperSMul } G X$.$$
Lean4
/-- If two groups `H` and `G` act on a topological space `X` such that `G` acts properly and
there exists a group homomorphism `H → G` which is a closed embedding compatible with the actions,
then `H` also acts properly on `X`. -/
@[to_additive /-- If two groups `H` and `G` act on a topological space `X` such that `G` acts
properly and there exists a group homomorphism `H → G` which is a closed embedding compatible with
the actions, then `H` also acts properly on `X`. -/
]
theorem properSMul_of_isClosedEmbedding {H : Type*} [Group H] [MulAction H X] [TopologicalSpace H] [ProperSMul G X]
(f : H →* G) (f_clemb : IsClosedEmbedding f) (f_compat : ∀ (h : H) (x : X), f h • x = h • x) : ProperSMul H X where
isProperMap_smul_pair :=
by
have h : IsProperMap (Prod.map f (fun x : X ↦ x)) := f_clemb.isProperMap.prodMap isProperMap_id
have : (fun hx : H × X ↦ (hx.1 • hx.2, hx.2)) = (fun hx ↦ (f hx.1 • hx.2, hx.2)) := by simp [f_compat]
rw [this]
exact ProperSMul.isProperMap_smul_pair.comp h
