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

`f`

is closed and has compact fibers.`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.- 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

Definition of proper maps. See also `isClosedMap_iff_clusterPt`

for a related criterion
for closed maps.

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 `ℱ`

.

- 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

By definition, a proper map is continuous.

A proper map is closed.

Characterization of proper maps by ultrafilters.

If `f`

is proper and converges to `y`

along some ultrafilter `𝒰`

, then `𝒰`

converges to some
`x`

such that `f x = y`

.

The composition of two proper maps is proper.

If the composition of two continuous functions `g ∘ f`

is proper and `f`

is surjective,
then `g`

is proper.

If the composition of two continuous functions `g ∘ f`

is proper and `g`

is injective,
then `f`

is proper.

If the composition of two continuous functions `f : X → Y`

and `g : Y → Z`

is proper
and `Y`

is T2, then `f`

is proper.

A binary product of proper maps is proper.

Any product of proper maps is proper.

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.

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

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

A injective continuous and closed map is proper.

A homeomorphism is proper.

The identity is proper.

A closed embedding is proper.

The coercion from a closed subset is proper.

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

The range of a proper map is closed.

Version of `isProperMap_iff_isClosedMap_and_compact_fibers`

in terms of `cofinite`

and
`cocompact`

. Only works when the codomain is `T1`

.

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

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.

Version of `isProperMap_iff_isCompact_preimage`

in terms of `cocompact`

.

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.

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.

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.

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