Proper maps: compact domains, composition with homeomorphisms, products and pullbacks

Composing with a homeomorphism on either side neither creates nor destroys properness, in the pattern of Mathlib's Homeomorph.comp_isOpenMap_iff.

Mathlib's IsProperMap.prodMap says that a product of two proper maps is proper. This file proves the converse: if Prod.map f g is proper and the source of g is nonempty, then f is proper, and symmetrically. No separation axiom is needed. An ultrafilter on the source of f along which f converges is pushed into the product along a slice x ↦ (x, z), and a limit of the pushed ultrafilter projects to a limit of the original one.

The nonemptiness hypotheses cannot be dropped: a map out of an empty space is proper, so Prod.map f g is proper for every f when the source of g is empty.

Main declarations

• IsProperMap.compactSpace and IsProperMap.sigmaCompactSpace: the domain of a proper map to a compact (respectively sigma-compact) space is compact (respectively sigma-compact).
• Homeomorph.comp_isProperMap_iff and Homeomorph.comp_isProperMap_iff': properness is invariant under composition with a homeomorphism.
• IsProperMap.of_prodMap_left and IsProperMap.of_prodMap_right: the factors of a proper product map with nonempty sources are proper.
• isProperMap_prodMap_iff: for nonempty sources, Prod.map f g is proper exactly when f and g are.
• IsProperMap.of_isEmbedding_of_range_eq: the pullback of a proper map along an embedding of its codomain is proper. This is Mathlib's IsProperMap.restrictPreimage, stated for a square of embeddings rather than for subtypes.
• Continuous.isClosedEmbedding_fst_prod: a parameter-preserving map (p, x) ↦ (p, G (p, x)) with injective slices, compact second factor and Hausdorff target is a closed embedding.

@[simp]

theorem Homeomorph.comp_isProperMap_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Z → X} : IsProperMap (⇑h ∘ f) ↔ IsProperMap f

Postcomposing with a homeomorphism neither creates nor destroys properness.

@[simp]

theorem Homeomorph.comp_isProperMap_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Y → Z} : IsProperMap (f ∘ ⇑h) ↔ IsProperMap f

Precomposing with a homeomorphism neither creates nor destroys properness.

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

The domain of a proper map to a compact space is compact. No separation axiom is needed.

theorem IsProperMap.sigmaCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [SigmaCompactSpace Y] (hf : IsProperMap f) : SigmaCompactSpace X

The domain of a proper map to a sigma-compact space is sigma-compact. No separation axiom is needed.

theorem IsProperMap.of_prodMap_left {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} [Nonempty Z] (h : IsProperMap (Prod.map f g)) : IsProperMap f

If a product map Prod.map f g is proper and the source of g is nonempty, then f is proper.

theorem IsProperMap.of_prodMap_right {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} [Nonempty X] (h : IsProperMap (Prod.map f g)) : IsProperMap g

If a product map Prod.map f g is proper and the source of f is nonempty, then g is proper.

@[simp]

theorem isProperMap_prodMap_iff {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} [Nonempty X] [Nonempty Z] : IsProperMap (Prod.map f g) ↔ IsProperMap f ∧ IsProperMap g

For nonempty sources, a product map Prod.map f g is proper exactly when both f and g are proper.

theorem IsProperMap.of_isEmbedding_of_range_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] {f' : X' → Y'} {i : X' → X} {j : Y' → Y} (hf : IsProperMap f) (hi : Topology.IsEmbedding i) (hj : Topology.IsEmbedding j) (hcomm : f ∘ i = j ∘ f') (hrange : Set.range i = f ⁻¹' Set.range j) : IsProperMap f'

The pullback of a proper map along an embedding is proper. If f ∘ i = j ∘ f', where i and j are embeddings and the range of i is the preimage under f of the range of j, then f' is proper.

theorem Continuous.isClosedEmbedding_fst_prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {P : Type u_5} [TopologicalSpace P] [CompactSpace X] [T2Space Y] {G : P × X → Y} (hG : Continuous G) (hinj : ∀ (p : P), Function.Injective fun (x : X) => G (p, x)) : Topology.IsClosedEmbedding fun (q : P × X) => (q.1, G q)

A parameter-preserving map (p, x) ↦ (p, G (p, x)) whose slices are injective, from a product with a compact second factor to a Hausdorff space, is a closed embedding. Its image is the projection along the compact factor of a closed set, so it is closed. This applies to the track of an isotopy of a compact space, run over any parameter space.