filter disease

Stream: maths

[Patrick Massot]

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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

aka any map

[Patrick Massot]

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

[Patrick Massot]

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]

of course f_* is covariantly functorial

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

What would be Hom between two filters?

[Patrick Massot]

sorry

[Patrick Massot]

you mean for the poset structure?

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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]

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

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

+1 for the commutative diagram!

[Scott Morrison]

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]

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

[Johannes Hölzl]

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

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

[Patrick Massot]

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

[Patrick Massot]

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?