Zulip Chat Archive

Stream: condensed mathematics

Topic: topology is fun


view this post on Zulip Patrick Massot (Mar 13 2021 at 21:19):

Still having a look at what I could clean up a bit before PRing to mathlib, I see:

-- is there a short proof using filters? jmc couldn't find it
lemma is_compact {f : X  Y} (hf : inducing f) (s : set X) (hs : is_compact (f '' s)) :
  is_compact s :=
begin
  apply compact_of_finite_subcover,
  intros ι U hU hsU,
  have :  i,  V, is_open V  f ⁻¹' V = (U i),
  { intro i, apply hf.exists_open (hU i) },
  choose V hV₁ hV₂ using this,
  have : f '' s   (i : ι), V i,
  { rw [set.image_subset_iff, set.preimage_Union],
    refine set.subset.trans hsU (set.Union_subset_Union _),
    intro i, rw hV₂ },
  obtain t, ht := hs.elim_finite_subcover V hV₁ this,
  refine t, _⟩,
  simp only [set.image_subset_iff, set.preimage_Union] at ht,
  refine set.subset.trans ht (set.Union_subset_Union _),
  intro i,
  refine set.Union_subset_Union _,
  rintro -,
  rw hV₂
end

view this post on Zulip Patrick Massot (Mar 13 2021 at 21:19):

I say:

lemma is_compact {f : X  Y} (hf : inducing f) (s : set X) (hs : is_compact (f '' s)) :
  is_compact s :=
begin
  introsI F F_ne_bot F_le,
  obtain _, x, x_in : x  s, rfl⟩, hx : cluster_pt (f x) (map f F)⟩ :=
    hs (calc map f F  map f (𝓟 s) : map_mono F_le
                 ... = 𝓟 (f '' s) : map_principal),
  use [x, x_in],
  unfold cluster_pt,
  rwa [hf.nhds_eq_comap,  filter.map_ne_bot_iff, filter.push_pull']
end

view this post on Zulip Johan Commelin (Mar 13 2021 at 21:23):

That comment was just sitting there, waiting for you to come along (-;

view this post on Zulip Patrick Massot (Mar 13 2021 at 21:30):

Let's make it a bit more readable:

lemma is_compact {f : X  Y} (hf : inducing f) (s : set X) (hs : is_compact (f '' s)) :
  is_compact s :=
begin
  introsI F F_ne_bot F_le,
  obtain _, x, x_in : x  s, rfl⟩, hx : cluster_pt (f x) (map f F)⟩ :=
    hs (calc map f F  map f (𝓟 s) : map_mono F_le
                 ... = 𝓟 (f '' s) : map_principal),
  use [x, x_in],
  suffices : (map f (𝓝 x  F)).ne_bot, by simpa [filter.map_ne_bot_iff],
  rwa calc map f (𝓝 x  F) = map f ((comap f $ 𝓝 $ f x)  F) : by rw hf.nhds_eq_comap
                        ... = 𝓝 (f x)  map f F :  filter.push_pull' _ _ _,
end

view this post on Zulip Johan Commelin (Mar 13 2021 at 21:31):

You have a double before filter.push_pull' on the final line

view this post on Zulip Patrick Massot (Mar 13 2021 at 21:33):

Note how the crucial thing you were missing is the push-pull formula for filters (docs#filter.push_pull'), which is indeed pretty subtle. Fortunately we needed it for perfectoid spaces, so it's there.

view this post on Zulip Patrick Massot (Mar 13 2021 at 21:49):

By the way, is there any reason this compactness lemma was not stated as an iff? The other direction is trivial since f is continuous.

view this post on Zulip Patrick Massot (Mar 13 2021 at 21:51):

Is it used only in compact_space (filtration (Λ →+ M) c)?

view this post on Zulip Patrick Massot (Mar 13 2021 at 22:09):

I also see in that file:

lemma t2_space [t2_space Y] {f : X  Y} (hf : embedding f) :
  t2_space X :=
{ t2 := λ x y h,
  begin
    obtain U, V, hU, hV, hx, hy, hUV := t2_separation (hf.inj.ne h),
    refine f ⁻¹' U, f ⁻¹' V,
      hf.continuous.is_open_preimage _ hU,
      hf.continuous.is_open_preimage _ hV,
      set.mem_preimage.mpr hx,
      set.mem_preimage.mpr hy, _⟩,
    rw  set.disjoint_iff_inter_eq_empty at hUV ,
    exact hUV.preimage _
  end }

view this post on Zulip Patrick Massot (Mar 13 2021 at 22:09):

I shouldn't enjoy it so much, but I can't resist PRing it as:

lemma t2_space [t2_space Y] {f : X  Y} (hf : embedding f) : t2_space X :=
t2_iff_nhds.mpr $ λ x y h, hf.inj $ eq_of_nhds_ne_bot
λ H, by simpa [hf.to_inducing.nhds_eq_comap,  comap_inf, H, not_ne_bot.mpr] using h

view this post on Zulip Patrick Massot (Mar 13 2021 at 22:10):

Here the key trick from mathlib is

lemma t2_iff_nhds : t2_space α   {x y : α}, ne_bot (𝓝 x  𝓝 y)  x = y

view this post on Zulip Johan Commelin (Mar 13 2021 at 22:10):

Patrick Massot said:

Is it used only in compact_space (filtration (Λ →+ M) c)?

I think so, yes

view this post on Zulip Johan Commelin (Mar 13 2021 at 22:11):

If you want to make it iffy, go ahead (-;

view this post on Zulip Kevin Buzzard (Mar 13 2021 at 22:26):

The push pull statement is just f(Sf1(T))=f(S)Tf(S\cap f^{-1}(T))=f(S)\cap T for generalised sets.

view this post on Zulip Kevin Buzzard (Mar 13 2021 at 22:30):

If S' is the largest subfilter of S such that tendsto S' T then the filter in question is the smallest subfilter T' of T such that tendsto S' T'.


Last updated: May 09 2021 at 16:20 UTC