HepLean Documentation

Mathlib.Topology.Maps.Proper.Basic

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 #

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 #

References #

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

Instances For
    source
    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 ℱ.

    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} (hf : IsProperMap f) (hg : IsProperMap g) :
    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
    @[deprecated IsProperMap.prodMap]
    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)

    Alias of IsProperMap.prodMap.

    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 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
    @[deprecated IsClosedEmbedding.isProperMap]
    theorem isProperMap_of_closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) :
    IsProperMap f

    Alias of IsClosedEmbedding.isProperMap.

    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
    @[deprecated IsClosed.isProperMap_subtypeVal]
    theorem isProperMap_subtype_val_of_closed {X : Type u_1} [TopologicalSpace X] {C : Set X} (hC : IsClosed C) :
    IsProperMap Subtype.val

    Alias of IsClosed.isProperMap_subtypeVal.

    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
    @[deprecated IsProperMap.restrict]
    theorem isProperMap_restr_of_proper_of_closed {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

    Alias of IsProperMap.restrict.

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

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

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