Easiest way to show an image is closed if almost compact

Stream: Is there code for X?

[Geoffrey Irving]

I have a function f : ℂ → ℂ analytic for r ≤ abs z, which converges to infinity at infinity (i.e., it has a pole, but I should only need topological properties here). What's the easiest way to show that f '' {z | r ≤ abs z} is closed? Fundamentally this is almost the image of a compact set, except that infinity is removed, but that's fine as f also approaches infinity.

In other words, I want

import Mathlib

lemma closed_image {f : ℂ → ℂ} {r : ℝ} (hf : ContinuousOn f {z | r ≤ Complex.abs z})
    (hi : Filter.Tendsto f (Filter.cocompact ℂ) (Filter.cocompact ℂ)) :
    IsClosed (f '' {z | r ≤ Complex.abs z}) := by
  sorry

I can do this with calculations, but it seems like there should be an easy abstract way to get this.

[Geoffrey Irving]

Better version:

lemma closed_image' {f : ℂ → ℂ} {s : Set ℂ} (hf : ContinuousOn f s) (hs : IsClosed s)
    (hi : Filter.Tendsto f (Filter.cocompact ℂ) (Filter.cocompact ℂ)) :
    IsClosed (f '' s) := by
  sorry

[Anatole Dedecker]

EDIT: this is correct, but already proven in docs#isProperMap_iff_tendsto_cocompact, so one should not use it directly.

The way I would do it is:
- $\mathbb{C}$ is compactly generated (because locally compact), so you just need to check that $f(S)\cap K$ is closed for any compact $K$
- $f(S) \cap K = f(S \cap f^{-1}(K))$
- $f$ is proper so the latter is compact as the image of a compact set

[Anatole Dedecker]

As I just mentioned here we don't have compactly generated spaces, but really we have everything to state all of this for (weakly) locally compact spaces, even though it is really about compactly generated spaces.

[Anatole Dedecker]

I have PRs to review before going to bed so if you or someone else wants to have fun with this please do! The cocompact assumption should be replaced by docs#IsProperMap (this is equivalent in this setting, but it's the right concept in general), and $\mathbb{C}$ by any docs#WeaklyLocallyCompactSpace

[Anatole Dedecker]

Wait, I am dumb (or tired, let's say tired)

[Anatole Dedecker]

I'm redoing the proof of docs#isProperMap_iff_tendsto_cocompact :face_palm:

[Anatole Dedecker]

So you should really use that and then docs#IsProperMap.isClosedMap

[Anatole Dedecker]

Hmmm, except you only have docs#ContinuousOn...

[Anatole Dedecker]

This sounds like a good reason to define IsProperMapOn, but in the mean time I should we should be able to circumvent that.

[Geoffrey Irving]

Yes, I’m not continuous everywhere unfortunately (f has a natural boundary of dimension 2 at radius = 1).

[Geoffrey Irving]

I think the IsProperMap machinery would lift straightforwardly but tediously to IsProperMapOn, but we don’t have that written down.

[Anatole Dedecker]

I'm working on a quick fix, but indeed the proper fix is IsProperMapOn. That shouldn't be too hard but a bit annoying maybe.

[Geoffrey Irving]

I’ll take a look at that.

[Anatole Dedecker]

Here's my proposal:

import Mathlib

open Filter Set

-- closed inducing is enough, should be replace/be used in the proof of `Homeomorph.isClosedMap`?
lemma ClosedEmbedding.isProperMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} (hf : ClosedEmbedding f) : IsProperMap f := by
  rw [isProperMap_iff_isClosedMap_and_compact_fibers]
  refine ⟨hf.continuous, hf.isClosedMap, fun y ↦ hf.isCompact_preimage isCompact_singleton⟩

-- This direction of `isProperMap_iff_tendsto_cocompact` requires no assumptions
lemma IsProperMap.tendsto_cocompact {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} (hf : IsProperMap f) :
    Tendsto f (cocompact X) (cocompact Y) :=
  hasBasis_cocompact.tendsto_right_iff.mpr fun _ hK ↦ (hf.isCompact_preimage hK).compl_mem_cocompact

lemma IsProperMap.comap_cocompact_eq {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} (hf : IsProperMap f) :
    comap f (cocompact Y) = cocompact X :=
  le_antisymm (comap_cocompact_le hf.continuous) hf.tendsto_cocompact.le_comap

lemma closed_image' {f : ℂ → ℂ} {s : Set ℂ} (hf : ContinuousOn f s) (hs : IsClosed s)
    (hi : Filter.Tendsto f (Filter.cocompact ℂ) (Filter.cocompact ℂ)) :
    IsClosed (f '' s) := by
  rw [continuousOn_iff_continuous_restrict] at hf
  rw [← range_restrict]
  suffices IsProperMap (s.restrict f) from this.isClosedMap.closed_range
  rw [isProperMap_iff_tendsto_cocompact, -- why is this slow???
      ← hs.closedEmbedding_subtype_val.isProperMap.comap_cocompact_eq]
  exact ⟨hf, hi.comp tendsto_comap⟩

[Anatole Dedecker]

The three lemmas before can be useful (especially the first one) so this experiment is not completely useless, but really I can't envision any good way to make this fit into the API without developping IsProperMapOn. Fortunately, proofs using filters are often really easy to reduce to subsets, and most of the proof in this file are very filter-y

[Geoffrey Irving]

I supposed I need IsClosedMap as well.

What's the right way to spell "t is closed relative to s"? I typically do s ∩ closure t ⊆ t, but this unfortunately mentions t twice.

import Mathlib
open Set Filter Function Topology Filter
variable {α : Type*} {β : Type*}
variable [TopologicalSpace α] [TopologicalSpace β]

/-- `f : α → β` is closed on `s : Set α` if it sends relatively closed sets to closed sets -/
def IsClosedMapOn (f : α → β) (s : Set α) : Prop :=
  ∀ t : Set α, t ⊆ s → s ∩ closure t ⊆ t → IsClosed (f '' t)

I suppose the alternative is just IsClosedMap (s.restrict f).

[Anatole Dedecker]

Hmmmm, I should have anticipated this, this is starting to turn into a really big refactor which we may want to think about twice before doing… We have multiple ways to talk about being relatively closed subsets, I’d say the easiest one to deal with are "preimage by Subtype.val is closed" and "cluster points in s of principal t are in t"

[Geoffrey Irving]

I may skip it for now, and if it’s okay I’ll PR your lemmas above.

[Anatole Dedecker]

Maybe the best for now is not to make any new definition for closed maps and use the restriction, maybe adding one or two lemmas about equivalent conditions for a restriction to be closed, and only focusing on proper maps

[Anatole Dedecker]

You can also use what I did above indeed. I’m just not sure how best to state closure_image' for the library