topological space from filter

Stream: maths

[Kevin Buzzard]

The argument I know to prove that if X is a top space and X x Y -> Y is a closed map for all Y then X is compact involves a topological structure on option X if X is a set with a filter on it. It looks like this:

def filter_topology {X : Type*} (F : filter X) : topological_space (option X) :=
{ is_open := λ U, if none ∈ U then some ⁻¹' U ∈ F else true,
  is_open_univ := begin
    rw if_pos,
      rw preimage_univ,
      exact filter.univ_mem_sets,
    refine mem_univ (none : option X),
  end,
  is_open_inter := begin
    intros U V hU hV,
    split_ifs, swap, trivial,
    cases h with h0U h0V,
    rw if_pos at hU, swap, exact h0U,
    rw if_pos at hV, swap, exact h0V,
    show some ⁻¹' (U ∩ V) ∈ F,
    rw preimage_inter,
    exact F.inter_sets hU hV,
  end,
  is_open_sUnion := begin
    intros I,
    intro hI,
    split_ifs, swap, trivial,
    rw mem_sUnion at h,
    rcases h with ⟨U, hU, h0U⟩,
    rw preimage_sUnion,
    replace hI := hI U hU,
    rw if_pos at hI, swap, exact h0U,
    refine filter.mem_sets_of_superset hI _,
    exact subset_bUnion_of_mem hU,
  end
}

Is that some well-known topological construction? Do we have it in mathlib?

[Kevin Buzzard]

In short, X gets the discrete topology, and the neighbourhoods of the extra points are precisely (the point) + (element of the filter).

[Reid Barton]

The one-point compactification is an instance of this construction, right? With F = the filter of sets whose complement has compact closure, or so?

[Kevin Buzzard]

X has the discrete topology in my construction, I didn't think about whether it extended to a general top space. In this case F would be the cofinite filter.

[Patrick Massot]

It is well-known, some (deviant) people define filters using it. I don't think it's in mathlib.

[Reid Barton]

Ah yes, I just noticed that too

[Kevin Buzzard]

If you know that X x Y -> Y is a closed map for all Y, and you want to prove that X is compact, your problem is that you don't have a clue which Y to use. My first thought was to try Y=X, but I don't know whether it's true that S x S -> S closed implies S compact and I kind of doubt it. The proof I know goes like this: let F be a proper filter on X, and we want to show that F has an adherent point. Let Y be the top space defined above (note: use discrete top on X even though X is a top space) and now consider the closure of the diagonal map {(x,x)}; its image is closed so must contain *, and if (x,*) is in X x Y in the closure of the diagonal then x does the job.

[Reid Barton]

Good thing the computer scientists chose the definition of compact that they did right?

[Kevin Buzzard]

Right!

[Kevin Buzzard]

And in the proof the other way (showing that if X is compact then pr_2 is always closed) I never have to unfold the definition of compact because we have the tube lemma which is all I need.

[Reid Barton]

The new point is always closed in this construction, right?

[Reid Barton]

Your original one

[Kevin Buzzard]

Yes I guess so. Any subset of X is open.

[Kevin Buzzard]

Reid Barton said:

Good thing the computer scientists chose the definition of compact that they did right?

I'm just counting myself lucky that they didn't use this approach

[Reid Barton]

I'm guessing that there is a general construction that takes two topological spaces $U$ and $Z$ and tells you what data you need to write down (something like how the neighborhood filters of points of $Z$ look when intersected with $U$) to build a space $X = U \cup Z$ with $U$ open and $Z$ its complement. Your construction would then be a special case of this where $U$ is X with the discrete topology and $Z$ is a point.

[Reid Barton]

Of course you will recognize this from algebraic geometry, I'm just not sure exactly what the right data is in this setting

[Kevin Buzzard]

Here's the application:

import topology.maps topology.subset_properties

example : ℕ := 691

open_locale classical

open set

/-- If X is compact then pr₂ : X × Y → Y is a closed map -/
theorem closed_pr2_of_compact
  {X : Type*} [topological_space X] [compact_space X]
  {Y : Type*} [topological_space Y] :
  is_closed_map (prod.snd : X × Y → Y) :=
