## Stream: maths

### Topic: filter disease

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

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

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

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

aka any map

#### Patrick Massot (Aug 07 2018 at 17:59):

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

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

#### Patrick Massot (Aug 07 2018 at 18:01):

of course f_* is covariantly functorial

#### Kevin Buzzard (Aug 07 2018 at 18:05):

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

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

#### Patrick Massot (Aug 07 2018 at 18:09):

What would be Hom between two filters?

sorry

#### Patrick Massot (Aug 07 2018 at 18:11):

you mean for the poset structure?

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

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

#### Patrick Massot (Aug 07 2018 at 18:21):

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

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

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


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

#### Patrick Massot (Aug 07 2018 at 21:40):

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

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

#### Patrick Massot (Aug 07 2018 at 21:42):

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

#### Kevin Buzzard (Aug 07 2018 at 21:54):

+1 for the commutative diagram!

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

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

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

#### Patrick Massot (Aug 08 2018 at 10:44):

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?