Zulip Chat Archive

Stream: maths

Topic: topological space from filter


view this post on Zulip Kevin Buzzard (Feb 28 2020 at 16:33):

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?

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 16:34):

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

view this post on Zulip Reid Barton (Feb 28 2020 at 16:37):

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

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 16:38):

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.

view this post on Zulip Patrick Massot (Feb 28 2020 at 16:38):

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

view this post on Zulip Reid Barton (Feb 28 2020 at 16:38):

Ah yes, I just noticed that too

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 16:41):

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.

view this post on Zulip Reid Barton (Feb 28 2020 at 16:42):

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

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 16:42):

Right!

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 16:43):

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.

view this post on Zulip Reid Barton (Feb 28 2020 at 16:48):

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

view this post on Zulip Reid Barton (Feb 28 2020 at 16:48):

Your original one

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 16:48):

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

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 16:49):

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

view this post on Zulip Reid Barton (Feb 28 2020 at 16:54):

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

view this post on Zulip Reid Barton (Feb 28 2020 at 16:55):

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

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 18:27):

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.

view this post on Zulip Scott Morrison (Feb 28 2020 at 18:46):

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. :-)

view this post on Zulip Scott Morrison (Feb 28 2020 at 18:46):

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

view this post on Zulip Scott Morrison (Feb 28 2020 at 18:48):

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.

view this post on Zulip Scott Morrison (Feb 28 2020 at 18:49):

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

view this post on Zulip Scott Morrison (Feb 28 2020 at 18:51):

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

view this post on Zulip Jalex Stark (Feb 28 2020 at 20:47):

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.

view this post on Zulip Jalex Stark (Feb 28 2020 at 20:48):

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

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 20:55):

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

view this post on Zulip Reid Barton (Feb 28 2020 at 22:28):

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

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 23:17):

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

view this post on Zulip Reid Barton (Feb 28 2020 at 23:24):

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

view this post on Zulip Reid Barton (Feb 29 2020 at 01:50):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 13:20):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 13:21):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 13:23):

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.

view this post on Zulip Sebastien Gouezel (Feb 29 2020 at 13:45):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 13:49):

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.

view this post on Zulip Patrick Massot (Feb 29 2020 at 16:59):

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

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 17:05):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 17:12):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 17:14):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 17:14):

Then (x,y)(x, y) is in CC because CC is closed.

view this post on Zulip Patrick Massot (Feb 29 2020 at 17:15):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 19:01):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 19:01):

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

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 19:28):

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

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 19:29):

Thanks a lot for this Patrick.

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 19:31):

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

view this post on Zulip Patrick Massot (Feb 29 2020 at 21:51):

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


Last updated: May 06 2021 at 18:20 UTC