More point set topology questions

Stream: Is there code for X?

[Adam Topaz]

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

[Adam Topaz]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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?

[Adam Topaz]

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.

[Yury G. Kudryashov]

I opened issue #4543.

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Yury G. Kudryashov]

For the first one you can supply nonempty_of_ne_bot F.1

[Adam Topaz]

That's for sets.

[Adam Topaz]

I think.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

docs#filter.nonempty_of_ne_bot

[Yury G. Kudryashov]

We don't have this instance!

[Adam Topaz]

Oops!

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

I guess our is_ultrafilter API is much better.

[Yury G. Kudryashov]

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

[Adam Topaz]

I never have time.

[Adam Topaz]

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

[Yury G. Kudryashov]

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)

[Yury G. Kudryashov]

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

[Adam Topaz]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

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.

[Adam Topaz]

@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?

[Yury G. Kudryashov]

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

[Adam Topaz]

unknown identifier 'is_compact_univ'
Am I missing an import?

[Yury G. Kudryashov]

It's compact_univ

[Yury G. Kudryashov]

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

[Adam Topaz]

No worries. Found it now.

[Adam Topaz]

Pushed the change just now.

[Adam Topaz]

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

[Yury G. Kudryashov]

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

[Adam Topaz]

#4545