Proper maps between topological spaces

This file develops the basic theory of proper maps between topological spaces. A map f : X → Y between two topological spaces is said to be proper if it is continuous and satisfies the following equivalent conditions:

1. f is closed and has compact fibers.
2. f is universally closed, in the sense that for any topological space Z, the map Prod.map f id : X × Z → Y × Z is closed.
3. For any ℱ : Filter X, all cluster points of map f ℱ are images by f of some cluster point of ℱ.

We take 3 as the definition in IsProperMap, and we show the equivalence with 1, 2, and some other variations. We also show the usual characterization of proper maps to a locally compact Hausdorff space as continuous maps such that preimages of compact sets are compact.

Main statements

• isProperMap_iff_ultrafilter: characterization of proper maps in terms of limits of ultrafilters instead of cluster points of filters.
• IsProperMap.pi_map: any product of proper maps is proper.
• isProperMap_iff_isClosedMap_and_compact_fibers: a map is proper if and only if it is continuous, closed, and has compact fibers
• isProperMap_iff_isCompact_preimage: a map to a locally compact Hausdorff space is proper if and only if it is continuous and preimages of compact sets are compact.
• isProperMap_iff_universally_closed: a map is proper if and only if it is continuous and universally closed, in the sense of condition 2. above.

Implementation notes

In algebraic geometry, it is common to also ask that proper maps are separated, in the sense of Stacks: definition OCY1. We don't follow this convention because it is unclear whether it would give the right notion in all cases, and in particular for the theory of proper group actions. That means that our terminology does NOT align with that of Stacks: Characterizing proper maps, instead our definition of IsProperMap coincides with what they call "Bourbaki-proper".

Regarding the proofs, we don't really follow Bourbaki and go for more filter-heavy proofs, as usual. In particular, their arguments rely heavily on restriction of closed maps (see IsClosedMap.restrictPreimage), which makes them somehow annoying to formalize in type theory. In contrast, the filter-based proofs work really well thanks to the existing API.

In fact, the filter proofs work so well that I thought this would be a great pedagogical resource about how we use filters. For that reason, all interesting proofs in this file are commented, so don't hesitate to have a look!

TODO

• prove the equivalence with condition 3 of Stacks: Theorem 005R. Note that they mean something different by "universally closed".

References

• [N. Bourbaki, General Topology][bourbaki1966]
• Stacks: Characterizing proper maps

theorem isProperMap_iff_clusterPt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : IsProperMap f ↔ Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ

Definition of proper maps. See also isClosedMap_iff_clusterPt for a related criterion for closed maps.

structure IsProperMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) extends Continuous : Prop

A map f : X → Y between two topological spaces is said to be proper if it is continuous and, for all ℱ : Filter X, any cluster point of map f ℱ is the image by f of a cluster point of ℱ.

• isOpen_preimage : ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)
• clusterPt_of_mapClusterPt : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ

  By definition, if f is a proper map and ℱ is any filter on X, then any cluster point of map f ℱ is the image by f of some cluster point of ℱ.

theorem IsProperMap.clusterPt_of_mapClusterPt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (self : IsProperMap f) ⦃ℱ : Filter X⦄ ⦃y : Y⦄ : MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ

By definition, if f is a proper map and ℱ is any filter on X, then any cluster point of map f ℱ is the image by f of some cluster point of ℱ.

theorem IsProperMap.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsProperMap f) : Continuous f

By definition, a proper map is continuous.

theorem IsProperMap.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsProperMap f) : IsClosedMap f

A proper map is closed.

theorem isProperMap_iff_ultrafilter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ (x : X), f x = y ∧ ↑𝒰 ≤ nhds x

Characterization of proper maps by ultrafilters.

theorem isProperMap_iff_ultrafilter_of_t2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [T2Space Y] : IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ (x : X), ↑𝒰 ≤ nhds x

theorem IsProperMap.ultrafilter_le_nhds_of_tendsto {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsProperMap f) ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄ (hy : Filter.Tendsto f (↑𝒰) (nhds y)) : ∃ (x : X), f x = y ∧ ↑𝒰 ≤ nhds x

If f is proper and converges to y along some ultrafilter 𝒰, then 𝒰 converges to some x such that f x = y.

theorem IsProperMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsProperMap f) (hg : IsProperMap g) : IsProperMap (g ∘ f)

The composition of two proper maps is proper.

theorem isProperMap_of_comp_of_surj {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : Continuous f) (hg : Continuous g) (hgf : IsProperMap (g ∘ f)) (f_surj : Function.Surjective f) : IsProperMap g

If the composition of two continuous functions g ∘ f is proper and f is surjective, then g is proper.

theorem isProperMap_of_comp_of_inj {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : Continuous f) (hg : Continuous g) (hgf : IsProperMap (g ∘ f)) (g_inj : Function.Injective g) : IsProperMap f