begin
  intros C hC,
  rw ←is_open_compl_iff,
  rw is_open_iff_forall_mem_open,
  intros y hy,
  rcases generalized_tube_lemma (compact_univ : compact (set.univ : set X))
    (compact_singleton : compact {y}) (is_open_compl_iff.2 hC) _ with
    ⟨U, V, hU, hV, hXU, hyV, hUV⟩,
  { use V,
    split,
    { rintros v hvV ⟨uv, huv, rfl⟩,
      revert huv,
      apply hUV,
      rw set.mem_prod,
      split,
        apply hXU, apply set.mem_univ,
      exact hvV,
    },
    split, exact hV,
    apply hyV,
    apply set.mem_singleton,
  },
  { intros xy hxy,
    intro hxyC,
    apply hy,
    use xy,
    split, exact hxyC,
    rw mem_prod at hxy,
    cases hxy with hx hy,
    exact mem_singleton_iff.1 hy,
  }
end

def filter_topology {X : Type*} (F : filter X) : topological_space (option X) :=
{ is_open := λ U, if none ∈ U then some ⁻¹' U ∈ F else true,
  is_open_univ := begin
    rw if_pos,
      rw preimage_univ,
      exact filter.univ_mem_sets,
    refine mem_univ (none : option X),
  end,
  is_open_inter := begin
    intros U V hU hV,
    split_ifs, swap, trivial,
    cases h with h0U h0V,
    rw if_pos at hU, swap, exact h0U,
    rw if_pos at hV, swap, exact h0V,
    show some ⁻¹' (U ∩ V) ∈ F,
    rw preimage_inter,
    exact F.inter_sets hU hV,
  end,
  is_open_sUnion := begin
    intros I,
    intro hI,
    split_ifs, swap, trivial,
    rw mem_sUnion at h,
    rcases h with ⟨U, hU, h0U⟩,
    rw preimage_sUnion,
    replace hI := hI U hU,
    rw if_pos at hI, swap, exact h0U,
    refine filter.mem_sets_of_superset hI _,
    exact subset_bUnion_of_mem hU,
  end
}

/-- Conversely, if pr₂ : X × Y → Y is a closed map for all Y then X is compact -/
instance compact_space_of_closed_pr2 {X : Type*} [topological_space X]
  (hclosed : ∀ (Y : Type*) [topological_space Y], is_closed_map (prod.snd : X × Y → Y)) :
  compact_space X :=
begin
  constructor,
  -- we will show that every proper filter has an adherent point
  intros F hF h, clear h,
  -- Let Y be the topological space defined above (X + extra point with nhds F)
  letI := filter_topology F,
  replace hclosed := hclosed (option X),
  -- Let D be the closure of {(x,x)} in X × Y.
  set D := closure (set.range (λ x : X, (⟨x, some x⟩ : X × option X))) with hD,
  -- Its image in Y is closed.
  replace hclosed := hclosed D (is_closed_closure),
  -- If the image contains the extra point
  by_cases hnone : none ∈ prod.snd '' D,
  { -- then (x, extra point) is in the closure of D
    rcases hnone with ⟨xy, hxy, hy⟩,
    -- and we claim this x works
    use xy.fst,
    split, exact mem_univ _,
    intro hbot,
    rw ←filter.empty_in_sets_eq_bot at hbot,
    rw filter.mem_inf_sets at hbot,
    rcases hbot with ⟨A, hA, U, hU, hAU⟩,
    rw subset_empty_iff at hAU,
    revert hAU,
    change A ∩ U ≠ ∅,
    rw set.ne_empty_iff_nonempty,
    rw mem_nhds_sets_iff at hU,
    rcases hU with ⟨U', hU'U, hU', hxyU'⟩,
    set V : set (X × option X) := set.prod U' (insert none (some '' A)),
    have hV : is_open V,
      apply is_open_prod hU',
      change if none ∈ (insert none (some '' A)) then some ⁻¹' (insert none (some '' A)) ∈ F else true,
      rw if_pos,
        convert hA using 1,
        ext a,
        simp,
      apply mem_insert,
    have hxyV : xy ∈ V,
      rw mem_prod,
      split, exact hxyU',
      rw hy,
      apply mem_insert,
    rw hD at hxy,
    rw mem_closure_iff at hxy,
    replace hxy := hxy V hV hxyV,
    rcases hxy with ⟨_, hp, p, rfl⟩,
    use p,
    rw mem_prod at hp,
    cases hp with hpU hpA,
    split,
      change some p ∈ _ at hpA,
      rw mem_insert_iff at hpA,
      cases hpA, cases hpA,
      rcases hpA with ⟨p', hp', hpp'⟩,
      convert hp',
      exact option.some_inj.1 hpp'.symm,
    apply hU'U,
    exact hpU
  },
  { -- And if the image doesn't contain the extra point then
    -- in fact we can get a contradiction.
    exfalso,
    -- Indeed X is a subset of the image because (x,x) ∈ D
    have hX : range some ⊆ prod.snd '' D,
    { rintros _ ⟨x, rfl⟩,
      use ⟨x, some x⟩,
      split, swap, refl,
      apply subset_closure,
      use x
    },
    rw ←is_open_compl_iff at hclosed,
    change if none ∈ -(prod.snd '' D) then some ⁻¹' -(prod.snd '' D) ∈ F
      else true at hclosed,
    replace hnone := mem_compl hnone,
    rw if_pos hnone at hclosed,
    apply hF,
    rw ←filter.empty_in_sets_eq_bot,
    convert hclosed,
    symmetry,
    rw eq_empty_iff_forall_not_mem,
    intros x hx,
    apply hx,
    apply hX,
    use x,
  }
