proper maps

Stream: maths

[Jireh Loreaux]

I'm going to define proper maps (those for which preimages of compact set are compact). Should I have it extend continuous_map, or just have a bare proper_map and then separately a proper_continuous_map?

[Yaël Dillies]

docs#spectral_map :grinning:

[Patrick Massot]

Jireh, this isn't the right definition of proper maps in general

[Yaël Dillies]

@Johan Commelin, you told me that my spectral maps were called proper maps in the real world. Are you sure there is no difference? Proper maps seem to have preimages of compact be compact while spectral maps have preimages of compact opens be compact open.

[Reid Barton]

I was going to say "shouldn't proper actually mean universally closed" but I don't remember the reason. But I'm more interested in whether proper-but-not-necessarily-continuous maps actually show up in math somewhere--I thought about this class of maps for a little while and if there's something written down about them, I might find it helpful.

[Patrick Massot]

In Bourbaki, proper means continuous and universally closed.

[Reid Barton]

Right, AFAIK everyone includes "continuous" in the meaning of "proper". I just meant that "proper-but-not-continuous" seems like a potentially useful concept, but it would need another name. (example: the "identity" map $[0, 1) \amalg \{1\} \to [0, 1]$ is continuous but not proper, while its inverse is proper-but-not-continuous)

[Andrew Yang]

Yaël Dillies said:

Johan Commelin, you told me that my spectral maps were called proper maps in the real world. Are you sure there is no difference? Proper maps seem to have preimages of compact be compact while spectral maps have preimages of compact opens be compact open.

