Zulip Chat Archive

Stream: general

Topic: continuous maps vanishing at infinity


Jireh Loreaux (Mar 15 2022 at 14:59):

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 (Mar 15 2022 at 15:08):

  • 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 (Mar 15 2022 at 15:09):

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

Jireh Loreaux (Mar 15 2022 at 16:11):

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 (Mar 15 2022 at 16:17):

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

Jireh Loreaux (Mar 15 2022 at 16:36):

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 (Mar 15 2022 at 16:37):

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 (Mar 15 2022 at 16:38):

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

Heather Macbeth (Mar 15 2022 at 16:40):

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 (Mar 15 2022 at 16:41):

Yes, much nicer. Good point.

Jireh Loreaux (Mar 15 2022 at 17:14):

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

Jireh Loreaux (Mar 16 2022 at 14:40):

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 (Mar 16 2022 at 15:03):

Or generalize the definition of topological_ring?

Johan Commelin (Mar 16 2022 at 15:03):

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

Jireh Loreaux (Mar 16 2022 at 17:48):

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 (Mar 16 2022 at 17:52):

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 (Mar 16 2022 at 17:59):

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 (Mar 16 2022 at 18:00):

you mean over a ring?

Yaël Dillies (Mar 16 2022 at 18:00):

Yes!

Yaël Dillies (Mar 16 2022 at 18:01):

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

Jireh Loreaux (Mar 18 2022 at 19:31):

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 (Mar 19 2022 at 01:24):

@Yaël Dillies

Yaël Dillies (Mar 19 2022 at 01:25):

Long story short: Wait for Lean 4

Jireh Loreaux (Mar 19 2022 at 05:04):

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


Last updated: Dec 20 2023 at 11:08 UTC