continuous maps vanishing at infinity

Stream: general

[Jireh Loreaux]

I'm looking to define the type of continuous maps vanishing at infinity. Does this seem like a reasonable start? I don't want to get too deep if I'm heading in the wrong direction somehow.

import topology.continuous_function.bounded

/-!
# Continuous functions vanishing at infinity

The type of continuous functions vanishing at infinity. When the domain is a locally compact space,
this type has nice properties. When the domain is compact `C₀(α, β) ≃ C(α, β)` via the identity map.
-/
universes u v

variables {F : Type*} {α : Type u} {β : Type v}

open_locale bounded_continuous_function

/-- `C₀(α, β)` is the type of continuous functions `α → β` which vanish at infinity from a
topological space to a metric space with a zero element. -/
structure zero_at_infty_continuous_map (α : Type u) (β : Type v)
  [topological_space α] [has_zero β] [metric_space β] extends continuous_map α β :
  Type (max u v) :=
(zero_at_infty' : ∀ ε > 0, ∃ K : set α,
  is_compact K ∧ ∀ x ∉ K, to_fun x ∈ metric.closed_ball (0 : β) ε)

localized "notation `C₀(` α `, ` β `)` := zero_at_infty_continuous_map α β" in zero_at_infty

/-- `zero_at_infty_continuous_map_class F α β` states that `F` is a type of continuous maps which
vanish at infinity.

You should also extend this typeclass when you extend `zero_at_infty_continuous_map`. -/
class zero_at_infty_continuous_map_class (F α β : Type*) [topological_space α] [has_zero β]
  [metric_space β] extends continuous_map_class F α β :=
(zero_at_infty (f : F) : ∀ ε > 0, ∃ K : set α,
  is_compact K ∧ ∀ x ∉ K, f x ∈ metric.closed_ball (0 : β) ε)

export zero_at_infty_continuous_map_class (zero_at_infty)

namespace zero_at_infty
section basics
variables [topological_space α] [has_zero β] [metric_space β] [metric_space γ]

instance : zero_at_infty_continuous_map_class C₀(α, β) α β :=
{ coe := λ f, f.to_fun,
  coe_injective' := λ f g h, by { obtain ⟨⟨_, _⟩, _⟩ := f, obtain ⟨⟨_, _⟩, _⟩ := g, congr' },
  map_continuous := λ f, f.continuous_to_fun,
  zero_at_infty := λ f, f.zero_at_infty' }

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