I thought they were called quasi-compact maps (c.f. stacks#005A)

[Johan Commelin]

Hmmz, I retract my claim.

[Adam Topaz]

@Reid Barton how about "preproper" for a name? (semiserious)

[Reid Barton]

It sounds good if we can't find an existing term for the same concept.

[Reid Barton]

Apparently in my notes I used the word "prim", but I don't think I got it from anywhere.

[Reid Barton]

preproper reminds me a bit of prepromorphisms

[Jireh Loreaux]

I thought Patrick's point was that the preimage of compact definition is the wrong version of proper map. Stacks does mention quasi-compact.

[Ruben Van de Velde]

Adam Topaz said:

Reid Barton how about "preproper" for a name? (semiserious)

Semiproper? (preserious suggestion)

[Patrick Massot]

Jireh, Reid is talking about both issues.

[Jireh Loreaux]

My point is only that if, for example, we have proper = continuous and universally closed, and quasi-compact (?) = continuous and preimages of compact are compact, then it would be a bit strange to call preproper = preimages of compact are compact, because it wouldn't match (same goes for any substitute for preproper involving the word proper).

[Reid Barton]

Right, and I don't know what the "correct" definition of "proper-but-not-continuous" should be

[Heather Macbeth]

@Jireh Loreaux I think the definition should be tendsto f cocompact cocompact, but maybe you've already figured this out :)

[Jireh Loreaux]

Yes, indeed. That's actually what I was planning on (more power to the filter library!) since I'm using it for functions vanishing at infinity anyway :smile:. The whole point is basically to eventually get the C₀ functor.

[Damiano Testa]

Wouldn't universally_closed be "proper-but-not-continuous"?
Re-reading the conversation, I think that I misunderstood what was meant by "proper-but-not-continuous"!

[Antoine Chambert-Loir]

Bourbaki is slightly inconsistent on the definition of proper. It is defined in Topologie générale, chapter III.
As @Patrick Massot said, it means continuous and universally closed and they show that it is equivalent with various stuff, such as continuous, closed and fibers are quasi-compact. For locally compact (Hausdorff) spaces, this notion falls back to the fact that the preimages of compact sets are compact.

Similarly, there are separated maps $f \colon X \to Y$, those for which the diagonal $X \to Y \times_X Y$ is a closed map. They are defined in Topologie algébrique, following a similar definition in algebraic geometry.
According to whether one imposes to compact sets to Hausdorff, it makes sense to require proper maps to be separated.

The basic results are elegant, their proofs are quite direct and their formalization should work without too much trouble.

[Jireh Loreaux]

So, I think I would be interested in defining what I'm calling cocompact continuous maps, although I haven't seen these anywhere ever. These are continuous maps f : α → β which satisfy tendsto f (cocompact α) (cocompact β). Quasi-compact maps (continuous with preimages of compact sets compact) are cocompact continuous maps, and the converse is true when the codomain is Hausdorff.

I think there is a counterexample to the converse when the codomain is not Hausdorff, but I haven't checked the details carefully: the identity map from ℝ to the "line with two origins" (this map misses one of the origins); I think this is cocompact and continuous but the pre-image of the closed (and compact) interval [-1,1] (which includes the origin not in the range) is [-1,0) ∪ (0,1] which is not compact. Likely someone else can come up with an easier counterexample, but I never work with non-Hausdorff spaces.

The reason I care about such maps is that they are exactly the things which play nice with the type β →C₀ γ of continuous maps which vanish at infinity (see #12907). In particular, if f : β →C₀ γ and g : α → β is a cocompact continuous map, then f ∘ g : α →C₀ γ.

Here is the relevant introductory API for these maps. Please indicate if you think this does not belong in mathlib.

/-
Copyright (c) 2022 Jireh Loreaux. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jireh Loreaux
-/
import topology.continuous_function.basic

/-!
# Cocompact continuous maps

The type of *cocompact continuous maps* are those which tend to the cocompact filter on the
codomain along the cocompact filter on the domain. When the domain and codomain are Hausdorff, this
is equivalent to many other conditions, including that preimages of compact sets are compact. -/

universes u v w

open filter set

/-- A *cocompact continuous map* is a continuous function between topological spaces which
tends to the cocompact filter along the cocompact filter. Functions for which preimgaes of compact
sets are compact always satisfy this property, and the converse holds for cocompact continuous maps
when the codomain is Hausdorff (see `cocompact_map.tendsto_of_forall_preimage` and
`cocompact_map.compact_preimage`) -/
structure cocompact_map (α : Type u) (β : Type v) [topological_space α] [topological_space β]
  extends continuous_map α β : Type (max u v) :=
(cocompact_tendsto' : tendsto to_fun (cocompact α) (cocompact β))

/-- `cocompact_map_class F α β` states that `F` is a type of cocompact continuous maps.

You should also extend this typeclass when you extend `cocompact_map`. -/
class cocompact_map_class (F : Type*) (α β : out_param $ Type*) [topological_space α]
  [topological_space β] extends continuous_map_class F α β :=
(cocompact_tendsto (f : F) : tendsto f (cocompact α) (cocompact β))

namespace cocompact_map_class

variables {F α β : Type*} [topological_space α] [topological_space β]
  [cocompact_map_class F α β]

instance : has_coe_t F (cocompact_map α β) := ⟨λ f, ⟨f, cocompact_tendsto f⟩⟩

end cocompact_map_class

namespace cocompact_map

section basics
variables {α β γ δ : Type*} [topological_space α] [topological_space β] [topological_space γ]
  [topological_space δ]

instance : cocompact_map_class (cocompact_map α β) α β :=
{ coe := λ f, f.to_fun,
  coe_injective' := λ f g h, by { obtain ⟨⟨_, _⟩, _⟩ := f, obtain ⟨⟨_, _⟩, _⟩ := g, congr' },
  map_continuous := λ f, f.continuous_to_fun,
  cocompact_tendsto := λ f, f.cocompact_tendsto' }

export cocompact_map_class (cocompact_tendsto)

/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
directly. -/
instance : has_coe_to_fun (cocompact_map α β) (λ _, α → β) := fun_like.has_coe_to_fun

@[simp] lemma coe_to_continuous_fun {f : cocompact_map α β} :
  (f.to_continuous_map : α → β) = f := rfl

@[ext] lemma ext {f g : cocompact_map α β} (h : ∀ x, f x = g x) : f = g := fun_like.ext _ _ h

/-- Copy of a `cocompact_map` with a new `to_fun` equal to the old one. Useful
to fix definitional equalities. -/
protected def copy (f : cocompact_map α β) (f' : α → β) (h : f' = f) : cocompact_map α β :=
{ to_fun := f',
  continuous_to_fun := by {rw h, exact f.continuous_to_fun},
  cocompact_tendsto' := by { simp_rw h, exact f.cocompact_tendsto' } }

@[simp] lemma coe_mk (f : C(α, β)) (h : tendsto f (cocompact α) (cocompact β)) :
  ⇑(⟨f, h⟩ : cocompact_map α β) = f := rfl

section
variable (α)
/-- The identity as a cocompact continuous map. -/
protected def id : cocompact_map α α := ⟨continuous_map.id _, tendsto_id⟩
@[simp] lemma coe_id : ⇑(cocompact_map.id α) = id := rfl
end

@[simp] lemma id_apply (a : α) : continuous_map.id α a = a := rfl

instance : inhabited (cocompact_map α α) := ⟨cocompact_map.id α⟩

/-- The composition of cocompact continuous maps, as a cocompact continuous map. -/
def comp (f : cocompact_map β γ) (g : cocompact_map α β) : cocompact_map α γ :=
⟨f.to_continuous_map.comp g, (cocompact_tendsto f).comp (cocompact_tendsto g)⟩

@[simp] lemma coe_comp (f : cocompact_map β γ) (g : cocompact_map α β) :
  ⇑(comp f g) = f ∘ g := rfl

@[simp] lemma comp_apply (f : cocompact_map β γ) (g : cocompact_map α β) (a : α) :
  comp f g a = f (g a) := rfl

@[simp] lemma comp_assoc (f : cocompact_map γ δ) (g : cocompact_map β γ)
  (h : cocompact_map α β) : (f.comp g).comp h = f.comp (g.comp h) := rfl

@[simp] lemma id_comp (f : cocompact_map α β) : (cocompact_map.id _).comp f = f :=
ext $ λ _, rfl

@[simp] lemma comp_id (f : cocompact_map α β) : f.comp (cocompact_map.id _) = f :=
ext $ λ _, rfl

lemma tendsto_of_forall_preimage {f : α → β} (h : ∀ s, is_compact s → is_compact (f ⁻¹' s)) :
  tendsto f (cocompact α) (cocompact β) :=
λ s hs, match mem_cocompact.mp hs with ⟨t, ht, hts⟩ :=
  mem_map.mpr (mem_cocompact.mpr ⟨f ⁻¹' t, h t ht, by simpa using preimage_mono hts⟩) end

/-- If the codomain is Hausdorff, preimages of compact sets are compact under a cocompact
continuous map. -/
lemma compact_preimage [t2_space β] (f : cocompact_map α β) ⦃s : set β⦄ (hs : is_compact s) :
  is_compact (f ⁻¹' s) :=
begin
  obtain ⟨t, ht, hts⟩ := mem_cocompact'.mp (by simpa only [preimage_image_preimage, preimage_compl]
    using mem_map.mp (cocompact_tendsto f $ mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr
    (image_preimage_subset f _)⟩)),
  exact compact_of_is_closed_subset ht (hs.is_closed.preimage $ map_continuous f)
    (by simpa using hts),
end

end basics

end cocompact_map

[Yaël Dillies]

Keep up the good hom, Jireh!

[Jireh Loreaux]

Since there didn't seem to be an strenuous objections: #12938

[Anatole Dedecker]

I've just opened #6005 (still WIP) setting up the basic theory of proper maps (without the "separated" assumption that Antoine mentionned above). Right now it just contains the equivalence universal closedness and the more concrete characterizations, I'll also add the characterization in locally compact spaces and that will make a nice first PR on the subject.

Now, the real reason I wanted to revive this thread is that I actually found some interesting (I think ?) simplifications to the proofs in Bourbaki, and I didn't want my thoughts to be "lost" in mathlib comments. In particular, this lemma says that, for proving that $f : X\to Y$ you only have to check universal closedness for one space, namey Filter X with the topology docs#Filter.instTopologicalSpaceFilter !

[Patrick Massot]

Nice!

[Yury G. Kudryashov]

Nice to see that my addition of topology on Filter X found some application!

[Anatole Dedecker]

Indeed, thanks for that! The idea was that Bourbaki uses this "topological space defined by F : FIlter X" where you add one point to the space such that converging to that point is exactly converging to the filter. That sounded annoying since we don't have that, but I realized that this is exactly range pure \union {F} with the induced topology from Filter X (okay, as long as F is not already a pure filter).

[Adam Topaz]

Does it work with Ultrafilter X instead of Filter X?

[Anatole Dedecker]

Oh probably, let me try

[Yury G. Kudryashov]

Should we add this construction and make docs#OnePoint a special case?

[Adam Topaz]

Just asking because Ultrafilter X is the Stone-Cech compactification of X as a discrete space.

[Kevin Buzzard]

ultrafilter is the variety, filter is the scheme (more points but you don't need them in most cases)

[Anatole Dedecker]

Adam Topaz said:

Just asking because Ultrafilter X is the Stone-Cech compactification of X as a discrete space.

Oh of course, that would probably give a more satisfying explanation

[Anatole Dedecker]

Btw, should the topology on Ultrafilter be defined as the one coming from Filter? I guess there's some possible golfing here.

[Anatole Dedecker]

Indeed it does work with Ultrafilter X. I guess it should also work for StoneCech X, which is probably even more satisfying, but I've done enough general topology for today.

[Patrick Massot]

Anatole Dedecker said:

The idea was that Bourbaki uses this "topological space defined by F : FIlter X" where you add one point to the space such that converging to that point is exactly converging to the filter. That sounded annoying since we don't have that

Of course we have that! This is docs#nhdsAdjoint. It's crucial because it left-adjoint to docs#nhds.

[Anatole Dedecker]

I was talking about the version that adds a "point at infinity", but we can probably relate it to nhdsAdjoint.

[Adam Topaz]

BTW, using (ultra)filter looks to me like the topological analogue of the valuative criterion for properness from algebraic geometry.

[Yury G. Kudryashov]

Probably, you can do the "point at infinity" using map, nhdsAdjoint, and sup or inf (I always forget which one is which).

[Anatole Dedecker]

#6005 is now ready for review. I've thought about it a bit and the current proof can't really work for the compactification because I do use the specific form of neighborhoods in Filter X/Ultrafilter X. I haven't thought about it a lot more so I'm not saying it's necessarily false, just that I'm sticking with the filter/ultrafilter version for the sake of simplicity.

[Yury G. Kudryashov]

Am I right that in

theorem IsCompact.preimage_continuous {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X]
    [T2Space Y] {f : X → Y} (hf : Continuous f) {s : Set Y} (hs : IsCompact s) :
    IsCompact (f ⁻¹' s) :=
  (hs.isClosed.preimage hf).isCompact

one can't drop [T2Space Y]? What's a counterexample?

[Anatole Dedecker]

Take $Y = \{0, 1\}$ the Sierpinski space (docs#sierpinskiSpace), $X = [0, 1]$, $U = (0, 1)$, and $f = \mathbf{1}_U : X \to Y$. $f$ is continuous, but the preimage of the compact $\{1\}$ is $U$ which is not compact.