Zulip Chat Archive

Stream: maths

Topic: filter disease


view this post on Zulip Patrick Massot (Aug 07 2018 at 17:33):

This feels really strange: I just caught myself writing a long string of manipulations involving filters pull-backed, push-forwarded, multiplied and compared, because it felt easier than thinking in terms of compositions of limits and such things

view this post on Zulip Patrick Massot (Aug 07 2018 at 17:37):

The key point is how filters allow to talk about limits when x tends to x' while staying in the image of a dense embedding.

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 17:55):

It's on my to-do list to understand if and when filters can be pulled back and pushed forward

view this post on Zulip Patrick Massot (Aug 07 2018 at 17:57):

filters live on bare sets, hence can be pulled back and pushed forward by bare set morphisms

view this post on Zulip Patrick Massot (Aug 07 2018 at 17:57):

aka any map

view this post on Zulip Patrick Massot (Aug 07 2018 at 17:59):

both operation are order preserving. And f_*F \le G iff F \le f^*G

view this post on Zulip Patrick Massot (Aug 07 2018 at 18:00):

Now let's do composition of limits. f goes to G along F (I don't know how to pronounce this) if, by definition, f_*F \le G. Now it's an exercise for you

view this post on Zulip Patrick Massot (Aug 07 2018 at 18:01):

of course f_* is covariantly functorial

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 18:05):

Are they adjoint functors? @Kenny Lau you'd like this stuff

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 18:06):

You'll soon be complaining that they teach limits wrong at Imperial. Did you see my filter blog post? Maybe you know all this stuff already

view this post on Zulip Patrick Massot (Aug 07 2018 at 18:09):

What would be Hom between two filters?

view this post on Zulip Patrick Massot (Aug 07 2018 at 18:10):

sorry

view this post on Zulip Patrick Massot (Aug 07 2018 at 18:11):

you mean for the poset structure?

view this post on Zulip Patrick Massot (Aug 07 2018 at 18:12):

Yes, we have f_*f^*G \le G and F \le f^f_F for all F and G

view this post on Zulip Patrick Massot (Aug 07 2018 at 18:13):

I must be careful not to be carried away, or else I'll be tempted to teach this to innocent students

view this post on Zulip Patrick Massot (Aug 07 2018 at 18:21):

where are adjoint functors in mathlib now that we got a category PR accepted?

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 18:48):

You're right, I guess it must be like the opens in a top space, the inclusions are the only morphisms, and the one equation you mentioned above is I guess precisely the affirmative answer

view this post on Zulip Patrick Massot (Aug 07 2018 at 21:38):

I managed to abstract the lemma I was using three times in my proof.

import analysis.topology.continuity

open set filter

variables {α : Type*} [topological_space α]
variables {β : Type*} [topological_space β]
variables {γ : Type*}
variables {δ : Type*} [topological_space δ]

variables {e : α  β} {f : γ  α} {g : γ  δ} {h : δ  β}
/-
 γ -f→ α
g↓     ↓e
 δ -h→ β
-/

lemma key  {d : δ} {a : α} (H : tendsto h (nhds d) (nhds (e a))) (comm : h  g = e  f)
  (de : dense_embedding e) :  tendsto f (vmap g (nhds d)) (nhds a) :=
begin
  have lim1 : map g (vmap g (nhds d))  nhds d := map_vmap_le,
  replace lim1 : map h (map g (vmap g (nhds d)))  map h (nhds d) := map_mono lim1,
  rw [filter.map_map, comm,  filter.map_map, map_le_iff_le_vmap] at lim1,
  have lim2 :  vmap e (map h (nhds d))   vmap e  (nhds (e a)) := vmap_mono H,
  rw de.induced at lim2,
  exact le_trans lim1 lim2,
end

view this post on Zulip Patrick Massot (Aug 07 2018 at 21:39):

@Johannes Hölzl I hope you're proud of me. But I'd still be interested if there is a smarter proof (or if it's already in mathlib).

view this post on Zulip Patrick Massot (Aug 07 2018 at 21:40):

By the way, why isn't dense_embedding a class?

view this post on Zulip Patrick Massot (Aug 07 2018 at 21:41):

Also, I find it a bit painful that the map is an implicit argument in map_mono and vmap_mono.

view this post on Zulip Patrick Massot (Aug 07 2018 at 21:42):

Now I'll go sleeping, feeling I've learned some nice stuff today.

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 21:54):

+1 for the commutative diagram!

view this post on Zulip Scott Morrison (Aug 08 2018 at 01:12):

where are adjoint functors in mathlib now that we got a category PR accepted?

Sorry to disappoint, @Patrick Massot, but only the first epsilon of category theory has been PR'd. It's a ways to go before you have adjoint functors.

view this post on Zulip Reid Barton (Aug 08 2018 at 03:19):

However, adjoint functors between posets are Galois connections, and they are in mathlib (order/galois_connection.lean).

view this post on Zulip Johannes Hölzl (Aug 08 2018 at 05:34):

@Johannes Hölzl I hope you're proud of me. But I'd still be interested if there is a smarter proof (or if it's already in mathlib).

Looks good to me. I don't think there is a related proof in mathlib. I'm on a bike trip this week, I can check out next Monday.

view this post on Zulip Patrick Massot (Aug 08 2018 at 10:44):

@Scott Morrison Sorry about this joke. I know it's only the beginning, I did look at your PR.

view this post on Zulip Patrick Massot (Aug 08 2018 at 11:04):

There is no hurry at all. The more difficult question is: how should we name that?

view this post on Zulip Patrick Massot (Aug 08 2018 at 11:21):

And also I'm a bit confused by the relation between dense_embedding and embedding in mathlib. My lemma actually doesn't use the dense part, but it uses the way the induced axiom is stated. But I guess it could be stated that way for embeddings too, right?


Last updated: May 06 2021 at 18:20 UTC