end

I have said before that I feel like I write Lean code like a child, just stepping through carefully with each basic tactic. I never really get stuck any more and I really enjoy going through these sorts of proofs in Lean. But what should I be doing to make my Lean code better? I kind of suspect that (a) this result would be fine to put in mathlib but (b) this proof would be not acceptable.

[Scott Morrison]

Maybe golf some bits into term mode? I remain unconvinced that the proofs get better, but they certainly get shorter and that makes me feel more grown-up. :-)

[Scott Morrison]

I doubt the last one should be an instance, as the hclosed argument can't be found by typeclass search.

[Scott Morrison]

I like shorter proofs, with more lemmas, so another stage of golfing might be to do that. e.g. prove that last result in the special case Y = (option X), then deduce the universally quantified one from it trivially. You could also separate the two branches of by_cases into lemmas, I guess.

[Scott Morrison]

I would certainly add more braces: you're using pythonic indenting to simulate proper braces. :-)

[Scott Morrison]

But I think it's pretty reasonable. We should have more "all tactics" proofs in mathlib, to reduce the stigma. You do you! :-)

[Jalex Stark]

I think proof irrelevance means that "add a good theorem to mathlib with an okay proof" is a good contribution, and then later someone else could make a good contribution by improving the proof?
Also as a new user I feel like "read mathlib" is one of the main strategies I have to get better at theory building, and I imagine that the code Kevin just wrote is easier for me to learn from than whatever we get after some code golfing.

[Jalex Stark]

I guess it's somewhat open how pedagogical the code in mathlib is supposed to be, but I think making it more pedagogical speeds up community growth

[Kevin Buzzard]

I don't really understand the mathlib principles which in some sense are maximally anti-pedagogical. The job of the library is not to teach. Because I'm not a programmer I don't really question the principles behind it all. I think there is a place for code which teaches but I'm pretty sure that it isn't mathlib

[Reid Barton]

By the way, isn't there a version of this for proper maps?

[Kevin Buzzard]

You mean in algebraic geometry? Yes, that's why I got interested in the result. I proved it for projective morphisms today in class and realised that I didn't actually know the proof of this topological variant

[Reid Barton]

Even in topology (proper = preimage of compact is compact)

[Reid Barton]

I guess the direction "$f : X \to Y$ universally closed implies $f$ proper" follows from what you did already. (It would certainly suffice to show that if $f' : X' \to Y'$ is a pullback of $f$ with $Y'$ compact, then $X'$ is compact. But $f'$ is again universally closed, and $Y' \to *$ is universally closed because $Y'$ is compact, so $X' \to *$ is universally closed and therefore $X'$ is compact.) I didn't think about the other direction.

[Patrick Massot]

I had a look at local simplification in Kevin's proof. One option is to use more automation, without changing the structure of the proof. I think the main problem of Kevin's approach is not cleaning tactic state after applying the tube lemma. Here the algorithm can be to use simp at *, look at tactic state and then reproduce it with a more civilized method. This brings you to:

/-- If X is compact then pr₂ : X × Y → Y is a closed map -/
theorem closed_pr2_of_compact
  {X : Type*} [topological_space X] [compact_space X]
  {Y : Type*} [topological_space Y] :
  is_closed_map (prod.snd : X × Y → Y) :=
begin
  intros C hC,
  rw [←is_open_compl_iff, is_open_iff_forall_mem_open],
  intros y hy,

  rcases generalized_tube_lemma (compact_univ : compact (set.univ : set X))
    (compact_singleton : compact {y}) (is_open_compl_iff.2 hC) _ with
    ⟨U, V, hU, hV, hXU, hyV, hUV⟩,

  { -- The next three lines were found by typing `simp at *` and then noticing
    -- univ_subset_iff is mysteriously not a simp lemma
    replace hy : ∀ (x : X), (x, y) ∉ C, by simpa using hy,
    replace hXU : U = univ, by simpa [univ_subset_iff] using hXU,
    replace hyV : y ∈ V, by simpa using hyV,
    refine ⟨V, _, by assumption, by assumption⟩,
    rintros v hvV ⟨uv, huv, rfl⟩,
    revert huv,
    apply hUV,
    finish },
  { intros xy hxy hxyC,
    rw ← (show xy.2 = y, by simpa using hxy) at hy,
    apply hy,
    use xy,
    finish, }
