One point compactification of the natural numbers

Stream: mathlib4

[Dagur Asgeirsson]

I have no experience working with real numbers in lean, so I'm hoping to nerdsnipe someone into golfing the following :innocent:

import Mathlib

open OnePoint

noncomputable def map : C(OnePoint ℕ, ℝ) where
  toFun
    | ∞ => 0
    | OnePoint.some n => 1 / (n+1 : ℝ)
  continuous_toFun := by
    rw [continuous_iff_continuousAt]
    rintro (_|n)
    · erw [OnePoint.continuousAt_infty]
      intro s (hs : s ∈ nhds 0)
      rw [Real.isTopologicalBasis_Ioo_rat.mem_nhds_iff] at hs
      obtain ⟨t, ht, zero_mem, hts⟩ := hs
      simp only [Set.mem_iUnion, Set.mem_singleton_iff, exists_prop] at ht
      obtain ⟨a, b, _, rfl⟩ := ht
      refine ⟨Finset.range (Nat.ceil (1/b)), isClosed_discrete _, ?_, ?_⟩
      · rw [isCompact_iff_finite]
        exact Finset.finite_toSet _
      · change Set.MapsTo (fun (n : ℕ) ↦ 1 / (n+1 : ℝ)) _ _
        intro n hn
        apply hts
        simp only [one_div, Set.mem_Ioo]
        simp only [Set.mem_Ioo] at zero_mem
        constructor
        · exact lt_trans zero_mem.1 Nat.inv_pos_of_nat
        · simp only [one_div, Finset.coe_range, Set.compl_Iio, Set.mem_Ici, Nat.ceil_le,
            ← Rat.cast_le (K := ℝ)] at hn
          rw [inv_lt (by positivity) zero_mem.2, ← Rat.cast_inv]
          exact lt_of_le_of_lt hn (lt_add_one _)
    · erw [continuousAt_coe]
      exact continuous_bot.continuousAt

[Dagur Asgeirsson]

I guess I more generally want a theorem like:

lemma natUnionInfty_classifies_convergent_sequences {X : Type*} [TopologicalSpace X]
    (f : OnePoint ℕ → X) : Continuous f ↔
      sorry /- the restriction of `f` to `ℕ` is a convergent sequence -/ := sorry

What's the idiomatic spelling for convergent sequences?

[Kevin Buzzard]

I don't know if this is idiomatic but I think it's mathematically correct:

import Mathlib

open scoped Topology OnePoint
open Filter

lemma natUnionInfty_classifies_convergent_sequences {X : Type*} [TopologicalSpace X]
    (f : OnePoint ℕ → X) : Continuous f ↔
    Tendsto (fun n : ℕ ↦ f n) atTop (𝓝 (f ∞)) := sorry

[Jireh Loreaux]

That's what I would have suggested Kevin.

[Kevin Buzzard]

So we have things like HasSum and Summable, but not HasLimit and Limitable?

[Jireh Loreaux]

