topology is fun

Stream: condensed mathematics

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

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.

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

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 }

[Patrick Massot]

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⟩

[Patrick Massot]

Here the key trick from mathlib is

lemma t2_iff_nhds : t2_space α ↔ ∀ {x y : α}, ne_bot (𝓝 x ⊓ 𝓝 y) → x = y

[Johan Commelin]

Patrick Massot said:

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

I think so, yes

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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'.