# 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.

## 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

## 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

source
structure IsProperMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) extends Continuous f :
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 `ℱ`.

Instances For

source
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.

source
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.

source
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.

source
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.

source
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
source
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`.

source
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} (hg : IsProperMap g) (hf : IsProperMap f) :
IsProperMap (g ∘ f)

The composition of two proper maps is proper.

source
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.

source
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.

source
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.

source
theorem IsProperMap.prodMap {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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
@[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.

source
theorem IsHomeomorph.isProperMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) :
IsProperMap f
source
@[simp]
theorem isProperMap_id {X : Type u_1} [TopologicalSpace X] :
IsProperMap id

The identity is proper.

source
theorem Topology.IsClosedEmbedding.isProperMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) :
IsProperMap f

A closed embedding is proper.

source
theorem IsClosed.isProperMap_subtypeVal {X : Type u_1} [TopologicalSpace X] {C : Set X} (hC : IsClosed C) :
IsProperMap Subtype.val

The coercion from a closed subset is proper.

source
theorem IsProperMap.restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {C : Set X} (hf : IsProperMap f) (hC : IsClosed C) :
IsProperMap fun (x : ↑C) => f ↑x

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

source
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.

source
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`.

source
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.

source
theorem isProperMap_const_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] (y : Y) :
(IsProperMap fun (x : X) => y) ↔ CompactSpace X

A constant map to a T₁ space is proper if and only if its domain is compact.

source
theorem isProperMap_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [h : CompactSpace X] [T1Space Y] (y : Y) :
IsProperMap fun (x : X) => y
source
theorem isProperMap_fst_of_compactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] :
IsProperMap Prod.fst

If `Y` is a compact topological space, then `Prod.fst : X × Y → X` is a proper map.

source
theorem isProperMap_snd_of_compactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] :
IsProperMap Prod.snd

If `X` is a compact topological space, then `Prod.snd : X × Y → Y` is a proper map.

source
theorem isClosedMap_fst_of_compactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] :
IsClosedMap Prod.fst

If `Y` is a compact topological space, then `Prod.fst : X × Y → X` is a closed map.

source
theorem isClosedMap_snd_of_compactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] :
IsClosedMap Prod.snd

If `X` is a compact topological space, then `Prod.snd : X × Y → Y` is a closed map.

source
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.