instance [zero_at_infty_continuous_map_class F α β] : has_coe_t F C₀(α, β) :=
⟨λ f, { to_fun := f, continuous_to_fun := map_continuous f, zero_at_infty' := zero_at_infty f }⟩

@[simp] lemma coe_to_continuous_fun (f : C₀(α, β)) : (f.to_continuous_map : α → β) = f := rfl

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because it is a composition of multiple projections. -/
def simps.apply (h : C₀(α, β)) : α → β := h

initialize_simps_projections zero_at_infty_continuous_map (to_continuous_map_to_fun → apply)

variables [zero_at_infty_continuous_map_class F α β]

protected lemma bounded (f : F) : ∃ C, ∀ x y : α, dist ((f : α → β) x) (f y) ≤ C :=
begin
  obtain ⟨K : set α, hK₁, hK₂⟩ := zero_at_infty (f : F) (1 : ℝ) zero_lt_one,
  obtain ⟨C, hC⟩ := (hK₁.image (map_continuous f)).bounded.subset_ball (0 : β),
  refine ⟨max C 1 + max C 1, (λ x y, _)⟩,
  have : ∀ x, f x ∈ metric.closed_ball (0 : β) (max C 1),
  { intro x,
    by_cases hx : x ∈ K,
    { exact le_trans (metric.mem_closed_ball.mp $ hC ⟨x, hx, rfl⟩) (le_max_left _ _) },
    { exact le_trans (metric.mem_closed_ball.mp $ hK₂ x hx) (le_max_right _ _) } },
  exact  (dist_triangle (f x) 0 (f y)).trans
    (add_le_add (metric.mem_closed_ball.mp $ this x) (metric.mem_closed_ball'.mp $ this y)),
end

instance : bounded_continuous_map_class C₀(α, β) α β :=
{ coe := λ f, f.to_fun,
  coe_injective' := λ f g h, by { obtain ⟨⟨_, _⟩, _⟩ := f, obtain ⟨⟨_, _⟩, _⟩ := g, congr' },
  map_continuous := λ f, f.continuous_to_fun,
  map_bounded := λ f, zero_at_infty.bounded f }

[Yaël Dillies]

• You should use \{{}} around \e and x.
• The final instance should be stated in terms of the _class, not the type of morphisms.
• You can drop the simps projection stuff as we haven't yet decided on the correct way to use it for homs.
• I know we use the notation C(\a, \b) for continuous maps but even though it's standard literature notation I think that's a shame and that we should change it to \a ->C \b or something more mathlib-like. So here I'd suggest using \a ->C\_0 \b or similar.
• Ideally, we would have a type of bounded maps in which case your bounded lemma would turn into an instance zero_at..._class -> bounded_map_class. Leave that for now I'd say.

[Yaël Dillies]

This is the first time I see someone \ {Anne, I} following closely the hom refactor so I'm very happy overall :)

[Jireh Loreaux]

The ⦃⦄ means semi-implicit argument, right? Why do I want that here? I've worked with these very little, and it seems that I can't pass it an explicit value for the argument (but I'm probably doing it wrong). Where is the documentation for these?

[Yaël Dillies]

You can find an explanation in #tpil. Have a look at how they're used in docs#set.pairwise and docs#convex

[Jireh Loreaux]

oh, I see, you want this:

∀ ⦃ε : ℝ⦄, (0 < ε) → ∃ K : set α,  is_compact K ∧ ∀ ⦃x : α⦄, (x ∉ K) → to_fun x ∈ metric.closed_ball (0 : β) ε)

not this:

∀ ⦃ε > 0⦄, ∃ K : set α, is_compact K ∧ ∀ ⦃x ∉ K⦄, f x ∈ metric.closed_ball (0 : β) ε)

[Jireh Loreaux]

That makes way more sense. I was confused trying to figure out how ε and x were supposed to be inferred in the second one.

[Heather Macbeth]

@Jireh Loreaux What about using docs#filter.cocompact ?

[Heather Macbeth]

structure zero_at_infty_continuous_map (α : Type u) (β : Type v)
  [topological_space α] [has_zero β] [metric_space β] extends continuous_map α β :
  Type (max u v) :=
(zero_at_infty' : tendsto to_fun (cocompact α) (𝓝 0))

[Jireh Loreaux]

Yes, much nicer. Good point.

[Jireh Loreaux]

In that case, I guess I'll just relax [metric_space β] to [topological_space β].

[Jireh Loreaux]

I guess we don't have any non-unital analogue of topological_ring, do we? I could just have has_continuous_add and has_continuous_mul separately I suppose; is that the right approach?

[Johan Commelin]

Or generalize the definition of topological_ring?

[Johan Commelin]

It doesn't need to assume that the underlying type actually has a ring structure, right?

[Jireh Loreaux]

Well, for non-unital semirings, sure, it would generalize just fine. But if you just relax semiring to non_unital_semiring as is, then the (perhaps minor) problem is that we don't have "has_continuous_neg" and for a ring (not a semiring), the way we get this right now is by multiplying by -1 and using has_continuous_mul. All this would still be fine if it weren't for non_unital_ring, where you still want "has_continuous_neg" but there's no way to get it for free since you don't have -1. I don't see an immediately easy way to fix that.

[Jireh Loreaux]

I guess maybe the way to deal with this is to have topological_semiring (which only requires non_unital_semiring, maybe even non_unital_non_assoc_semiring) and is just the combination of has_continuous_add and has_continuous_mul. Then separately have topological_ring (which only requires non_unital_ring or maybe non_unital_non_assoc_ring) which extends topological_semiring by adding the currently nonexistent has_continuous_neg.

[Yaël Dillies]

It looks everything would be solved by having has_continuous_neg and an instance has_continuous_mul → has_continuous_neg when working over a group.

[Jireh Loreaux]

you mean over a ring?

[Yaël Dillies]

Yes!

[Yaël Dillies]

topological_ring := topological_semiring + has_continuous_neg sounds like a good idea too.

[Jireh Loreaux]

So, I am defining topological_semiring as above along with topological_ring (with a type class argument of non_unital_non_assoc_ring). I can write the instance of [non_assoc_ring R] [has_continuous_mul R] → has_continuous_neg R, but then it would be nice if Lean could automatically infer this when creating instances of topological_ring when possible. How do I write the definition of topological_ring to (try to) do this automatically?

[Jireh Loreaux]

@Yaël Dillies

[Yaël Dillies]

Long story short: Wait for Lean 4

[Jireh Loreaux]

:cry: any place I can read the long version of this story?