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 Hausdorff compactly generated space is proper if and only if it is continuous and preimages of compact sets are compact. This is in particular true if the space is locally compact or sequential.
• 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".

Concerning isProperMap_iff_isCompact_preimage, this result should be the only one needed to link the definition of a proper map and the criteria "preimage of compact sets are compact", however the notion of compactly generated space is not yet in Mathlib (TODO) so it is used as an intermediate result to prove WeaklyLocallyCompactSpace.isProperMap_iff_isCompact_preimage and SequentialSpace.isProperMap_iff_isCompact_preimage. In the future those should be inferred by typeclass inference.

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 compactly generated 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.isClosed_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.

@[deprecated IsProperMap.isClosed_range]

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)

Alias of IsProperMap.isClosed_range.

---

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] (compactlyGenerated : ∀ (s : Set Y), IsClosed s ↔ ∀ ⦃K : Set Y⦄, IsCompact K → IsClosed (s ∩ K)) : IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)

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

This result should be the only one needed to link the definition of a proper map and the criteria "preimage of compact sets are compact", but the notion of compactly generated space is not yet in Mathlib (TODO) so we use it as an intermediate result to prove WeaklyLocallyCompactSpace.isProperMap_iff_isCompact_preimage and SequentialSpace.isProperMap_iff_isCompact_preimage. In the future those should be inferred by typeclass inference.

theorem compactlyGenerated_of_weaklyLocallyCompactSpace {X : Type u_1} [TopologicalSpace X] [T2Space X] [WeaklyLocallyCompactSpace X] {s : Set X} : IsClosed s ↔ ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)

A locally compact space is compactly generated.

theorem WeaklyLocallyCompactSpace.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.

This result is a direct consequence of isProperMap_iff_isCompact_preimage, because any Hausdorff and weakly locally compact space is compactly generated. In the future it should be inferred by typeclass inference, however compactly generated spaces are not yet in Mathlib (TODO), therefore we also add this theorem.

theorem compactlyGenerated_of_sequentialSpace {X : Type u_1} [TopologicalSpace X] [T2Space X] [SequentialSpace X] {s : Set X} : IsClosed s ↔ ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)

A sequential space is compactly generated.

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

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

This result is a direct consequence of isProperMap_iff_isCompact_preimage, because any Hausdorff and sequential space is compactly generated. In the future it should be inferred by typeclass inference, however compactly generated spaces are not yet in Mathlib (TODO), therefore we also add this theorem.

theorem isProperMap_iff_tendsto_cocompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [T2Space Y] (compactlyGenerated : ∀ (s : Set Y), IsClosed s ↔ ∀ ⦃K : Set Y⦄, IsCompact K → IsClosed (s ∩ K)) : IsProperMap f ↔ Continuous f ∧ Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)

Version of isProperMap_iff_isCompact_preimage in terms of cocompact.

theorem WeaklyLocallyCompactSpace.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 WeaklyLocallyCompactSpace.isProperMap_iff_isCompact_preimage in terms of cocompact.

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

Version of SequentialSpace.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.