formalizing one point compactification

Stream: maths

[Yourong Zang]

Hello, I've formalized a few things about one-point compactifications. My code is available here. The statements and proofs I wrote are super naive, but I couldn't find a neater way to define the natural topology on option. Therefore, I am not sure if the things I've done here meet mathlib's standards. Please let me know if there is something in mathlib I should be using.

I proved that the one-point compactification is a compact topological space, and it inherits properties such as t1 from a t1 X, connectedness from a noncompact, preconnected X, and t2 from a locally compact, t2 X. The names I gave to those lemmas are quite generic; I am grateful for any suggestion on them.

Thanks in advance! :grinning:

[Yakov Pechersky]

When working on a z : option X, it's easier to say cases z than

  by_cases z = none,
  {  },
  {  }

[Yourong Zang]

Yakov Pechersky said:

When working on a z : option X, it's easier to say cases z than

  by_cases z = none,
  {  },
  {  }

Will change that.

[Yakov Pechersky]

In fact, you can say

  rintro ⟨_|z⟩,

[Eric Wieser]

That's longer and harder to type than cases z though

[Heather Macbeth]

Some points for discussion (I have to go now, so will check in later):

• is it better to use the type synonym or to make this a topology directly on option X?
• can you prove the characterization "smallest compactification of X", or even arrange things so that that is the definition?

[Mario Carneiro]

Eric Wieser said:

That's longer and harder to type than cases z though

That's rintro, so it's being used to replace intro z, cases z

[Mario Carneiro]

although I think the syntax there is wrong, it should be rintro (_|z),

[Yakov Pechersky]

either works:

lemma univ_eq_union_none : (set_base X ∪ {none}) = univ :=
begin
  refine le_antisymm (subset_univ _) _,
  rintro ⟨_|x⟩;
  simp
end

[Kevin Buzzard]

I suspect that if X is compact then the one point compactification is the second smallest compactification :-) Is there a universal property? There is for Stone-Cech I think but I'm less sure about this one...

[Yakov Pechersky]

Here is some golf. It's important to have the right API simp lemmas early, makes trivial proofs trivial.

def alexandroff (X : Type*) [topological_space X] := option X

def of_base {X : Type*} [topological_space X] : X → alexandroff X := some

variables {X : Type*} [topological_space X]

lemma of_base_apply {x : X} : of_base x = some x := rfl

instance : has_coe X (alexandroff X) := ⟨of_base⟩

@[simp] lemma coe_some_eq_of_base {x : X} : (some x : alexandroff X) = x := rfl

@[simp] lemma coe_ne_none (x : X) : (x : alexandroff X) ≠ none .

@[simp] lemma of_base_eq_coe {x : X} : of_base x = (x : alexandroff X) := rfl

def set_base (X : Type*) [topological_space X] : set (alexandroff X) := coe '' (univ : set X)

@[simp] lemma coe_mem_set_base (x : X) : (x : alexandroff X) ∈ (set_base X) :=
by simp [set_base]

lemma univ_eq_union_none : (set_base X ∪ {none}) = univ :=
begin
  refine le_antisymm (subset_univ _) _,
  rintro ⟨_|x⟩;
  simp
end

@[simp] lemma none_not_mem_set_base : none ∉ set_base X :=
by simp [set_base, ←coe_some_eq_of_base]

@[simp] lemma not_mem_set_base_iff (x : alexandroff X) :
  x ∉ set_base X ↔ x = none :=
by { cases x; simp }

lemma inter_none_eq_empty : (set_base X) ∩ {none} = ∅ :=
by { ext ⟨_|x⟩; simp }

