## Stream: condensed mathematics

### Topic: topology is fun

#### 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


#### 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


#### Johan Commelin (Mar 13 2021 at 21:23):

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

#### 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


#### Johan Commelin (Mar 13 2021 at 21:31):

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

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

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

#### Patrick Massot (Mar 13 2021 at 21:51):

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

#### 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 }


#### 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⟩


#### 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


#### 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

#### Johan Commelin (Mar 13 2021 at 22:11):

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

#### Kevin Buzzard (Mar 13 2021 at 22:26):

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

#### 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