Zulip Chat Archive

Stream: Is there code for X?

Topic: More point set topology questions


view this post on Zulip Adam Topaz (Oct 08 2020 at 18:58):

Does mathlib have one and/or both of the following facts?

lemma le_nhds_Lim {X : Type*} [topological_space X] [compact_space X] [nonempty X]
  (F : ultrafilter X) : F.1  nhds (Lim F.1) := sorry
lemma Lim_eq_iff_le_nhds {X : Type*} [topological_space X] [compact_space X] [t2_space X]
  [nonempty X] (x : X) (F : ultrafilter X) : Lim F.1 = x  F.1  nhds x := sorry

view this post on Zulip Adam Topaz (Oct 08 2020 at 19:03):

I have a (currently very messy) proof of the equivalence between compact Hausdorff spaces and the category of algebras for the ultrafilter monad. These would help cleaning it up a bit.

In case anyone is interested:
https://github.com/leanprover-community/mathlib/blob/ca24ce9856e8d2b4e2d6148f1030cda171c8ba49/src/topology/category/Compactum.lean#L578

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 20:52):

It seems that the answer is "no" but we have docs#compact_iff_ultrafilter_le_nhds and docs#Lim_spec

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 20:59):

The second one follows from the first one and docs#Lim_eq.
BTW,

  • have a look at the trick I used in docs#Lim_spec to avoid a [nonempty] assumption;
  • could you please
    • rename docs#Lim_spec to le_nhds_Lim and docs#lim_spec to tendsto_nhds_lim;
    • add Lim_eq_iff (h : ∃ a, Lim f ≤ nhds a) {a} : Lim f = a ↔ F ≤ nhds a and lim_eq_iff (h : ∃ a, tendsto g f (nhds a)) {a} : lim f g = a ↔ tendsto g f a?

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:04):

Right, I've seen docs#compact_iff_ultrafilter_le_nhds docs#Lim_spec and docs#Lim_eq (they're actually used in the linked file above, but I'm still working on cleaning it up). I'm not sure what you mean about the nonempty assumption. It's a little subtle, since one has to use the fact that X is empty if and only if ultrafilter X is empty.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:06):

I opened issue #4543.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:07):

If you'll try to prove this (do cases on compact_iff_ultrafilter_le_nhds, then use Lim_spec), then the only place where you'll need nonempty is the implicit argument of Lim.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:09):

Ah, I see. That's not a problem for the second lemma (you can supply ⟨x⟩ as [nonempty α])

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:10):

And same for the first one, since you have an ultrafilter.

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:11):

The branch above also proves this
https://github.com/leanprover-community/mathlib/blob/ca24ce9856e8d2b4e2d6148f1030cda171c8ba49/src/order/filter/ultrafilter.lean#L267
which gives a nonempty X from nonempty (ultrafilter X).

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:11):

For the first one you can supply nonempty_of_ne_bot F.1

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:11):

That's for sets.

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:11):

I think.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:11):

AFAIR, we have an instance {F : ultrafilter α} [ne_bot (F.1)]

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:11):

docs#filter.nonempty_of_ne_bot

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:12):

We don't have this instance!

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:12):

Oops!

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:13):

Just add it: instance {F : ultrafilter α} : ne_bot F.1 := F.2

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:14):

I guess our is_ultrafilter API is much better.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:14):

If you have time, you may want to migrate mathlib to bundled ultrafilters.

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:15):

I never have time.

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:15):

But I'll try to find some nonexistent time to take care of that issue.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:16):

Probably with definition like

structure ultrafilter (α : Type*) :=
(to_filter : filter α)
(ne_bot' : ne_bot to_filter)
(le_of_le' : g, ne_bot g  g  to_filter  to_filter  g)

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:17):

If you do this, then lemmas assuming is_ultrafilter in order/filter/filter_product can become instances.

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:17):

Why not keep ultrafilter as is, and just restate the lemmas.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:40):

I don't think that it makes sense to have both is_ultrafilter and ultrafilter.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:41):

If you have an ultrafilter, then most probably (unless it's pure a) it is defined using classical.some, and being an ultrafilter is its main property.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:43):

And if you leave only ultrafilter, then using a structure makes it possible to use { to_filter := ..., ne_bot := ..., le_of_le := ... } in a constructor instead of just subtype.mk.

view this post on Zulip Adam Topaz (Oct 08 2020 at 22:08):

@Yury G. Kudryashov
https://github.com/leanprover-community/mathlib/compare/lim_spec_cleanup

I'll wait for github's checks to finish before opening a PR. Is this what you had in mind?

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 22:12):

You can use

lemma is_ultrafilter.le_nhds_Lim [compact_space α] (F : ultrafilter α) :
  F.1  nhds (@Lim _ _ F.1.nonempty_of_ne_bot F.1) :=
begin
  rcases compact_iff_ultrafilter_le_nhds.mp compact_univ F.1 F.2 (by simp) with x,_,h⟩,
  exact le_nhds_Lim x,h⟩,
end

view this post on Zulip Adam Topaz (Oct 08 2020 at 22:15):

unknown identifier 'is_compact_univ'
Am I missing an import?

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 22:18):

It's compact_univ

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 22:19):

Sorry, I made lots of typos. Hopefully, fixed.

view this post on Zulip Adam Topaz (Oct 08 2020 at 22:20):

No worries. Found it now.

view this post on Zulip Adam Topaz (Oct 08 2020 at 22:21):

Pushed the change just now.

view this post on Zulip Adam Topaz (Oct 08 2020 at 22:21):

I'll still wait for the checks to pass, just to make sure the renaming didn't cause any issues I didn't notice.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 22:30):

You can already open a PR. It won't get merged till it passes CI anyway.

view this post on Zulip Adam Topaz (Oct 08 2020 at 22:49):

#4545


Last updated: May 16 2021 at 05:21 UTC