lemma of_base_preimage_none : (of_base⁻¹' {none} : set X) = ∅ :=
by { ext, simp }

instance : topological_space (alexandroff X)  :=
{ is_open := λ s, if none ∈ s then is_compact (of_base⁻¹' s)ᶜ ∧ is_open (of_base⁻¹' s)
    else is_open (of_base⁻¹' s),
  is_open_univ := by simp,
  is_open_inter :=
  λ s t hs ht, begin
    split_ifs at hs ht with h h' h' h' h,
    { simpa [h, h', compl_inter] using
        and.intro (hs.left.union ht.left) (hs.right.inter ht.right) },
    { simpa [h, h'] using hs.inter ht.right },
    { simpa [h, h'] using hs.right.inter ht },
    { simpa [h, h'] using hs.inter ht }
  end,
  is_open_sUnion :=
  λ S ht, begin
    suffices : is_open (of_base⁻¹' ⋃₀S),
    { split_ifs with h,
      { obtain ⟨(a : set (alexandroff X)), ha, ha'⟩ := mem_sUnion.mp h,
        specialize ht a ha,
        rw if_pos ha' at ht,
        refine ⟨compact_of_is_closed_subset ht.left this.is_closed_compl _, this⟩,
        rw [compl_subset_compl, preimage_subset_iff],
        intros y hy,
        refine ⟨a, ha, hy⟩ },
      { exact this } },
     rw is_open_iff_forall_mem_open,
     simp only [and_imp, exists_prop, mem_Union, preimage_sUnion, mem_preimage, of_base_eq_coe,
                exists_imp_distrib],
     intros y s hs hy,
     refine ⟨of_base ⁻¹' s, subset_subset_Union _ (subset_subset_Union hs (subset.refl _)), _,
        mem_preimage.mpr hy⟩,
     specialize ht s hs,
     split_ifs at ht,
     { exact ht.right },
     { exact ht }
  end }

[Heather Macbeth]

@Kevin Buzzard, I'm a little rusty, but there's a universal property stated here:
https://ncatlab.org/nlab/show/one-point+compactification#UniversalProperty

[Heather Macbeth]

And there's a reference here to the "smallest compactification" property:
https://math.stackexchange.com/questions/201964/the-smallest-compactification

[Yourong Zang]

Yakov Pechersky said:

Here is some golf. It's important to have the right API simp lemmas early, makes trivial proofs trivial.

def alexandroff (X : Type*) [topological_space X] := option X

def of_base {X : Type*} [topological_space X] : X → alexandroff X := some

variables {X : Type*} [topological_space X]

lemma of_base_apply {x : X} : of_base x = some x := rfl

instance : has_coe X (alexandroff X) := ⟨of_base⟩

@[simp] lemma coe_some_eq_of_base {x : X} : (some x : alexandroff X) = x := rfl

@[simp] lemma coe_ne_none (x : X) : (x : alexandroff X) ≠ none .

@[simp] lemma of_base_eq_coe {x : X} : of_base x = (x : alexandroff X) := rfl

def set_base (X : Type*) [topological_space X] : set (alexandroff X) := coe '' (univ : set X)

@[simp] lemma coe_mem_set_base (x : X) : (x : alexandroff X) ∈ (set_base X) :=
by simp [set_base]

lemma univ_eq_union_none : (set_base X ∪ {none}) = univ :=
begin
  refine le_antisymm (subset_univ _) _,
  rintro ⟨_|x⟩;
  simp
end

@[simp] lemma none_not_mem_set_base : none ∉ set_base X :=
by simp [set_base, ←coe_some_eq_of_base]

@[simp] lemma not_mem_set_base_iff (x : alexandroff X) :
  x ∉ set_base X ↔ x = none :=
by { cases x; simp }

lemma inter_none_eq_empty : (set_base X) ∩ {none} = ∅ :=
by { ext ⟨_|x⟩; simp }

lemma of_base_preimage_none : (of_base⁻¹' {none} : set X) = ∅ :=
by { ext, simp }

instance : topological_space (alexandroff X)  :=
{ is_open := λ s, if none ∈ s then is_compact (of_base⁻¹' s)ᶜ ∧ is_open (of_base⁻¹' s)
    else is_open (of_base⁻¹' s),
  is_open_univ := by simp,
  is_open_inter :=
  λ s t hs ht, begin
    split_ifs at hs ht with h h' h' h' h,
    { simpa [h, h', compl_inter] using
        and.intro (hs.left.union ht.left) (hs.right.inter ht.right) },
    { simpa [h, h'] using hs.inter ht.right },
    { simpa [h, h'] using hs.right.inter ht },
    { simpa [h, h'] using hs.inter ht }
  end,
  is_open_sUnion :=
  λ S ht, begin
    suffices : is_open (of_base⁻¹' ⋃₀S),
    { split_ifs with h,
      { obtain ⟨(a : set (alexandroff X)), ha, ha'⟩ := mem_sUnion.mp h,
        specialize ht a ha,
        rw if_pos ha' at ht,
        refine ⟨compact_of_is_closed_subset ht.left this.is_closed_compl _, this⟩,
        rw [compl_subset_compl, preimage_subset_iff],
        intros y hy,
        refine ⟨a, ha, hy⟩ },
      { exact this } },
     rw is_open_iff_forall_mem_open,
     simp only [and_imp, exists_prop, mem_Union, preimage_sUnion, mem_preimage, of_base_eq_coe,
                exists_imp_distrib],
     intros y s hs hy,
     refine ⟨of_base ⁻¹' s, subset_subset_Union _ (subset_subset_Union hs (subset.refl _)), _,
        mem_preimage.mpr hy⟩,
     specialize ht s hs,
     split_ifs at ht,
     { exact ht.right },
     { exact ht }
  end }

Thank you so much for the modifications! One question: what does the dot at the end of the lemma coe_ne_none (x : X) : (x : alexandroff X) ≠ none . do?

[Yakov Pechersky]

That the proof is so trivial you don't even need to give a term proof. It's based on the fact that some x \ne none by the definition of the inductive type.

[Kevin Buzzard]

I would have been tempted to call it infty not none

[Yourong Zang]

Kevin Buzzard said:

I would have been tempted to call it infty not none

But in that case, would tactics like cases and rintro <_|x> still be neat to use?

[Eric Wieser]

I can't help feeling it would be easier to just define the topology on option, and then only introduce the type alias for the purpose of making the instance

[Eric Wieser]

Otherwise you end up rewriting tonnes of option API.

[Yourong Zang]

Eric Wieser said:

I can't help feeling it would be easier to just define the topology on option, and then only introduce the type alias for the purpose of making the instance

Do you mean I should define alexandroff X after constructing the topology of option X?

[Eric Wieser]

I'm suggesting that might at least be easier, yes - although I can't advise on whether it's actually better. Something like:

/-- see note [reducible non-instances] -/
@[reducible] def one_point_compaction : topological_space (option X) := sorry

def alexandroff := option X

instance : topological_space (alexandroff X) := one_point_compaction

[Yourong Zang]

Eric Wieser said:

I'm suggesting that might at least be easier, yes - although I can't advise on whether it's actually better. Something like:

/-- see note [reducible non-instances] -/
@[reducible] def one_point_compaction : topological_space (option X) := sorry

def alexandroff := option X

instance : topological_space (alexandroff X) := one_point_compaction

This looks very neat. Suppose I define aliases of := some, infty := none like Prof. @Kevin Buzzard suggested and take some x : alexdroff X. I was wondering if it is possible to do something like cases x and produce two goals with of x and infty.

[Eric Wieser]

No, unfortunately you can't make cases do that. The best you can do is something like docs#with_bot.rec_bot_coe

[Eric Wieser]

Which you'd use as induction x with alexdroff.rec_of_infty

[Yourong Zang]

Eric Wieser said:

Which you'd use as induction x with alexdroff.rec_of_infty

Thank you!

[Eric Wieser]

Oops, I meant using not with

[Yakov Pechersky]

Eric, why should option get that topology as opposed to, let's say, the introduced point being near every other point?

[Yourong Zang]

I think that's a good point. It's probably a good idea to define alexandroff first and construct the topology, instead of doing it on option. There are only about 4-5 super trivial lemmas from option we need to prove, similar to those in docs#with_bot. The other trivial lemmas are about sets in the extension, so they must be there regardless of the name we use.

[Eric Wieser]

@Yakov Pechersky, option doesn't "get" that topology, it's a def not an instance. My snippet just says "it is possible to construct this topology on option", not "this is the canonical topology on option"

[Yakov Pechersky]

Ah, I see. Makes sense!

[Eric Wieser]

Having the definition available on option makes it easier (or at least, more discoverable) to apply locally to with_top and with_bot if needed

[Eric Wieser]

(do those have a topology in mathlib already?)

[Yourong Zang]

Eric Wieser said:

Having the definition available on option makes it easier (or at least, more discoverable) to apply locally to with_top and with_bot if needed

Thank you for this excellent point! Suppose I define topological_space (option X) first. Should I define the other instances, say t2_space (option X) for a locally compact, t2 X in the same way? Or should I do that on alexandroff X as an instance instead?

[Eric Wieser]

Surprisingly you can actually just make the t2 space an instance on option I think

[Eric Wieser]

Because it doesn't contain any data

[Eric Wieser]

Or from another viewpoint, it is really an instance on one_point_compaction rather than option X.

[Kyle Miller]

It might be worth distinguishing the two topologies on option X (I'm not sure if I've followed what the consensus has been on this). If I got this right:

• The forgetful functor from the category of pointed topological spaces to topological spaces has a left adjoint (call it option) that introduces a basepoint with the disjoint union topology.
• The forgetful functor from the category of pointed locally compact T2 spaces to locally compact T2 spaces (morphisms are proper maps) has a left adjoint (call it alexandroff) that introduces a basepoint with the one-point compactification topology.

A relationship between them is that the identity function gives a continuous map option X -> alexandroff X of pointed spaces.

Though, I'm not sure if I've ever seen the first construction in use. It seems that usually, if you have nice enough connected spaces, you care about homotopy classes of pointed spaces, so you can choose an arbitrary basepoint.

[Reid Barton]

The first construction does get used in homotopy theory, and is usually denoted by $X \mapsto X_+$, though it might be considered largely as a notational device. For example, the unreduced homology of $X$ is the reduced homology of $X_+$.