filters

Stream: general

[Rohan Mitta]

Hi,

I'm attempting to prove a proposition from a Topology book and am getting stuck using filters, which I'm not very comfortable with in lean. Can anyone help me with the first sorry? I'm pretty sure that step is true due to the uniform continuity of f but I can't figure out what to do with it.

import analysis.topology.topological_space
import analysis.topology.continuity
import analysis.metric_space
import analysis.topology.uniform_space
import order.filter

noncomputable theory

theorem complete_iff_of_uniform_cts_bij {α : Type*} [metric_space α] {β : Type*} [metric_space β] (f : α → β)
    (g : β → α) (Hf : uniform_continuous f) (Hg : uniform_continuous g) (left_inv : function.left_inverse g f)
    (right_inv : function.right_inverse g f) : complete_space α ↔ complete_space β :=
begin
  split,
    intro H1,
    cases H1, split,
    intros filt Hfilt,

    have H2 := H1 (cauchy_map Hg Hfilt),
    cases H2 with x H_converges_to_x,
    existsi f x,
    rw filter.map_le_iff_le_vmap at H_converges_to_x,
    have Hmaps := filter.map_eq_vmap_of_inverse (function.id_of_right_inverse right_inv) (function.id_of_left_inverse left_inv),
    rw ← Hmaps at H_converges_to_x,
    have H3 : filter.map f (nhds x) = nhds (f x),

      sorry,
    rw H3 at H_converges_to_x, exact H_converges_to_x,
  sorry,

end

[Reid Barton]

H3 must be true because nhds only depends on the topology and f and g are homeomorphisms.
One direction of the equality will be from continuous.tendsto. The other one should require the continuity of g

[Johannes Hölzl]

Also, you have an uniform isomorphism (i.e. f with g as inverse). This implies that it is an topological embedding, a dense_embedding and uniform_embedding. If you look for them this should give you enough rules to prove your statement.

[Reid Barton]

... plus either left_inv or right_inv, and filter.map_map

[Patrick Massot]

@Rohan Mitta don't listen to them, you were almost done. Stating only only implication since the other one follows by symmetry:

theorem complete_iff_of_uniform_cts_bij {α : Type*} [metric_space α] {β : Type*} [metric_space β] (f : α → β)
    (g : β → α) (Hf : uniform_continuous f) (Hg : uniform_continuous g) (left_inv : function.left_inverse g f)
    (right_inv : function.right_inverse g f) : complete_space α → complete_space β :=
begin

  intro H1,
  cases H1, split,
  intros filt Hfilt,

  have H2 := H1 (cauchy_map Hg Hfilt),
  cases H2 with x H_converges_to_x,
  existsi f x,
  rw filter.map_le_iff_le_vmap at H_converges_to_x,
  have Hmaps := filter.map_eq_vmap_of_inverse (function.id_of_right_inverse right_inv) (function.id_of_left_inverse left_inv),
  rw ← Hmaps at H_converges_to_x,
  have := continuous.tendsto Hf.continuous x,
  exact le_trans H_converges_to_x this
end

[Kevin Buzzard]

Thanks all of you (I'm sitting next to Rohan)

[Rohan Mitta]

Amazing, thanks everyone!

[Patrick Massot]

Small cleanup:

open function
theorem complete_iff_of_uniform_cts_bij {α : Type*} [metric_space α] {β : Type*} [metric_space β] (f : α → β)
    (g : β → α) (Hf : uniform_continuous f) (Hg : uniform_continuous g) (left_inv : function.left_inverse g f)
    (right_inv : function.right_inverse g f) : complete_space α → complete_space β :=
begin
  rintro ⟨H1⟩,
  split,
  intros filt Hfilt,

  cases H1 (cauchy_map Hg Hfilt) with x H_converges_to_x,
  existsi f x,
  rw [filter.map_le_iff_le_vmap,
      ←filter.map_eq_vmap_of_inverse (id_of_right_inverse right_inv) (id_of_left_inverse left_inv)] at H_converges_to_x,

  exact le_trans H_converges_to_x (continuous.tendsto Hf.continuous x)
end

[Johannes Hölzl]

Thanks Patrick to actually look at the proof (obviously, I didn't ...)

[Johan Commelin]

Is there a particular reason that filter is only defined for set X. (I.e., a filter is a set of sets, etc...). The definition makes sense for arbitrary bounded lattices, of which set X is a particular instance. (And most of the basic lemmas are also true in this more general setting.) Is this to avoid the extra type class in basic files?

[Patrick Massot]

I think @Jeremy Avigad considered doing that, but I don't know what came out of this idea.

[Sebastien Gouezel]

Is there a useful application of the generalization?

[Patrick Massot]

I guess it depends who you ask... I certainly wouldn't want traditional filters to become less convenient to use after generalizing. They are everywhere in our topology library.

[Patrick Massot]

https://ncatlab.org/nlab/show/filter gives the general definition (of course) but doesn't seem to mention any application outside topology

[Johan Commelin]

The category of bounded distributive lattices is anti-equivalent to the category of spectral spaces via a "Spec" functor. It associates to a bounded distributive lattice the set of prime filters.

[Johan Commelin]

A filter F on a lattice is prime if x \glb y \in F → x \in F \or y \in F

[Johan Commelin]

This is probably not enough justification for the generalisation, though

[Jeremy Avigad]

Actually, it was @Mario Carneiro who actually started doing it, and got pretty far with the generalization, IIRC. I don't know what came of it.

[Mario Carneiro]

I got bogged down in the propagating library changes. I pushed my WIP on this to the pfilter branch; perhaps someone wants to pick this back up.

[Johan Commelin]

@Mario Carneiro Thanks for this branch

[Johan Commelin]

I see you went even more general than lattices, and just used preorders. Were you planning on having some special layer on top of that for filters on lattices?

[Johan Commelin]

It's not too encouraging that such a refactor is getting you bogged down... I wish we had better tools for refactoring.