If the composition of two continuous functions g ∘ f is proper and g is injective, then f is proper.

theorem isProperMap_of_comp_of_t2 {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} [T2Space Y] (hf : Continuous f) (hg : Continuous g) (hgf : IsProperMap (g ∘ f)) : IsProperMap f

If the composition of two continuous functions f : X → Y and g : Y → Z is proper and Y is T2, then f is proper.

theorem IsProperMap.prod_map {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsProperMap f) (hg : IsProperMap g) : IsProperMap (Prod.map f g)

A binary product of proper maps is proper.

theorem IsProperMap.pi_map {ι : Type u_5} {X : ι → Type u_6} {Y : ι → Type u_7} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i} (h : ∀ (i : ι), IsProperMap (f i)) : IsProperMap fun (x : (i : ι) → X i) (i : ι) => f i (x i)

Any product of proper maps is proper.

theorem IsProperMap.isCompact_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsProperMap f) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K)

The preimage of a compact set by a proper map is again compact. See also isProperMap_iff_isCompact_preimage which proves that this property completely characterizes proper map when the codomain is locally compact and Hausdorff.

theorem isProperMap_iff_isClosedMap_and_compact_fibers {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

A map is proper if and only if it is closed and its fibers are compact.

theorem isProperMap_iff_isClosedMap_of_inj {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (f_cont : Continuous f) (f_inj : Function.Injective f) : IsProperMap f ↔ IsClosedMap f

An injective and continuous function is proper if and only if it is closed.

theorem isProperMap_of_isClosedMap_of_inj {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (f_cont : Continuous f) (f_inj : Function.Injective f) (f_closed : IsClosedMap f) : IsProperMap f

A injective continuous and closed map is proper.

@[simp]

theorem Homeomorph.isProperMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : IsProperMap ⇑e

A homeomorphism is proper.

@[simp]

theorem isProperMap_id {X : Type u_1} [TopologicalSpace X] : IsProperMap id

The identity is proper.

theorem isProperMap_of_closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : ClosedEmbedding f) : IsProperMap f

A closed embedding is proper.

theorem isProperMap_subtype_val_of_closed {X : Type u_1} [TopologicalSpace X] {U : Set X} (hU : IsClosed U) : IsProperMap Subtype.val

The coercion from a closed subset is proper.

theorem isProperMap_restr_of_proper_of_closed {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {U : Set X} (hf : IsProperMap f) (hU : IsClosed U) : IsProperMap fun (x : ↑U) => f ↑x

The restriction of a proper map to a closed subset is proper.

theorem IsProperMap.closed_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsProperMap f) : IsClosed (Set.range f)

The range of a proper map is closed.

theorem isProperMap_iff_isClosedMap_and_tendsto_cofinite {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [T1Space Y] : IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Filter.Tendsto f (Filter.cocompact X) Filter.cofinite

Version of isProperMap_iff_isClosedMap_and_compact_fibers in terms of cofinite and cocompact. Only works when the codomain is T1.

theorem Continuous.isProperMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [CompactSpace X] [T2Space Y] (hf : Continuous f) : IsProperMap f

A continuous map from a compact space to a T₂ space is a proper map.

theorem isProperMap_iff_isCompact_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [T2Space Y] [WeaklyLocallyCompactSpace Y] : IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)

If Y is locally compact and Hausdorff, then proper maps X → Y are exactly continuous maps such that the preimage of any compact set is compact.

theorem isProperMap_iff_tendsto_cocompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [T2Space Y] [WeaklyLocallyCompactSpace Y] : IsProperMap f ↔ Continuous f ∧ Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)

Version of isProperMap_iff_isCompact_preimage in terms of cocompact.

theorem IsProperMap.universally_closed {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (Z : Type u_6) [TopologicalSpace Z] (h : IsProperMap f) : IsClosedMap (Prod.map f id)

A proper map f : X → Y is universally closed: for any topological space Z, the map Prod.map f id : X × Z → Y × Z is closed. We will prove in isProperMap_iff_universally_closed that proper maps are exactly continuous maps which have this property, but this result should be easier to use because it allows Z to live in any universe.

theorem isProperMap_iff_isClosedMap_filter {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)

A map f : X → Y is proper if and only if it is continuous and the map (Prod.map f id : X × Filter X → Y × Filter 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)

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_universally_closed {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

A map f : X → Y is proper if and only if it is continuous and universally closed, in the sense that for any topological space Z, the map Prod.map f id : X × Z → Y × Z is closed. Note that Z lives in the same universe as X here, but IsProperMap.universally_closed does not have this restriction.

This is taken as the definition of properness in [N. Bourbaki, General Topology][bourbaki1966].