Proper maps (in the sense of topology)

Stream: Is there code for X?

[Oliver Nash]

Have I gone mad or do we really not have the definition of proper maps?

[Oliver Nash]

For example, is the following really missing:

import topology.separation

variables {α β : Type*} [topological_space α] [topological_space β] (f : α → β)

def is_proper_map := ∀ ⦃K⦄, is_compact K → is_compact (f⁻¹' K)

lemma continuous.is_proper_map_of_compact_of_t2 [compact_space α] [t2_space β] (h : continuous f):
  is_proper_map f :=
λ K hK, (hK.is_closed.preimage h).is_compact

[Heather Macbeth]

I have used related properties a number of times under the spelling tendsto cocompact at_top or tendsto cocompact cocompact.

[Adam Topaz]

There was some discussion along these lines before...

[Adam Topaz]

docs#cocompact_map

[Heather Macbeth]

Eg.
docs#tendsto_norm_cocompact_at_top
docs#filter.tendsto_cocompact_mul_left

[Oliver Nash]

OK I'll look into this. At the very least, someone should add the phrase "proper map" to some doc strings.

[Oliver Nash]

Thanks!

[Oliver Nash]

This is exactly what I need, thanks.

[Oliver Nash]

Here's the relevant PR anyway: #17107

[Junyan Xu]

There was an attempt at the universally closed definition

[Anatole Dedecker]

See also this discussion related to why docs#cocompact_map is not called proper_map

[Oliver Nash]

Thanks, @Anatole Dedecker that's a useful thread. Incidentally I think we should unbundle cocompact_map into is_cocompact_map like we have for is_open_map and is_closed_map.

[Jireh Loreaux]

If you want to unbundle it, that's fine, but please also leave the bundled version in place. These are the right morphisms I need for various things related to non-unital C star algebras. See, for example, the functorial property at the bottom of that file.

[Jireh Loreaux]

Note also that we have the statement that cocompact maps have the property you specify when the space is locally compact and Hausdorff. Otherwise they may not.

[Oliver Nash]

I have no plans to unbundle for now at least! I'm just going by my own made up guidelines that:

1. It is preferable not to bundle to save boilerplate and to make it possible to combine predicates without authoring new classes
2. The main exceptions to 1 are when the set of maps themselves are a primary object of study, or (often related) when we have important typeclass instances keyed off such a map

To be concrete, I was mostly motivated to make my remark above because I wanted to speak of a cocompact group homomorphism and I cannot conveniently do this with the classes we currently have (but I could if we just had is_cocompact_map analogous to is_open_map and is_closed_map).

[Oliver Nash]

Thank you for creating cocompact_map in the first place though: implementation details aside, it was just what I needed (and I may be wrong about the bundling anyway).

[Jireh Loreaux]

Makes sense. For things which are common enough and span multiple domains, unbundled versions can certainly be useful.