English
A map is proper iff it is continuous, closed, and all fibers over points are compact.
Русский
Отображение проперно тогда и только тогда, когда оно непрерывно, закрыто и все волокна над точками компактны.
LaTeX
$$$IsProperMap f \iff (Continuous f \land IsClosedMap f \land \forall y, IsCompact (f^{-1}({y})))$$$
Lean4
/-- A map is proper if and only if it is closed and its fibers are compact. -/
theorem isProperMap_iff_isClosedMap_and_compact_fibers :
IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ ∀ y, IsCompact (f ⁻¹' { y }) :=
by
constructor <;> intro H
· exact ⟨H.continuous, H.isClosedMap, fun y ↦ H.isCompact_preimage isCompact_singleton⟩
· rw [isProperMap_iff_clusterPt]
-- Let `ℱ : Filter X` and `y` some cluster point of `map f ℱ`.
refine
⟨H.1, fun ℱ y hy ↦ ?_⟩
-- That means that the singleton `pure y` meets the "closure" of `map f ℱ`, by which we mean
-- `Filter.lift' (map f ℱ) closure`. But `f` is closed, so
-- `closure (map f ℱ) = map f (closure ℱ)` (see `IsClosedMap.lift'_closure_map_eq`).
-- Thus `map f (closure ℱ ⊓ 𝓟 (f ⁻¹' {y})) = map f (closure ℱ) ⊓ 𝓟 {y} ≠ ⊥`, hence
-- `closure ℱ ⊓ 𝓟 (f ⁻¹' {y}) ≠ ⊥`.
rw [H.2.1.mapClusterPt_iff_lift'_closure H.1] at hy
rcases H.2.2 y (f := Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' { y })) inf_le_right with ⟨x, hxy, hx⟩
refine
⟨x, hxy, ?_⟩
-- In particular `x` is a cluster point of `closure ℱ`. Since cluster points of `closure ℱ`
-- are exactly cluster points of `ℱ` (see `clusterPt_lift'_closure_iff`), this completes
-- the proof.
rw [← clusterPt_lift'_closure_iff]
exact hx.mono inf_le_left
