English
IsProperMap f is equivalent to continuity plus closedness of the canonical map on X × Ultrafilter X to Y × Ultrafilter X.
Русский
IsProperMap f эквивалентно сохранению непрерывности и замкнутости соответствующего отображения на \(X × Ultrafilter X → Y × Ultrafilter X\).
LaTeX
$$$IsProperMap(f) \\iff (Continuous(f) \\land IsClosedMap(Prod.map(f, id) : X \\times Ultrafilter X \\to Y \\times Ultrafilter X))$$$
Lean4
/-- A map `f : X → Y` is proper if and only if it is continuous and the map
`(Prod.map f id : X × Ultrafilter X → Y × Ultrafilter X)` is closed. This is stronger than
`isProperMap_iff_universally_closed` since it shows that there's only one space to check to get
properness, but in most cases it doesn't matter. -/
theorem isProperMap_iff_isClosedMap_ultrafilter {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y]
{f : X → Y} : IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id : X × Ultrafilter X → Y × Ultrafilter X) :=
by
-- The proof is basically the same as above.
constructor <;> intro H
· exact ⟨H.continuous, H.universally_closed _⟩
· rw [isProperMap_iff_ultrafilter]
refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
let F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
have := H.2 F isClosed_closure
have : (y, 𝒰) ∈ Prod.map f id '' F :=
this.mem_of_tendsto (hy.prodMk_nhds (Ultrafilter.tendsto_pure_self 𝒰))
(Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
rw [mem_closure_iff_nhds] at hx
rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU ((ultrafilter_isOpen_basic _).mem_nhds hUc)) with
⟨⟨y, 𝒢⟩, ⟨⟨hy : y ∈ U, hy' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure y⟩⟩
exact hy' hy