end

[Patrick Massot]

(this is using the same imports as in Kevin's message)

[Patrick Massot]

This is probably using too much automation for mathlib's taste. But this discussion is a red herring. mathlib also has a mathematical taste. In topology this taste dictates one shouldn't fear filters and lattices. I'll write a filtery proof next.

[Sebastien Gouezel]

May I suggest to replace the big rcases with an obtain to improve readability?

[Patrick Massot]

The readable proof will be the filter one. I've worked it out on paper, but I need to go so I'll Lean later.

[Patrick Massot]

Let's come back to this closed map question. Remember the statement : if $X$ is compact the $\pi_Y : X \times Y \to Y$ is a closed map for every $Y$. Now let's assume $X$ or $Y$ are metric spaces (or any other kind of spaces whose topology is entirely seen by sequences). Then the proof is:

1. Let $C$ be a closed subset of $X\times Y$, and let's prove $\pi_Y(C)$ is closed.
2. Let $y$ be a point in the closure of $\pi_Y(C)$
3. Let $v_n$ be a sequence in $\pi_Y(C)$ converging to $y$
4. By definition of $\pi_Y(C)$, there is a sequence $u_n$ in $X$ such that $(u_n, v_n) \in C$
5. By compactness of $X$, wlog $u_n$ converges to some $x$
6. Because $C$ is closed the limit $(x, y)$ of $(u_n, v_n)$ belongs to $C$
7. Hence $y = \pi_Y(x, y)$ belongs to $C$.

[Patrick Massot]

Now we need to do the general case. Remember filter replace sequences. More precisely a sequence $u$ gives a filter $u_*\infty$ where $\infty$ is the at_top filter on natural numbers. Saying that $v_n$ belongs to $\pi_Y(C)$ for $n$ large enough is equivalent to $v_*\infty \leq P(\pi_Y(C))$ where $P$ means principal. In particular the existence of $v$ converging in Step 3 implies $\mathcal{N}_y \sqcap P(\pi_Y(C))$ is proper. In the general case, Step 3 is replaced by this conclusion: 𝓝 y ⊓ 𝓟 (πY '' C) ≠ ⊥

[Patrick Massot]

Step 4 is a bit more tricky. You need to understand the analogue is upgrade Step 3 to $\pi_Y^*\mathcal{N}_y \sqcup P(C) \neq \bot$. Here you need the push-pull formula: $f_*(F \sqcap f^$G) = f_F \sqcap G.

[Patrick Massot]

Step 5 is straightforward, compactness of $X$ implies $(\pi_X)_* (\pi_Y^*\mathcal{N}_y \sqcap P(C))$ has a cluster point $x$.

[Patrick Massot]

Then $(x, y)$ is in $C$ because $C$ is closed.

[Patrick Massot]

I need to run, I'll paste the Lean code later.

[Patrick Massot]

First one needs to fill weird holes in the library (or be better at finding stuff). I'm pretty sure some of those are somewhere buried in the perfectoid project, we need to go back PRing.

import topology.maps topology.subset_properties tactic.apply_fun

open set filter function lattice
open_locale classical topological_space


lemma cluster_point_of_compact {X : Type*} [topological_space X] [compact_space X]
  {f : filter X} (h : f ≠ ⊥) : ∃ x, f ⊓ 𝓝 x ≠ ⊥ :=
by simpa using compact_univ f h (by simpa using f.univ_sets)

-- Not in library?!?
lemma set.image_inter_subset {α : Type*} {β : Type*} (f : α → β) (s t : set α) :
  f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
begin
  rintro _ ⟨x, ⟨xs, xt⟩, rfl⟩,
  exact ⟨mem_image_of_mem _ xs,mem_image_of_mem _ xt⟩
end

lemma set.push_pull {α : Type*} {β : Type*} (f : α → β) (s : set α) (t : set β) :
f '' (s ∩ f ⁻¹' t) = f '' s ∩ t :=
begin
  apply subset.antisymm,
  { calc f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ (f '' (f⁻¹' t)) : image_inter_subset _ _ _
  ... ⊆ f '' s ∩ t : inter_subset_inter_right _ (image_preimage_subset f t) },
  { rintros _ ⟨⟨x, h', rfl⟩, h⟩,
    use x,
    finish }
end

lemma lattice.inf_le_inf_left {α :Type*} [semilattice_inf α] (a : α) {b c: α} (h : b ≤ c): b ⊓ a ≤ c ⊓ a :=
by finish

lemma lattice.inf_le_inf_right {α :Type*} [semilattice_inf α] (a : α) {b c: α} (h : b ≤ c): a ⊓ b ≤ a ⊓ c :=
by finish

open lattice

lemma filter.push_pull {α : Type*} {β : Type*} (f : α → β) (F : filter α) (G : filter β) :
map f (F ⊓ comap f G) = map f F ⊓ G :=
begin
  apply le_antisymm,
  { calc map f (F ⊓ comap f G) ≤ map f F ⊓ (map f $ comap f G) : map_inf_le
      ... ≤ map f F ⊓ G : inf_le_inf_right (map f F) map_comap_le },
  {
    rintros U ⟨V, V_in, W, ⟨Z, Z_in, hZ⟩, h⟩,
    rw ← image_subset_iff at h,
    rw mem_inf_sets,
    use [f '' V, image_mem_map V_in, Z, Z_in],
    refine subset.trans _ h,
    have : f '' (V ∩ f ⁻¹' Z) ⊆ f '' (V ∩ W),
    { apply image_subset,
      exact inter_subset_inter_right _ ‹_›, },
    rwa set.push_pull at this }
end

lemma filter.push_pull' {α : Type*} {β : Type*} (f : α → β) (F : filter α) (G : filter β) :
map f (comap f G ⊓ F) = G ⊓ map f F :=
by simp only [filter.push_pull, inf_comm]

lemma filter.ne_bot_of_map_ne_bot  {α : Type*} {β : Type*} (f : α → β) {F : filter α} (h : map f F ≠ ⊥) : F ≠ ⊥ :=
begin
  intro H,
  apply h,
  rw H,
  exact map_bot
end

[Patrick Massot]

Then one can prove Kevin's theorem:

local notation `𝓟` := principal
local infix `×ᶠ`:55 := filter.prod

/-- If X is compact then pr₂ : X × Y → Y is a closed map -/
theorem closed_pr2_of_compact'
  {X : Type*} [topological_space X] [compact_space X]
  {Y : Type*} [topological_space Y] :
  is_closed_map (prod.snd : X × Y → Y) :=
begin
  set πX := (prod.fst : X × Y → X),
  set πY := (prod.snd : X × Y → Y),
  assume C (hC : is_closed C),
  rw is_closed_iff_nhds at hC ⊢,
  assume y (y_closure : 𝓝 y ⊓ 𝓟 (πY '' C) ≠ ⊥),
  have : map πX (comap πY (𝓝 y) ⊓ 𝓟 C) ≠ ⊥,
  { suffices : map πY (comap πY (𝓝 y) ⊓ 𝓟 C) ≠ ⊥,
      from map_ne_bot (λ h, this $  by rw h ; exact map_bot ),
    calc map πY (comap πY (𝓝 y) ⊓ 𝓟 C) =
       𝓝 y ⊓ map πY (𝓟 C) : filter.push_pull' _ _ _
      ... = 𝓝 y ⊓ 𝓟 (πY '' C) : by rw map_principal
      ... ≠ ⊥ : y_closure },
  obtain ⟨x, hx⟩ : ∃ x, map πX (comap πY (𝓝 y) ⊓ 𝓟 C) ⊓ 𝓝 x ≠ ⊥,
    from cluster_point_of_compact this,
  refine ⟨⟨x, y⟩, _, by simp [πY]⟩,
  apply hC, clear hC,
  apply filter.ne_bot_of_map_ne_bot πX,
  calc map πX (𝓝 (x, y) ⊓ 𝓟 C)
      = map πX (comap πX (𝓝 x) ⊓ comap πY (𝓝 y) ⊓ 𝓟 C) : by rw [nhds_prod_eq, filter.prod]
  ... = map πX (comap πY (𝓝 y) ⊓ 𝓟 C ⊓ comap πX (𝓝 x)) : by ac_refl
  ... = map πX (comap πY (𝓝 y) ⊓ 𝓟 C) ⊓ 𝓝 x            : by rw filter.push_pull
  ... ≠ ⊥ : hx,
end

[Kevin Buzzard]

Do you think you're reproving the generalised tube lemma somehow?

[Kevin Buzzard]

Thanks a lot for this Patrick.

[Kevin Buzzard]

The current version of my proof is here (with the converse later on in the file -- I refactored it this afternoon)

[Patrick Massot]

See https://github.com/leanprover-community/mathlib/pull/2069