But actually, what you probably want is cofinite instead of atTop, and then you can replace ℕ with any topological space with the discrete topology. (EDIT: from which you can recover Kevin's version above, which is the idiomatic spelling for ℕ)

[Adam Topaz]

Looks like OnePoint is missing some API!

[Adam Topaz]

In general one should use the cocompact filter, right?

[Kevin Buzzard]

docs#Filter.cocompact

[Jireh Loreaux]

well, sure, but if the space isn't discrete you're actually going to need conditions away from infinity to guarantee it is continuous.

[Adam Topaz]

I understand. What I mean is that there should be a lemma saying that if f : OnePoint X -> Y is a function whose restriction to X is continuous and which satisfies some property at infinity (essentially OnePoint.continuousAt_infty') then f is continuous.

[Jireh Loreaux]

Do we not have that already?

[Adam Topaz]

We essentially do but you have to combine OnePoint.continuousAt_infty' or OnePoint.continuousAt_infty and OnePoint.continuousAt_coe and continuous_iff_continuousAt

[Adam Topaz]

It looks like that's what Dagur did in this case :)

[Jireh Loreaux]

ah I see, we have the pieces but they are separated.

[Jireh Loreaux]

Subject to lots of golfing, here is the general result:

import Mathlib

open scoped Topology OnePoint
open Filter

lemma OnePoint.continuous_iff {X Y : Type*} [TopologicalSpace X]
    [TopologicalSpace Y] (f : OnePoint X → Y) : Continuous f ↔
    Continuous (fun x : X ↦ f x) ∧ Tendsto (fun x : X ↦ f x) (coclosedCompact X) (𝓝 (f ∞)) := by
  rw [continuous_iff_continuousAt]
  constructor
  · intro h
    refine ⟨?_, ?_⟩
    · rw [continuous_iff_continuousAt]
      exact fun x ↦ (h x).comp continuous_coe.continuousAt
    · rw [← Function.comp, ← continuousAt_infty']
      exact h _
  · rintro ⟨h₁, h₂⟩
    refine OnePoint.rec ?_ ?_
    · rw [continuousAt_infty']
      exact h₂
    · intro x
      rw [continuousAt_coe]
      exact h₁.continuousAt

[Jireh Loreaux]

then with the above

lemma OnePoint.continuous_iff_of_discrete {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [DiscreteTopology X] (f : OnePoint X → Y) :
    Continuous f ↔ Tendsto (fun x : X ↦ f x) cofinite (𝓝 (f ∞)) := by
  simp [continuous_iff, cocompact_eq_cofinite, continuous_of_discreteTopology]

lemma OnePoint.continuous_iff_of_nat {Y : Type*} [TopologicalSpace Y] (f : OnePoint ℕ → Y) :
    Continuous f ↔ Tendsto (fun x : ℕ ↦ f x) atTop (𝓝 (f ∞)) := by
  rw [continuous_iff_of_discrete, Nat.cofinite_eq_atTop]

noncomputable def map : C(OnePoint ℕ, ℝ) where
  toFun
    | ∞ => 0
    | OnePoint.some n => 1 / (n+1 : ℝ)
  continuous_toFun := OnePoint.continuous_iff_of_nat _ |>.mpr
    tendsto_one_div_add_atTop_nhds_zero_nat

[Kevin Buzzard]

Nerdsnipe achieved!

[Jireh Loreaux]

Bonus:

noncomputable def OnePoint.continuousMapNatEquiv (Y : Type*) [TopologicalSpace Y] [T2Space Y] :
    C(OnePoint ℕ, Y) ≃ { f : ℕ → Y // ∃ L, Tendsto (fun x : ℕ ↦ f x) atTop (𝓝 L) } where
  toFun f := ⟨fun x ↦ f x, ⟨f ∞, continuous_iff_of_nat _ |>.mp (map_continuous f)⟩⟩
  invFun f :=
    { toFun := fun x => match x with
        | ∞ => Classical.choose f.2
        | some x => f.1 x
      continuous_toFun := continuous_iff_of_nat _ |>.mpr <| Classical.choose_spec f.2 }
  left_inv f := by
    ext x
    refine OnePoint.rec ?_ ?_ x
    · refine tendsto_nhds_unique ?_ (continuous_iff_of_nat _ |>.mp <| map_continuous f)
      let f' : { f : ℕ → Y // ∃ L, Tendsto (fun x : ℕ ↦ f x) atTop (𝓝 L) } :=
        ⟨fun x ↦ f x, ⟨f ∞, continuous_iff_of_nat f |>.mp <| map_continuous f⟩⟩
      exact Classical.choose_spec f'.property
    · simp
  right_inv f := rfl

[Jireh Loreaux]

@Dagur Asgeirsson feel free to PR any of this, I don't really have time to do it.

[Dagur Asgeirsson]

Thanks Jireh! I will PR it soon

[Jireh Loreaux]

I couldn't resist. golfed:

import Mathlib

open scoped Topology OnePoint
open Filter

protected theorem OnePoint.forall {X : Type*} {p : OnePoint X → Prop} :
    (∀ (x : OnePoint X), p x) ↔ p ∞ ∧ ∀ (x : X), p (some x) :=
  Option.forall

lemma OnePoint.continuous_iff {X Y : Type*} [TopologicalSpace X]
    [TopologicalSpace Y] (f : OnePoint X → Y) : Continuous f ↔
    Tendsto (fun x : X ↦ f x) (coclosedCompact X) (𝓝 (f ∞)) ∧ Continuous (fun x : X ↦ f x) := by
  simp_rw [continuous_iff_continuousAt, OnePoint.forall, continuousAt_coe, continuousAt_infty']
  rfl

[Ruben Van de Velde]

Minus one line

import Mathlib

open scoped Topology OnePoint
open Filter

protected theorem OnePoint.forall {X : Type*} {p : OnePoint X → Prop} :
    (∀ (x : OnePoint X), p x) ↔ p ∞ ∧ ∀ (x : X), p (some x) :=
  Option.forall

lemma OnePoint.continuous_iff {X Y : Type*} [TopologicalSpace X]
    [TopologicalSpace Y] (f : OnePoint X → Y) : Continuous f ↔
    Tendsto (fun x : X ↦ f x) (coclosedCompact X) (𝓝 (f ∞)) ∧ Continuous (fun x : X ↦ f x) := by
  simp_rw [continuous_iff_continuousAt, OnePoint.forall, continuousAt_coe, continuousAt_infty', Function.comp_def]

[Damiano Testa]

Finally it is so trivial that we discovered the reason it is not in Mathlib...

[Kevin Buzzard]

I think that actually short proofs tell us that we're writing the right API

[Dagur Asgeirsson]

#13355

[Jireh Loreaux]

@Dagur Asgeirsson I think the discrete version (not specific to Nat) of that equiv I wrote down above could actually be useful from time to time. Care to include that too?

[Dagur Asgeirsson]

Yes I'll add that now