Zulip Chat Archive

Stream: maths

Topic: Separation stuff


Patrick Massot (Sep 19 2018 at 14:59):

@Johannes Hölzl I'm working on uniform spaces again, and I have a couple of question.

  • First, at https://github.com/leanprover/mathlib/blob/master/analysis/topology/topological_space.lean#L638-L640 the comment mentions two possible definitions of T1 spaces. Am I right to think the equivalence of those definitions is not in mathlib?
  • Bourbaki defines separated uniform spaces as uniform spaces whose underlying topology is T2. You define them in terms of the separation relation, and prove the underlying topological space is T2. But you don't prove the converse implication, do you?
  • When trying to prove the converse implication on paper, I get that T1 underlying topology is enough. Is this fishy? Or is it only that topologies coming from uniform structures are special and T1 implies T2 (and regular)?

Reid Barton (Sep 19 2018 at 15:23):

T1 implies T2 for uniform spaces should be the same epsilon/2 as shows metric spaces are T2

Reid Barton (Sep 19 2018 at 15:25):

Uh, on my phone and apparently can't form complete sentences but I guess you understand what I mean.

Patrick Massot (Sep 19 2018 at 15:26):

Indeed it looks very plausible, but I wanted to check with our local expert before starting to Lean it

Patrick Massot (Sep 19 2018 at 15:43):

I now have a really detailed paper proof of the fact that the group uniform structure on the completion of a group is the same as the completion of the group uniform structure. I have about 15 lemmas to state and prove in Lean. I'm really afraid because lots of them involve different uniform structures on the same type, and I don't know how to fight the type class resolution system here.

Patrick Massot (Sep 19 2018 at 16:37):

Ok, I decided to start with a lemma which is independent of all the group theory stuff and openly involves different uniform structures on the same type.

import analysis.topology.uniform_space
open set

variables {α : Type*} {β : Type*}

lemma uniform_continuous_id_of_emb [uniform_space α] (u u' : uniform_space β) (top : u.to_topological_space = u'.to_topological_space)
  {e : α  β} (ue : @uniform_embedding _ _ _ u e) (dense : x, x  closure (range e))
  (h : @uniform_continuous _ _ _ u' e) :  u  u' :=
begin
  let e₀ := (ue.dense_embedding dense).extend e,

  sorry
end

As expected, lots of @/_ flying around. First surprise: how does Lean accepts the dense hypothesis? Where does it get a topology on beta? I was expecting to need to need @ here, pick at random from u to u' and then use the topo hypothesis in the proof. And then Lean complains when I define e₀: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized u' inferred u. Here I want to use uniform structure u. How can I proceed?

Patrick Massot (Sep 19 2018 at 18:17):

Any hint about this?

Johannes Hölzl (Sep 19 2018 at 18:20):

first observation: in dense, the type class instances find somehow u'

Johannes Hölzl (Sep 19 2018 at 18:21):

For some reasons it also uses non-type class parameters...

Patrick Massot (Sep 19 2018 at 18:22):

Yes, this is what confuses me

Johannes Hölzl (Sep 19 2018 at 18:22):

the type class inference will use u if you swap u' and u. then u will be used in dense, and e₀ works

Johannes Hölzl (Sep 19 2018 at 18:22):

but this is surely not reliable.

Patrick Massot (Sep 19 2018 at 18:23):

Of course square brackets are meant to indicate how these arguments will be supplied when applying the lemma. But somehow I thought they also indicated what to put in the type class system for immediate use in following arguments

Patrick Massot (Sep 19 2018 at 18:23):

I thought about swapping, but I wanted a robust solution

Patrick Massot (Sep 19 2018 at 18:24):

And , while you're here, this thread starts with three questions for you...

Johannes Hölzl (Sep 19 2018 at 18:24):

to have it robust you need to use the @... notation

Patrick Massot (Sep 19 2018 at 18:26):

My son requires me, you have some extra thinking time :smile:

Johannes Hölzl (Sep 19 2018 at 18:27):

1) heh, the comment is the wrong way around. All we have specifically for T1 is the three theorem below the class. So AFAIR: no this equivalence is not in mathlib.

Kevin Buzzard (Sep 19 2018 at 18:27):

import analysis.topology.uniform_space
open set

variables {α : Type*} {β : Type*}

--set_option trace.class_instances true
lemma uniform_continuous_id_of_emb (u : uniform_space β)
 : false :=
begin
  have u' : uniform_space β := by apply_instance, -- works??
--  have : u = u' := rfl, -- fails??
  sorry
end

Kevin Buzzard (Sep 19 2018 at 18:27):

this is horrible

Johannes Hölzl (Sep 19 2018 at 18:28):

2) no the converse is not proved

Johannes Hölzl (Sep 19 2018 at 18:30):

3) Reid's comment makes sense to me.

Chris Hughes (Sep 19 2018 at 18:30):

@Kevin Buzzard you used have instead of let.

Kevin Buzzard (Sep 19 2018 at 18:31):

thank goodness for that

Kevin Buzzard (Sep 19 2018 at 18:31):

and not for the first time

Johannes Hölzl (Sep 19 2018 at 18:33):

@Patrick Massot do you work with: I. M. James: Topologies and Uniformities? This is what I used to formalize most of uniform spaces.

Kevin Buzzard (Sep 19 2018 at 18:33):

import analysis.topology.uniform_space
open set

variables {α : Type*} {β : Type*}

lemma uniform_continuous_id_of_emb [uniform_space α] (u u' : uniform_space β)
 : false :=
begin
  let βtop : topological_space β := by apply_instance, -- ??
  have : βtop = @uniform_space.to_topological_space β u' := rfl,
  sorry
end

Kevin Buzzard (Sep 19 2018 at 18:34):

So as Johannes says, type class inference picks up u' and it's not clear why

Kevin Buzzard (Sep 19 2018 at 18:43):

How can I proceed?

Well we now see the problem; type class inference succeeds when it shouldn't, so...

import analysis.topology.uniform_space
open set

variables {α : Type*} {β : Type*}

lemma uniform_continuous_id_of_emb [uniform_space α] (u u' : uniform_space β) (top : u.to_topological_space = u'.to_topological_space)
  {e : α  β} (ue : @uniform_embedding _ _ _ u e) (dense : x, x  @closure β (u.to_topological_space) (range e))
  (h : @uniform_continuous _ _ _ u' e) :  u  u' :=
begin
  let e₀ := @dense_embedding.extend _ β β _ (u.to_topological_space) e (u'.to_topological_space)
    (@uniform_embedding.dense_embedding _ _ _ u _ ue dense) e,

  sorry
end

I don't know what you're complaining about :-)

Johan Commelin (Sep 19 2018 at 18:44):

Did you steel Scott's monitor?

Johan Commelin (Sep 19 2018 at 18:44):

Those lines are way too long. :rolling_on_the_floor_laughing:

Kevin Buzzard (Sep 19 2018 at 18:44):

Here is a possible workaround: use beta and gamma with an equiv, let u be the uniform structure on beta and u' on gamma

Kevin Buzzard (Sep 19 2018 at 18:44):

Those lines are way too long. :rolling_on_the_floor_laughing:

I even halved the longest one!

Kevin Buzzard (Sep 19 2018 at 18:45):

and then you won't get the problems

Kevin Buzzard (Sep 19 2018 at 18:45):

and you can just push forward and pull back the uniformities.

Kevin Buzzard (Sep 19 2018 at 18:46):

This might actually work. But of course the question still remains as to how type class inference is stealing your uniformities. This is very funny. It's exactly the opposite of the complaint most of my student have -- "I can see it in the local context, how come Lean doesn't know why R is a ring?"

Johannes Hölzl (Sep 19 2018 at 18:49):

ah yes, when you move the parameters u and u' to the right side of :, then it doesn't work anymore:

lemma uniform_continuous_id_of_emb [uniform_space α] :
  (u u' : uniform_space β) (top : u.to_topological_space = u'.to_topological_space)
  {e : α  β} (ue : @uniform_embedding _ _ _ u e)
  (dense : x, x  closure (range e)) -- fails here
  (h : @uniform_continuous _ _ _ u' e), u  u' := ...

Kevin Buzzard (Sep 19 2018 at 18:50):

So when Leo said only stuff to the left of the colon could be used for type class inference, I didn't realise he meant that even stuff which we didn't want to use would get used...

Kevin Buzzard (Sep 19 2018 at 18:50):

Is this just for uniform spaces or does everything do this?

Johannes Hölzl (Sep 19 2018 at 18:50):

I guess everything?!

Johannes Hölzl (Sep 19 2018 at 18:51):

maybe only things which are marked as @[class]?

Kevin Buzzard (Sep 19 2018 at 18:51):

lemma test (α : Type) (u : ring α) : false :=
begin
  let v : ring α := by apply_instance,
  -- who knew that this worked??
  have : u = v := rfl,
  sorry
end

Kevin Buzzard (Sep 19 2018 at 18:51):

Is this a bug??

Mario Carneiro (Sep 19 2018 at 18:52):

I'm confused, why is this a surprise

Mario Carneiro (Sep 19 2018 at 18:52):

you asked for an instance, it found one

Kevin Buzzard (Sep 19 2018 at 18:52):

Patrick, even though Johannes has pointed out a fix, the more I think about the gamma trick the more I think you should consider it seriously. Then you can just use type class inference for beta with u and gamma with u', and deduce the actual thing you want afterwards with a minimal amount of @

Kevin Buzzard (Sep 19 2018 at 18:52):

I just had absolutely no idea that it would look there

Mario Carneiro (Sep 19 2018 at 18:53):

isn't that where it normally looks?

Kevin Buzzard (Sep 19 2018 at 18:53):

I thought there was the square bracket stuff and the round bracket stuff

Kevin Buzzard (Sep 19 2018 at 18:53):

and it only looked in the square bracket stuff

Mario Carneiro (Sep 19 2018 at 18:54):

Ah, I see. The square bracket only affects users of the theorem, it doesn't matter what you mark it when it's in the context

Mario Carneiro (Sep 19 2018 at 18:54):

the only thing that matters inside the theorem is whether the head constant is a @[class]

Kevin Buzzard (Sep 19 2018 at 18:54):

I see!

Johannes Hölzl (Sep 19 2018 at 18:55):

Hm, this is also news to me!

Kevin Buzzard (Sep 19 2018 at 18:56):

In which case Patrick I think this is an even bigger indication that you should just work with two different types and maps between them, and in the application make the types the same

Kevin Buzzard (Sep 19 2018 at 18:57):

Hopefully this solves some blockages higher up the chain of problems as well. I didn't know things worked like this, and presumably Patrick didn't either -- but I do remember him saying that he could not actually solve some problems with type classes because he could not direct his instances in the right direction. This will hopefully clear a lot of stuff up.

Johannes Hölzl (Sep 19 2018 at 18:58):

I also think it is a good idea to use two types and a uniform equivalence between them. The annoying this is: this may force you to prove for a lot of constants, that they are invariant under equivalences

Kevin Buzzard (Sep 19 2018 at 18:59):

I guess the reason many users didn't notice this is simply because it is very rare to actually have two terms of type foo X with foo a class, which you actually want to be distinct; usually users are wrestling to prove that they are the equal, not the other way around.

Johannes Hölzl (Sep 19 2018 at 18:59):

yes, type classes work so well, exactly for this reason: if you assume two different structures, you usually have two different types

Kevin Buzzard (Sep 19 2018 at 19:00):

I also think it is a good idea to use two types and a uniform equivalence between them. The annoying this is: this may force you to prove for a lot of constants, that they are invariant under equivalences

@Simon Hudon This is back to transport de structure. Deligne emphasized this concept in his IAS lecture last week.

Kevin Buzzard (Sep 19 2018 at 19:01):

Patrick is about to need the fact that if he has h : equiv X Y and a topological space structure on X, then all topology-like theorems he proves for X should have an analogue for Y obtained by mapping and co-mapping along h.

Johannes Hölzl (Sep 19 2018 at 19:05):

we need to extensions of equiv: continuous_equiv and uniform_equiv. We also assume a topological structure on Y (it may be the one induced by h, but this shouldn't be necessary def-equal)

Mario Carneiro (Sep 19 2018 at 19:14):

isn't continuous_equiv just homeo?

Johannes Hölzl (Sep 19 2018 at 19:15):

yes

Kevin Buzzard (Sep 19 2018 at 19:22):

I feel like we have taken a big step forward here though. My solution with long lines would have been hell and Patrick was complaining some time ago that he could not control his instances. I realised the other reason that this phenomenon was not well known -- if you have a term whose type is a class, 99% of the time you put it in square brackets in the statement of a theorem or definition

Patrick Massot (Sep 19 2018 at 19:30):

I'm back. Thanks everybody for your work on this.

Patrick Massot (Sep 19 2018 at 19:31):

I'm not sure I'm buying the two types solutions. The problem is that I'm not intersted in this lemma in isolation, it's a tiny step in a much bigger proof

Patrick Massot (Sep 19 2018 at 19:31):

So I'll actually need to apply this lemma

Simon Hudon (Sep 19 2018 at 19:45):

@Kevin Buzzard: @Johannes Hölzl keeps pointing out that transport overlaps with his transfer machinery. I think it would be worth checking if transfer solves your problems right out of the box.

Johannes Hölzl (Sep 19 2018 at 19:46):

it doesn't solve them right out of the box. It still requires quite some infrastructure. But I think it is less work to extend transfer than to implement a transport

Kevin Buzzard (Sep 19 2018 at 20:01):

I would like to hear much more about what is going on here. I don't know what either of these words are. Are they tactics? I remember having a lot of fun working towards transport. Maybe we have an actual use case here. Presumably Johannes in his message above has pinpointed exactly what we need in this situation

Kevin Buzzard (Sep 19 2018 at 20:03):

Patrick if you try and prove the lemma using just one beta then you have an @ nightmare. If you prove it using beta and gamma then you have a different problem which might be easily solvable and furthermore your lemma will be a more general result. You can get the lemma you want by applying the more general one in the case beta = gamma and then you are only in @ hell for a few lines

Patrick Massot (Sep 19 2018 at 20:04):

I think this is a very important topic, so I'll probably try a couple of solutions

Patrick Massot (Sep 19 2018 at 20:04):

I still need to know how I can use my "same topology hypothesis" to deduce that the range of e is dense for for topologies

Kevin Buzzard (Sep 19 2018 at 20:05):

This is very much like how transport de structure works in Galois theory. You first do it with an isomorphism X = Y and then apply it with X=Y but the isomorphism not equal to the identity and you deduce something which might look like a nontrivial computation with no work

Andrew Ashworth (Sep 19 2018 at 20:06):

transfer is a tactic, used in core lean to prove various properties of integers

Patrick Massot (Sep 19 2018 at 20:08):

Kevin, you heard about it in Orsay

Kevin Buzzard (Sep 19 2018 at 20:12):

Oh I remember! I hadn't put two and two together.

Patrick Massot (Sep 19 2018 at 20:19):

This fight against @ is epic. Did I tell you I forgot to assume both uniformities on β are complete and separated?

Patrick Massot (Sep 19 2018 at 20:20):

I tried to cut my proof into so many tiny lemmas that I forgot to copy-paste a couple of assumptions

Patrick Massot (Sep 19 2018 at 20:26):

set_option pp.all true is my only ally

Patrick Massot (Sep 19 2018 at 20:27):

rewrite tactic failed, motive is not type correct nested exception message: check failed, application type mismatch (use 'set_option trace.check true' for additional details) is my enemy

Kevin Buzzard (Sep 19 2018 at 20:28):

Now I am confused about why something which transfers proofs from N x N to Z can help. I think I need to think about how transfer actually works. But with the beta gamma approach there are no @s at all and you can just use type class inference as usual.

Kevin Buzzard (Sep 19 2018 at 20:29):

In fact I would be tempted to see how much you can do with beta not assumed equal to gamma and not ever prove anything with beta = gamma unless you absolutely have to.

Patrick Massot (Sep 19 2018 at 20:30):

You can try to prove the lemma if you want (without forgetting to assume both structures on target are complete and separated)

Johannes Hölzl (Sep 19 2018 at 20:31):

transfer doesn't require an equivalence, just a relation and proofs about terms related terms. That's how proofs about Z can be reduced to proofs about N x N

Kevin Buzzard (Sep 19 2018 at 20:34):

I guess I would need to know the maths statement and proof...

Patrick Massot (Sep 19 2018 at 20:36):

Here is the real world story (using A and B instead of greek letters for typing convenience). We have A with a fixed uniform structure, and B with two complete separated uniform structure u and u', which induce the same topology on B. We have e : A to B which is a uniform embedding into (B, u) with dense image. We assume e is uniformly continuous from A to (B, u'). Hence it can be extended by continuity to some uniformly continuous e0 from (B, u) to (B, u'). Since e0 \circ e = e, we learn the e0 is the identity on the image of e. But the later is dense, so by continuity, e0 = Id. So we learned that Id is uniformly continuous from (B, u) to (B, u'), QED.

Patrick Massot (Sep 19 2018 at 20:37):

As is often the case, the paper I have in front of me contains only an annotated commutative diagram.

Kevin Buzzard (Sep 19 2018 at 20:38):

Can we work on this together at cocalc (possibly at different times)?

Kevin Buzzard (Sep 19 2018 at 20:39):

or is it easier just to spam the chat with gists?

Patrick Massot (Sep 19 2018 at 20:39):

Here my full Lean so far:

import analysis.topology.uniform_space

open set
variables {α : Type*} {β : Type*}

def unif_emb {α : Type*} {β : Type*} (u_α : uniform_space α) (u_β : uniform_space β) (f : α  β) : Prop :=
uniform_embedding f

def unif_cont {α : Type*} {β : Type*} (u_α : uniform_space α) (u_β : uniform_space β) (f : α  β) : Prop :=
uniform_continuous f

def top (u : uniform_space α):= u.to_topological_space

def complete (u : uniform_space α) := complete_space α

def hausdorff (u : uniform_space α) := separated α

set_option pp.all true
lemma uniform_continuous_id_of_emb [ : uniform_space α] (u' u : uniform_space β)
  [cu : complete u] [hu : hausdorff u] [cu' : complete u'] [hu' : hausdorff u'] (htop : top u = top u')
  {e : α  β} (ue : unif_emb  u e) (dense : x, x  closure (range e))
  (h : unif_cont  u' e) :  u  u' :=
begin
  let e₀ := (ue.dense_embedding dense).extend e,
  haveI : separated β := hu,
  have : unif_cont u u' e₀,
  { dsimp [unif_cont, e₀],
    have := @uniform_continuous_uniformly_extend β α β u  u' e ue dense e h cu' hu',
    dsimp [top] at htop,

    sorry },

  sorry
end

Kevin Buzzard (Sep 19 2018 at 20:39):

I am trying to help my daughter with biology homework, clean the kitchen, eat some dinner and prove a lemma

Patrick Massot (Sep 19 2018 at 20:39):

A CoCalc effort would probably be fun

Patrick Massot (Sep 19 2018 at 20:40):

As you can see, I tried to hide a bunch of @ in new definitions which simply change binders

Patrick Massot (Sep 19 2018 at 20:41):

The bad side is we need dsimp then

Mario Carneiro (Sep 19 2018 at 20:45):

That real world proof looks applicable where the types are different. The only tricky bit is "generating the same topology", but I think this just means that the equiv is a quotient map (in the topological sense)

Patrick Massot (Sep 19 2018 at 20:45):

The relevant part of state is then

this :
  @uniform_continuous.{u_2 u_2} β β u u'
    (@dense_embedding.extend.{u_1 u_2 u_2} α β β (@uniform_space.to_topological_space.{u_1} α )
       (@uniform_space.to_topological_space.{u_2} β u)
       e
       (@uniform_space.to_topological_space.{u_2} β u')
       (@uniform_embedding.dense_embedding.{u_1 u_2} α β  u e ue dense)
       e),
htop :
  @eq.{u_2+1} (topological_space.{u_2} β) (@uniform_space.to_topological_space.{u_2} β u)
    (@uniform_space.to_topological_space.{u_2} β u')
 @uniform_continuous.{u_2 u_2} β β u u'
    (@dense_embedding.extend.{u_1 u_2 u_2} α β β (@uniform_space.to_topological_space.{u_1} α )
       (@uniform_space.to_topological_space.{u_2} β u)
       e
       (@uniform_space.to_topological_space.{u_2} β u)
       (@uniform_embedding.dense_embedding.{u_1 u_2} α β  u e ue dense)
       e)

So it looks like rwa htop at this should close the goal, but I get a that nasty error instead

Patrick Massot (Sep 19 2018 at 20:46):

(deleted)

Kevin Buzzard (Sep 19 2018 at 20:46):

Here is the version which is written in what I believe is the correct generality (using A and B and C instead of greek letters for typing convenience). We have A, B, C uniform spaces, with B and C uniform and complete, and a homeo j : B -> C. We have e : A to B which is a uniform embedding into B with dense image. We assume j circ e is uniformly continuous from A to C. Hence it can be extended by continuity to some uniformly continuous j' from B to C. Since j = j' on e(A), j = j' and hence j is uniformly continuous from B to C, QED without a single @

Patrick Massot (Sep 19 2018 at 20:48):

I'll try to prove that tomorrow, but I fear this is only pushing the pain to the moment I will need to apply the lemma

Mario Carneiro (Sep 19 2018 at 20:49):

we need the theorem that id is uniformly continuous from u to u' iff u <= u'

Mario Carneiro (Sep 19 2018 at 20:49):

that is the only part that really needs @ work, and the proof is trivial using map_id on filters

Patrick Massot (Sep 19 2018 at 20:50):

Sure, we need this id stuff.

Patrick Massot (Sep 19 2018 at 20:50):

But I don't understand the next sentence

Patrick Massot (Sep 19 2018 at 20:51):

And I don't understand why rewrite doesn't work in my attempt.

Johannes Hölzl (Sep 19 2018 at 20:53):

uniform continuity works on pairs of function, i.e. you need to prove (λx:α×α, (x.1, x.2)) = id

Johannes Hölzl (Sep 19 2018 at 20:54):

and then unfold uniform_continuity and rewrite with this equality

Patrick Massot (Sep 19 2018 at 20:56):

Sure, but this is completely orthogonal to my problem, right?

Patrick Massot (Sep 19 2018 at 20:56):

I'm far away from having that id is uniformly continuous here

Kevin Buzzard (Sep 19 2018 at 20:59):

Do we have homeomorphisms in the strong sense of a continuous equiv with a continuous inverse?

Johannes Hölzl (Sep 19 2018 at 21:00):

no :(

Patrick Massot (Sep 19 2018 at 21:01):

https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/homeos.lean

Patrick Massot (Sep 19 2018 at 21:01):

Would you like to get this in mathlib?

Patrick Massot (Sep 19 2018 at 21:02):

I need to go sleeping, but don't hesitate to unblock this. I hope I could then imitate the solution in many other such lemmas

Kevin Buzzard (Sep 19 2018 at 21:04):

Patrick here is the statement with beta ne gamma:

lemma uniform_continuous_id_of_emb' [ : uniform_space α] [uniform_space β] [uniform_space γ]
  [complete_space β] [separated β] [complete_space γ] [separated γ] (j : equiv β γ) -- need cts
  {e : α  β} (ue : uniform_embedding e) (dense : x, x  closure (range e))
  (h : uniform_continuous (j  e)) :  uniform_continuous j := sorry

I had to use none of your five binder-changing defs

Patrick Massot (Sep 19 2018 at 21:09):

Weird! My rewrite now works

Patrick Massot (Sep 19 2018 at 21:09):

I wanted to try one more time. I have no idea what changed

Patrick Massot (Sep 19 2018 at 21:11):

Thanks Kevin. I'll definitely try this road tomorrow

Patrick Massot (Sep 19 2018 at 21:11):

But, as I wrote earlier, I think it's important enough that I try several things

Johannes Hölzl (Sep 19 2018 at 21:13):

wait, does the statement hold at all?

Johannes Hölzl (Sep 19 2018 at 21:13):

How do you want to prove it? (ah, reading your previous description)

Johannes Hölzl (Sep 19 2018 at 21:17):

  have : unif_cont u u' e₀,
  { dsimp [unif_cont, e₀],
    have := @uniform_continuous_uniformly_extend β α β u  u' e ue dense e h cu' hu',
    dsimp [top] at htop,
    rwa [htop] {occs := occurrences.pos [2]} },

the have can be proved fixing the occurence. I guess the e₀ = id proof doesn't mention any uniformities?

Kevin Buzzard (Sep 19 2018 at 21:22):

Oh -- I should add that my formalisation is not quite correct because the equiv should be a homeo

Kevin Buzzard (Sep 19 2018 at 21:25):

Hmm, we seem to need the theorem that id is uniformly continuous from u to u' iff u <= u'. But I would rather prove a statement that an equiv is uniformly continuous iff some pushforward of a uniformity is <= the other one. Is this already in Lean?

Johannes Hölzl (Sep 19 2018 at 21:30):

this holds by definitional equality. EDIT: no, it doesn't

Kevin Buzzard (Sep 19 2018 at 21:40):

def unif_cont {α : Type*} {β : Type*} (u_α : uniform_space α) (u_β : uniform_space β) (f : α  β) : Prop :=
uniform_continuous f

Is this OK if alpha = beta? I'm not so sure. I think type class inference chooses the same uniform structure twice. @Patrick Massot I think there's a bug here. Thoughts anyone?

Johannes Hölzl (Sep 19 2018 at 21:47):

lemma uniform_continuous_iff {α β} [ : uniform_space α] [ : uniform_space β] (f : α  β):
  uniform_continuous f  .comap f   :=
filter.map_le_iff_le_comap

Johannes Hölzl (Sep 19 2018 at 21:49):

@Kevin Buzzard the content of unif_cont is fully elaborated. The elaborator doesn't do a type class search when it is used in uniform_continuous_id_of_emb

Kevin Buzzard (Sep 19 2018 at 21:50):

Oh I see. So it's Ok.

Kevin Buzzard (Sep 19 2018 at 21:50):

As you can see, I am still coming to terms with my new knowledge about how typeclass inference works. Patrick -- sorry -- it's Ok.

Kevin Buzzard (Sep 19 2018 at 21:56):

Patrick's version --

lemma uniform_continuous_id_of_emb [ : uniform_space α] (u' u : uniform_space β)
  [cu : complete u] [hu : hausdorff u] [cu' : complete u'] [hu' : hausdorff u'] (htop : top u = top u')
  {e : α  β} (ue : unif_emb  u e) (dense : x, x  closure (range e))
  (h : unif_cont  u' e) :  u  u' :=

Should the conclusion be u' <= u? I'm not an expert in uniform spaces.

Kevin Buzzard (Sep 19 2018 at 21:58):

I ask because Patrick seemed to be saying that the conclusion was that id was continuous from u to u', and Johannes seems to want to conclude from this that u' <= u. But this could easily be some situation where <= is defined as >= for some people (as far as I know)

Kevin Buzzard (Sep 19 2018 at 22:07):

There is no uniform_space.comap_id :-(

Kevin Buzzard (Sep 19 2018 at 22:57):

gaargh there seems to be no ext

Kevin Buzzard (Sep 19 2018 at 23:04):

⊢ u' = uniform_space.comap id u'

Kevin Buzzard (Sep 19 2018 at 23:23):

  have : unif_cont u u' e₀,
  { dsimp [unif_cont, e₀],
    have := @uniform_continuous_uniformly_extend β α β u  u' e ue dense e h cu' hu',
    dsimp [top] at htop,
    rwa [htop] {occs := occurrences.pos [2]} },

With the gamma version it's just

  let e₀ := (ue.dense_embedding dense).extend (j  e),
  have : uniform_continuous e₀,
  { dsimp [unif_cont, e₀],
    exact uniform_continuous_uniformly_extend ue dense h,
  },

Kevin Buzzard (Sep 19 2018 at 23:24):

Everything is easier this way, switching to gamma is a no-brainer

Kevin Buzzard (Sep 19 2018 at 23:26):

import analysis.topology.uniform_space

open set
variables {α : Type*} {β : Type*} {γ : Type*}

lemma uniform_continuous_id_of_emb' [uniform_space α] [uniform_space β] [uniform_space γ]
  [complete_space β] [separated β] [complete_space γ] [separated γ] (j : equiv β γ) -- need continuity assumption
  {e : α  β} (ue : uniform_embedding e) (dense : x, x  closure (range e))
  (h : uniform_continuous (j  e)) : uniform_continuous j :=
begin
  let e₀ := (ue.dense_embedding dense).extend (j  e),
  have : uniform_continuous e₀,
  { dsimp [e₀],
    exact uniform_continuous_uniformly_extend ue dense h,
  },
  sorry -- I need that j is a homeo and this isn't in the assumptions
end

but it's bedtime now

Kevin Buzzard (Sep 19 2018 at 23:26):

and we need to say that j is a homeo not just an equiv.

Kevin Buzzard (Sep 19 2018 at 23:28):

lemma uniform_continuous_iff {α β} [ : uniform_space α] [ : uniform_space β] (f : α  β):
  uniform_continuous f  .comap f   :=
filter.map_le_iff_le_comap

def unif_emb {α : Type*} {β : Type*} (u_α : uniform_space α) (u_β : uniform_space β) (f : α  β) : Prop :=
uniform_embedding f

def unif_cont {α : Type*} {β : Type*} (u_α : uniform_space α) (u_β : uniform_space β) (f : α  β) : Prop :=
uniform_continuous f

def top (u : uniform_space α):= u.to_topological_space

def complete (u : uniform_space α) := complete_space α

def hausdorff (u : uniform_space α) := separated α

lemma uniform_continuous_id_of_emb [ : uniform_space α] (u' u : uniform_space β)
  [cu : complete u] [hu : hausdorff u] [cu' : complete u'] [hu' : hausdorff u'] (htop : top u = top u')
  {e : α  β} (ue : unif_emb  u e) (dense : x, x  closure (range e))
  (h : unif_cont  u' e) :  u'  u :=
begin
  have H : unif_cont u u' id := @uniform_continuous_id_of_emb' α β β  u u' cu hu cu' hu' (equiv.refl β) e ue dense h,
  unfold unif_cont at H,
  rw uniform_continuous_iff at H,
  convert H,
  -- ⊢ u' = uniform_space.comap id u'
  -- should be trivial?
  sorry
end

Kevin Buzzard (Sep 19 2018 at 23:35):

have : uniform_continuous e₀ := uniform_continuous_uniformly_extend ue dense h,

Patrick Massot (Sep 20 2018 at 07:21):

Indeed it seems the following is missing:

lemma id_prod : (λ (p : α × α), (p.1, p.2)) = id :=
by ext ; simp

attribute [extensionality] uniform_space_eq

lemma uniform_space_comap_id {α : Type*} : uniform_space.comap (id : α  α) = id :=
begin
  ext u,
  dsimp [uniform_space.comap],
  rw [id_prod, filter.comap_id]
end

The first one is strange, but I couldn't find it @Johannes Hölzl any thought?

Patrick Massot (Sep 20 2018 at 07:22):

Should we add this to mathlib? make the first one a simp lemma?

Johannes Hölzl (Sep 20 2018 at 07:22):

you mean id_prod? I don't think we have it yet

Patrick Massot (Sep 20 2018 at 07:22):

Yes, id_prod

Kevin Buzzard (Sep 20 2018 at 07:22):

I feel like a child collecting football cards again

Kevin Buzzard (Sep 20 2018 at 07:22):

great excitement when we discover a new basic lemma we don't have

Patrick Massot (Sep 20 2018 at 07:23):

simp or not simp?

Johannes Hölzl (Sep 20 2018 at 07:23):

I guess we will never run out of basic lemmas

Johannes Hölzl (Sep 20 2018 at 07:23):

currently I'm in favor of not simp

Kevin Buzzard (Sep 20 2018 at 07:23):

I ran out of football cards once; I remember the joy of getting the last one. Bryan Flynn, Leeds United.

Johannes Hölzl (Sep 20 2018 at 07:24):

I don't think we have a lot of eta-rule like these in the simp-set. And it might get confusing. But then this rule is quiet nice...

Kevin Buzzard (Sep 20 2018 at 07:24):

But I thought we would ultimately find that every basic lemma is either easy or has a tactic-free and simple proof

Patrick Massot (Sep 20 2018 at 07:24):

What about tagging uniform_space_eq?

Johannes Hölzl (Sep 20 2018 at 07:27):

yes, uniform_space_eq should be tagged with @[extensionality].

Patrick Massot (Sep 20 2018 at 07:36):

Ok, I first PR'ed id_prod, then I'll do the other two

Johannes Hölzl (Sep 20 2018 at 07:39):

just waiting for Travis

Patrick Massot (Sep 20 2018 at 15:23):

Quick update on this topic: mathlib got https://github.com/leanprover/mathlib/commit/d0f1b21a9df64f48a8d28203bf292eb80e05a6da and https://github.com/leanprover/mathlib/commit/1da8cc51854c2e75f456878b195b162dc8dbb130 then I added https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/homeos.lean to the perfectoid project (I think I still don't whether mathlib wants it). We can then write the two versions of the lemma (following my real life sketch and Kevin's Lean start) as:

open set
variables {α : Type*} {β : Type*} {γ : Type*}

lemma uniform_continuous_id_of_emb' [uniform_space α] [uniform_space β] [uniform_space γ]
  [complete_space β] [separated β] [complete_space γ] [separated γ] (j : homeo β γ)
  {e : α  β} (ue : uniform_embedding e) (dense : x, x  closure (range e))
  (h : uniform_continuous (j  e)) : uniform_continuous j :=
begin
  let e₀ := (ue.dense_embedding dense).extend (j  e),
  have uc_e₀ : uniform_continuous e₀,
  { dsimp [e₀],
    exact uniform_continuous_uniformly_extend ue dense h },
  convert uc_e₀,
  ext b,
  have closed : is_closed {b : β | j b = e₀ b} := (is_closed_eq j.fun_con uc_e₀.continuous),
  have dense' : closure (range e) = univ, by rwa eq_univ_iff_forall,
  apply is_closed_property dense' closed (λ a, eq.symm $ uniformly_extend_of_emb ue dense h)
end

def unif_emb {α : Type*} {β : Type*} (u_α : uniform_space α) (u_β : uniform_space β) (f : α  β) : Prop :=
uniform_embedding f

def unif_cont {α : Type*} {β : Type*} (u_α : uniform_space α) (u_β : uniform_space β) (f : α  β) : Prop :=
uniform_continuous f

def top (u : uniform_space α):= u.to_topological_space

def complete (u : uniform_space α) := complete_space α

def hausdorff (u : uniform_space α) := separated α

lemma uniform_continuous_id_of_emb [ : uniform_space α] (u' u : uniform_space β)
  [cu : complete u] [hu : hausdorff u] [cu' : complete u'] [hu' : hausdorff u'] (htop : top u = top u')
  {e : α  β} (ue : unif_emb  u e) (dense : x, x  closure (range e))
  (h : unif_cont  u' e) :  u'  u :=
begin
  let iduu' : @homeo β β (top u) (top u') :=
  { to_fun := id,
    inv_fun := id,
    left_inv := λ x, rfl,
    right_inv := λ x, rfl,
    fun_con := by rw htop; exact continuous_id,
    inv_con := by rw htop; exact continuous_id },

  rw show e = iduu'  e, by refl at h,
  have H := @uniform_continuous_id_of_emb' α β β  u u' cu hu cu' hu' iduu' e ue dense h,

  rw uniform_continuous_iff at H,
  convert H,
  rw show (iduu' : β  β) = id, by refl,
  simp [uniform_space_comap_id]
end

Patrick Massot (Sep 20 2018 at 15:26):

Of course the first proof has no @, we are not fighting mathlib here. The second one is not too bad in my opinion. The statement is clean, because of the "rebinded" definitions, which cost nothing in the proof.

Patrick Massot (Sep 20 2018 at 15:27):

The main @ thing is the definition of the identity seen as a homeo between different topologies, which costs two slightly awkwards rw show ..., by refl.

Patrick Massot (Sep 20 2018 at 15:28):

What do you guys think about all this?

Mario Carneiro (Sep 20 2018 at 15:29):

I think the identity homeo should be a theorem

Patrick Massot (Sep 20 2018 at 15:30):

Stating what?

Mario Carneiro (Sep 20 2018 at 15:30):

just like the theorem that identity is continuous iff the topologies are le, the identity is a homeo iff the topologies are eq

Patrick Massot (Sep 20 2018 at 15:31):

This bundled definition of a homeo doesn't seem so nice when it comes to stating that some map is a homeo

Mario Carneiro (Sep 20 2018 at 15:31):

this is true. Maybe settle for one direction, the one you proved

Mario Carneiro (Sep 20 2018 at 15:33):

The reverse direction says that if f : homeo A A T1 T2 and f x = x for all x, then T1 = T2

Patrick Massot (Sep 20 2018 at 15:33):

So it would be a def, not a lemma, right?

Mario Carneiro (Sep 20 2018 at 15:33):

yes

Mario Carneiro (Sep 20 2018 at 15:35):

After all this refactoring, I would ask whether you really need uniform_continuous_id_of_emb though

Mario Carneiro (Sep 20 2018 at 15:35):

we treated it as the endgame but maybe you can avoid le on uniformities to begin with

Kevin Buzzard (Sep 20 2018 at 15:36):

I was wondering the same

Patrick Massot (Sep 20 2018 at 15:36):

Of course this is also a legitimate question. But this thread is also used as an exercise in type class hell survival.

Kevin Buzzard (Sep 20 2018 at 15:37):

Patrick's original question was whether the completion of a top group "equalled" (in a mathematician-like way) the completion of the underlying uniform space. But these two completions are just two different types so you could instead ask if they are uniform-equiv, not that this exists.

Kevin Buzzard (Sep 20 2018 at 15:38):

On the other hand Johannes, if I recall correctly, put a bunch of stuff in topological_space.lean about different topologies on the same space...

Patrick Massot (Sep 20 2018 at 15:38):

What do you mean "different types"?

Kevin Buzzard (Sep 20 2018 at 15:39):

Isn't there one "complete-a-group" function which completes a group and spits out one type, and one "complete-a-uniform-space" function which completes a uniform space and spits out a second type? And we think of them as "equal" but they're two different types. That's all I mean, and you know all this already.

Kevin Buzzard (Sep 20 2018 at 15:40):

I was wondering if you ever needed to compare two uniformities on the same type, but I don't know the full story

Patrick Massot (Sep 20 2018 at 15:40):

No, there is a complete a uniform space structure, an instance saying that the result has a uniform structure, and there are instances saying that abelian top groups are uniform spaces, and that the completion of a group is a top group

Patrick Massot (Sep 20 2018 at 15:41):

The full story is still at https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/group_completion.lean#L124

Patrick Massot (Sep 20 2018 at 15:41):

and https://github.com/kbuzzard/lean-perfectoid-spaces/blob/master/src/for_mathlib/group_completion.lean#L118 of course (maybe with tiny differences)

Patrick Massot (Sep 20 2018 at 15:42):

So we really have two uniform space structures on the same type. But of course I wonder whether I could cook up more functions to hide things to the type class system

Kevin Buzzard (Sep 20 2018 at 15:46):

So should that line 124 even make sense?

Kevin Buzzard (Sep 20 2018 at 15:46):

That's what I'm thinking

Kevin Buzzard (Sep 20 2018 at 15:46):

Given some top group H

Kevin Buzzard (Sep 20 2018 at 15:47):

there is an associated uniform space which is also H

Kevin Buzzard (Sep 20 2018 at 15:47):

but then isn't there topological_add_group.completion H (one type) and uniform_space.completion H (a different type)?

Kevin Buzzard (Sep 20 2018 at 15:48):

And then maybe you prove a theorem saying that two uniform structures are the same

Mario Carneiro (Sep 20 2018 at 15:49):

I guess there is a single (uniform) completion operation which additionally has the property that it lifts topological group structure

Kevin Buzzard (Sep 20 2018 at 15:49):

right, but should it be like that?

Kevin Buzzard (Sep 20 2018 at 15:49):

should the theorem be that there's a uniform space equiv?

Mario Carneiro (Sep 20 2018 at 15:49):

Obviously topological_group should have a uniform component so that this can be by defeq

Kevin Buzzard (Sep 20 2018 at 15:50):

Obviously topological_group should have a uniform component

This is when it gets silly.

Patrick Massot (Sep 20 2018 at 15:50):

The theorem that is sorried there has mathematical content, it won't become trivial

Kevin Buzzard (Sep 20 2018 at 15:50):

right

Patrick Massot (Sep 20 2018 at 15:50):

So I don't know what Mario wants to see defeq

Mario Carneiro (Sep 20 2018 at 15:50):

of course, the content is shifted to the definition of the topological group

Kevin Buzzard (Sep 20 2018 at 15:51):

Is there no way of making all this sensible?

Mario Carneiro (Sep 20 2018 at 15:51):

There are zero cases where you want a topological group with a uniform structure that doesn't agree with it

Kevin Buzzard (Sep 20 2018 at 15:51):

It's like the product of metric spaces example, but it's even better, because we don't even have to take a product.

Patrick Massot (Sep 20 2018 at 15:51):

Except for non-commutative groups where there are two choices

Kevin Buzzard (Sep 20 2018 at 15:51):

rofl

Patrick Massot (Sep 20 2018 at 15:52):

Left uniformity and right uniformity

Kevin Buzzard (Sep 20 2018 at 15:52):

two different uniformities giving the same topology, right?

Patrick Massot (Sep 20 2018 at 15:52):

sure

Kevin Buzzard (Sep 20 2018 at 15:52):

Let's cross that bridge when we come to it

Patrick Massot (Sep 20 2018 at 15:52):

I assumed everything was commutative because I aimed for addition in rings

Patrick Massot (Sep 20 2018 at 15:52):

and it was complicated enough

Kevin Buzzard (Sep 20 2018 at 15:53):

I want to end up in a situation where there are no diamonds. Is this possible?

Mario Carneiro (Sep 20 2018 at 15:53):

yes

Kevin Buzzard (Sep 20 2018 at 15:53):

Given a uniform space I want to be able to complete it

Patrick Massot (Sep 20 2018 at 15:53):

I don't mind seeing the uniform structure as part of the abelian top group

Mario Carneiro (Sep 20 2018 at 15:53):

I assume you mean the diamonds commute by defeq

Kevin Buzzard (Sep 20 2018 at 15:53):

yes

Kevin Buzzard (Sep 20 2018 at 15:53):

What I was thinking is that the group completion should have a different name.

Patrick Massot (Sep 20 2018 at 15:53):

But I don't see how this will help when proving the actual theorem, even if this proof is now part of the construction of the top group instance

Kevin Buzzard (Sep 20 2018 at 15:54):

this is not supposed to help proving the theorem

Kevin Buzzard (Sep 20 2018 at 15:54):

yes I was just wondering about how to make the theorem part of the infrastructure. Is this just clear to both of you?

Patrick Massot (Sep 20 2018 at 15:54):

I mean help in the Lean sense, not maths sense

Patrick Massot (Sep 20 2018 at 15:54):

Nothing is clear to me here (except the proof I see on paper in front of me)

Kevin Buzzard (Sep 20 2018 at 15:54):

I want to give the top group completion a different name, make it a different type to the uniform space completion

Kevin Buzzard (Sep 20 2018 at 15:55):

hmm but it still has to be a top group

Mario Carneiro (Sep 20 2018 at 15:55):

It will make that same_uniformity theorem true by defeq, so you won't have to muck about with rewriting instance arguments

Mario Carneiro (Sep 20 2018 at 15:56):

But it's true that the theorem still has to be proved, and it is an equality of uniformities

Kevin Buzzard (Sep 20 2018 at 15:56):

top groups and uniform spaces -- they are going to be classes, right? Let's make that assumption

Mario Carneiro (Sep 20 2018 at 15:56):

yes, are they not already?

Kevin Buzzard (Sep 20 2018 at 15:56):

And there's always going to be an instance from top group to uniform space, right?

Mario Carneiro (Sep 20 2018 at 15:56):

right

Patrick Massot (Sep 20 2018 at 15:56):

but it may be generated by extends

Mario Carneiro (Sep 20 2018 at 15:57):

?

Kevin Buzzard (Sep 20 2018 at 15:57):

and will a top group definitely have a uniformity component?

Kevin Buzzard (Sep 20 2018 at 15:57):

so the instance is a forgetful functor?

Patrick Massot (Sep 20 2018 at 15:57):

If class top_group extends uniform_space

Mario Carneiro (Sep 20 2018 at 15:57):

right

Kevin Buzzard (Sep 20 2018 at 15:57):

But with the completion construction

Kevin Buzzard (Sep 20 2018 at 15:57):

you can insert the theorem into the construction, can you not?

Mario Carneiro (Sep 20 2018 at 15:57):

yes, that's the idea

Kevin Buzzard (Sep 20 2018 at 15:57):

right

Kevin Buzzard (Sep 20 2018 at 15:59):

so the top group completion must have the "uniform space generated by the top group structure" uniform space

Patrick Massot (Sep 20 2018 at 15:59):

So the gain would be when I wanted to use the same_uniformity theorem, in https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/group_completion.lean#L161 not when I want to prove it

Mario Carneiro (Sep 20 2018 at 16:00):

yes

Patrick Massot (Sep 20 2018 at 16:00):

sounds very good

Kevin Buzzard (Sep 20 2018 at 16:00):

I think I'm there

Patrick Massot (Sep 20 2018 at 16:01):

Kevin, do you want to know why we need this theorem? It's easy to explain

Patrick Massot (Sep 20 2018 at 16:01):

Mario, the trouble is I tried to do this "top_group extends uniform space" trick after the Orsay meeting but couldn't handle everything that broke when I started

Kevin Buzzard (Sep 20 2018 at 16:03):

I can see for maths reasons why we want to prove the two uniformities are equal.

Kevin Buzzard (Sep 20 2018 at 16:03):

What I was thinking about was how all this could play well with the type class system.

Kevin Buzzard (Sep 20 2018 at 16:03):

That is exactly why I changed your beta,beta to beta,gamma, because then the theorem you were struggling on suddenly seemed much easier

Patrick Massot (Sep 20 2018 at 16:03):

ok, we're on the same page

Kevin Buzzard (Sep 20 2018 at 16:06):

but if topological_group extends uniform_space (I don't know if it does or if it should) then we have to be careful, but it sounds like it's OK. I guess it doesn't matter whether it extends or not -- you probably still want an instance. Eew. Is top group -> uniform space -> top space defeq to top group -> top space?

Patrick Massot (Sep 20 2018 at 16:06):

Yes, I made sure this is true back in June

Kevin Buzzard (Sep 20 2018 at 16:07):

It's ridiculous that this sort of thing is important. I think the system is not quite fit for purpose.

Patrick Massot (Sep 20 2018 at 16:07):

https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/topological_structures.lean#L353

Kevin Buzzard (Sep 20 2018 at 16:07):

I'm with Chris. He had trouble with two instances which were provably equivalent but not defeq. There should be a way to make this work by brandishing a theorem at the type class inference system and saying "use this if stuck"

Patrick Massot (Sep 20 2018 at 16:09):

just like the theorem that identity is continuous iff the topologies are le

Do we actually have this theorem in mathlib? I can't find it

Kevin Buzzard (Sep 20 2018 at 16:09):

It would be wonderful if the default setting was "if it's a class, then you will have one instance and that's the end of it. If there are two instances, then you had better supply the proof that they're the same"

Kevin Buzzard (Sep 20 2018 at 16:09):

and you had to explicitly switch this off.

Patrick Massot (Sep 20 2018 at 16:18):

Let's try to use the existing Lean. @Mario Carneiro what do you suggest I should do? Should I try to refactor everything about commutative additive top groups? Should I start with class topological_abelian_group (α : Type u) extends uniform_space α, add_comm_group α?

Patrick Massot (Sep 20 2018 at 16:18):

and then prove an instance converting this to the existing topological group classes?

Kevin Buzzard (Sep 20 2018 at 16:39):

he'll make you call it topological_add_comm_group

Mario Carneiro (Sep 20 2018 at 16:57):

I'm okay with saying top instead of topological

Mario Carneiro (Sep 20 2018 at 16:58):

exactly because you want to stack adjectives like this

Patrick Massot (Sep 20 2018 at 17:39):

What about my question?

Mario Carneiro (Sep 20 2018 at 17:56):

I hate to answer a question like that with yes, but yes

Mario Carneiro (Sep 20 2018 at 17:57):

then again, I think @Johannes Hölzl had a part in the original formulation so maybe he should say something here

Patrick Massot (Sep 20 2018 at 18:02):

I hate to answer a question like that with yes, but yes

What would you prefer?

Mario Carneiro (Sep 20 2018 at 18:11):

what you said: a class top_add_comm_group that extends uniform_space and add_comm_group

Patrick Massot (Sep 21 2018 at 13:32):

I tried various things today, but clearly I'm not doing it right. Recall I defined the Hausdorff completion functor in https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/master/src/for_mathlib/completion.lean I also defined a uniform structure on commutative topological groups in https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/master/src/for_mathlib/topological_structures.lean#L109, and wanted to get a group completion functor. For this it seems we need closer integration of topological groups and uniform structures. I made a first attempt at https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/e44b49e7bd9f77f59246f725cc38bf879c2af50f/src/for_mathlib/top_groups.lean There I have an axiom relating a uniform structure and a group structure, but the uniform structure is a parameter. There are only two sorries in that file, and the completion stuff is available right from the beginning, seemingly without diamond issue. However I'd like a way to produce a top_add_comm_group from a topological space structure and a group structure, building the uniform space structure automatically using a version of my previous unbundled work. I don't see how to do that. Then I tried https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/master/src/for_mathlib/top_groups.lean where the only parameter of top_add_comm_group is the carrier type. But then I had to setup much more wrapping around my completion stuff, and https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/master/src/for_mathlib/top_groups.lean#L45 completely fails. I really need help from @Johannes Hölzl or @Mario Carneiro in order to now which attempt (if any) goes in the right direction.

Johannes Hölzl (Sep 21 2018 at 17:13):

I'm taking a look at it

Johannes Hölzl (Sep 22 2018 at 10:48):

Do you need topological_add_group in your definition of top_add_comm_group? Shouldn't topological_add_group be derived from unif_group?

Patrick Massot (Sep 22 2018 at 11:44):

You're probably right

Johannes Hölzl (Sep 22 2018 at 11:53):

I forked your repo: https://github.com/johoelzl/lean-perfectoid-spaces

Johannes Hölzl (Sep 22 2018 at 11:54):

So in top_groups you need to prove that the group is a group, and then that the uniformity fits

Johannes Hölzl (Sep 22 2018 at 11:55):

first we need to show that - and + are (uniform) continuous, and reduce to -, + on G under to_completion. Then we can proof the group properties by the embedding along to_completion.

Johannes Hölzl (Sep 22 2018 at 11:56):

is this what you expected or do you want something different?

Patrick Massot (Sep 22 2018 at 12:19):

I want to be able to manipulate topological groups and their completions. The mathematical story is extremely clear, and I already formalized large parts of it, but they don't want to fit together. Have you seen my two recent attempts? There are successive commits. The older attempts are in neighboring files. Would you like me to LaTeX the math story?

Johannes Hölzl (Sep 22 2018 at 12:21):

I think LaTeX is not yet necessary. But what kind of manipulations do you want to make?

Patrick Massot (Sep 22 2018 at 12:24):

The same thing we want from the beginning: a completion functor, left adjoint to the inclusion of complete hausdorff group into all topological groups. That's all!

Patrick Massot (Sep 22 2018 at 12:25):

We do have it for uniform space, in my completion.lean

Johannes Hölzl (Sep 22 2018 at 12:26):

hm, this is a little bit too far for me. but you are currently stuck in proving that the completion of a topological group (with the induced uniformity) is again a group. This is what I see in top_groups. is this correct?

Johannes Hölzl (Sep 22 2018 at 12:27):

or did you just sorry this part, because you wanted to see how this way works for later proofs?

Patrick Massot (Sep 22 2018 at 12:30):

The key fact is we start with a completion which is a universal solution to the problem of factoring maps into complete hausdorff spaces:

When moving to topological groups, we want all those maps to be group morphisms. It looks like extending operation by continuity and running the same abstract non-sense will do it without any work. But when you think about how to prove that completion.map f is a group morphisms you see you need commutation of the two constructions (from top group to uniform space and from uniform space to completion)

Johannes Hölzl (Sep 22 2018 at 12:30):

so what I propose is:

  • we get obviously that group_completion G is a complete, separated uniformity (and everything we know about them). This is a couple of instances.
  • then we proof that it is a group. This requires some work, we need to lift the group operations and show that they are uniform and invariant under coerion

Patrick Massot (Sep 22 2018 at 12:32):

I did all that in my first attempt in https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/topological_structures.lean

Patrick Massot (Sep 22 2018 at 12:33):

But then the last instance fail completely because of the diamond issue, and even sorrying an equality of uniform structures didn't help because I couldn't manage rewriting instances

Patrick Massot (Sep 22 2018 at 12:34):

I'm sorry I need to take care of my family. But in any case I don't think this problem can be solved without investing some time into reading my various attempts

Patrick Massot (Sep 22 2018 at 12:34):

Thank you very much for trying to help me

Kevin Buzzard (Sep 22 2018 at 12:35):

I am of course actively interested in making all this work so let me know if I can help somehow.

Johannes Hölzl (Sep 22 2018 at 18:07):

So it turns out that top_add_comm_group is equivalent to uniform_add_group. From uniform_add_group we can derive uniformity = comap (λx:α×α, x.2 - x.1) (nhds (0:α)).

so the only complicated lift is the group structure itself

Patrick Massot (Sep 24 2018 at 09:27):

@Johannes Hölzl I see you made some progress in your fork. Are you still working on this? Or do you think I should try to copy your work and try to proceed?

Johannes Hölzl (Sep 24 2018 at 09:28):

I didn't continue on this yet. But I want to continue today

Patrick Massot (Sep 24 2018 at 09:29):

In particular, does it mean you think that the definition of top_add_comm_group is the correct starting point, and wrapping the completion stuff in group_completion is the right thing to do?

Patrick Massot (Sep 24 2018 at 09:30):

Ok, great. I'll wait and see then

Johannes Hölzl (Sep 24 2018 at 09:30):

But I think I will take a look again at your completion branch in leanprover-community.

Johannes Hölzl (Sep 24 2018 at 09:33):

I think top_add_comm_group is not necessary. I think uniform_add_group can also be used instead of it.

Johannes Hölzl (Sep 24 2018 at 09:34):

But if you want you can finish the proofs in top_groups.lean. In the meantime I look at your completion branch and try to bring it up to current mathlib and see how I want to merge it. What do you think about this?

Patrick Massot (Sep 24 2018 at 09:38):

I still don't understand what is uniform_add_group This notion doesn't exist in real world maths, and it seems equivalent to topological groups, at least in the communtative case. What's the point?

Johannes Hölzl (Sep 24 2018 at 09:43):

The difference is just that topological_add_group doesn't know about its uniformity. So I called the type class which requires the uniformity uniform_add_group. We can change topological_add_group to require an uniform space, and change the axiom to assume that - is uniformly continuous.

Johannes Hölzl (Sep 24 2018 at 09:44):

The difference to top_add_comm_group will be that topological_add_group is still unbundled.

Patrick Massot (Sep 24 2018 at 09:46):

I don't understand. What is unbundled?

Johannes Hölzl (Sep 24 2018 at 09:49):

Okay, bundled is not the right word in this context. What I mean is that topological_add_group has the topology and the group structure as parameter. top_add_group has it as the uniformity and its group as fields in its structure.

Patrick Massot (Sep 24 2018 at 10:03):

I'm sorry this conversation is not smoother, but my youngest daughter is sick, and I have to take care of her

Patrick Massot (Sep 24 2018 at 10:05):

The point of the "bundled" version was to try to make sure the work of proving the uniform structure compatibility in group completions would be hidden in the instance building, and would never be an issue afterwards

Patrick Massot (Sep 24 2018 at 10:06):

But of course this version needs a constructor which only takes group law axioms, a topology and a bunch of continuity proofs, in the same way as a metric space can be constructed from a distance without providing a uniformity

Johannes Hölzl (Sep 24 2018 at 10:15):

I will see how much of the actual construction can be hidden. Also, note that I will rebase your completions branch in leanprover-community after lunch. I hope you don't have any local changes

Patrick Massot (Sep 24 2018 at 10:16):

It's a bit of a mess that this work is somewhat split between this mathlib branch and the prefectoid repository, but I think the only substantial difference is the new top_groups.lean in the perfectoid repository, so you can work on the community mathlib branch

Patrick Massot (Sep 24 2018 at 12:08):

I worked a bit, see https://github.com/johoelzl/lean-perfectoid-spaces/compare/master...PatrickMassot:master I unsorried the add_comm_group structure by porting my previous work. Hopefully this could save you some time. This required adding a couple of lemmas first. I tried to follow the mathlib convention in naming group_completion.continuous_add and group_completion.continuous_add' but I noticed you didn't. Also, I shortened the name since it's all in the group_completion namespace, but since the purely topological continuous_add is in root namespace, it's a but of a mess. Hopefully all this will be much simpler in the end

Johannes Hölzl (Sep 24 2018 at 12:18):

Thanks! I'm currently reorganizing uniform_space.lean and move the separated quotient type and Cauchy to completions.lean.

Patrick Massot (Sep 24 2018 at 12:21):

Great!

Patrick Massot (Sep 24 2018 at 12:21):

I'm very excited and grateful to get some help here

Patrick Massot (Sep 24 2018 at 13:02):

Also note that the proofs in https://github.com/johoelzl/lean-perfectoid-spaces/blob/fa721c6aa863c79b22ce463358c2b616c413e38c/src/for_mathlib/top_groups.lean#L194 are not as abstract as we'd like them to be. Ideally they would all follow from things like https://github.com/leanprover-community/mathlib/blob/a5da4d5acccc9910d921cfadb2c8e4cce59e1d80/analysis/topology/completion.lean#L726. So all topological argument would ultimately be in https://github.com/leanprover-community/mathlib/blob/a5da4d5acccc9910d921cfadb2c8e4cce59e1d80/analysis/topology/completion.lean#L552, as they should be. But the trouble is that group axioms in mathlib are stated as equalities between elements, instead of functions. So a lot of packing and unpacking would be required. I hesitated to setup all this, with a new group structure constructor inspired by universal algebra but I preferred to move on.

Johannes Hölzl (Sep 25 2018 at 17:53):

@Patrick Massot I moved now most of the completion stiff to its own lean theory analysis.topology.completion. I added the group completion instances to the completion type itself. I guess this makes sense.
the only thing missing is a nice setup for topological groups, where one only needs to define the zero nighbourhood and get a topological group, or where one proofs that we have a topological group and get the uniformity. This is currently in analysis/topology/topological_groups but needs to be restructured.

Patrick Massot (Sep 25 2018 at 19:05):

Thanks @Johannes Hölzl It all looks nice, except that I still don't know what we are talking about. What is this theory of uniform_add_group? Is this meant to be only an intermediate definition? Is the missing piece the piece were you make connection with topological groups as they are defined in math books?

Patrick Massot (Sep 25 2018 at 19:10):

Also, I'm confused about when the diamond problem will return to hit us. The fact that the group uniform structure on the completion of a group is the completion of the group uniform structure is a non-empty mathematical content. In my approach it seemed necessary in order to get a functorial group completion. Where will this be needed in your way of building the theory?

Johannes Hölzl (Sep 25 2018 at 19:12):

uniform_add_group is a technical device. I don't want to force each appearance of a topological group to be a uniform space. That's why it is split into a topological_add_group (topology + group) and uniform_add_group (uniformity + group). We know also that we can derive a canonical uniform space for a topological group, but this is not setup as a type class instance.

Johannes Hölzl (Sep 25 2018 at 19:13):

What is exactly the diamond? We have add_group (completion A) and uniform_space (completion A). Both have currently only one way to construct them. What are the alternatives?

Patrick Massot (Sep 25 2018 at 19:14):

topological_add_group.to_uniform_space (completion A) = completion (topological_add_group.to_uniform_space A)

Patrick Massot (Sep 25 2018 at 19:14):

That's a non-empty mathematical result

Johannes Hölzl (Sep 25 2018 at 19:15):

but topological_add_group.to_uniform_space is currently not in our type class hierarchy

Patrick Massot (Sep 25 2018 at 19:16):

I don't understand why this theorem can be avoided while constructing the completion functor for commutative topological groups

Patrick Massot (Sep 25 2018 at 19:16):

It's independent of the discussion of have instances or def

Johannes Hölzl (Sep 25 2018 at 19:21):

With uniformity_eq_comap_nhds_zero (https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/topological_structures.lean#L276) it should be easy to prove this. In the one direction this is how we define the uniformity, in the other direction we have a uniform_add_group and can use uniformity_eq_comap_nhds_zero.

But maybe I misunderstand the problem. I will try to prove this diamond tomorrow.

Patrick Massot (Sep 25 2018 at 19:25):

Ok, thank you very much. I would really love to see the finished thing (including the link with topological groups). I hope I'll be able to learn something from this, since I spend quite a lot of time thinking about more naive (ie. straight from maths books) approaches

Patrick Massot (Sep 25 2018 at 20:24):

Indeed uniformity_eq_comap_nhds_zero looks like a characterization of the uniform structure that could be very important. The first step of the proof looks like it has nothing to do with groups:

lemma johannes_lemma {α : Type*} [uniform_space α] :  {s : set (α×α)} {f : α  α  α},
  uniform_continuous (λp:α×α, f p.1 p.2)  s  (@uniformity α _).sets 
   u  (@uniformity α _).sets, a b c, (a, b)  u  (f a c, f b c)  s :=
begin
  assume s f hf hs,
  rw [uniform_continuous, uniformity_prod_eq_prod, tendsto_map'_iff, ()] at hf,
  rcases mem_map_sets_iff.1 (hf hs) with t, ht, hts, clear hf,
  rcases mem_prod_iff.1 ht with u, hu, v, hv, huvt, clear ht,
  refine u, hu, assume a b c hab, hts $ (mem_image _ _ _).2 ⟨⟨⟨a, b, c, c⟩⟩, huvt ⟨_, _⟩, _⟩⟩,
  exact hab,
  exact refl_mem_uniformity hv,
  refl
end

I don't know what would be a better mathlib name.

Patrick Massot (Sep 25 2018 at 20:28):

Better statement:

lemma johannes_lemma {α : Type*} [uniform_space α] {β : Type*} [uniform_space β]
:  {s : set (β × β)} {f : α  α  β},
  uniform_continuous (λ p : α × α, f p.1 p.2)  s  (@uniformity β _).sets 
   u  (@uniformity α _).sets, a b c, (a, b)  u  (f a c, f b c)  s :=

Patrick Massot (Sep 25 2018 at 20:29):

And I don't change any character from the proof! I love that. Usually when we wrote in real world math: "the same proof shows that..." it's a polite lie

Patrick Massot (Sep 25 2018 at 20:32):

Of course we can also write this as:

lemma johannes_lemma {α : Type*} [uniform_space α] {β : Type*} [uniform_space β] {f : α  α  β}
: uniform_continuous (λ p : α × α, f p.1 p.2)   {s : set (β × β)}, s  (@uniformity β _).sets 
   u  (@uniformity α _).sets, a b c, (a, b)  u  (f a c, f b c)  s

Isn't it an iff then?

Reid Barton (Sep 25 2018 at 20:33):

I'm trying to process the "better statement". Is it essentially saying that if f:A×ABf : A \times A \to B is uniformly continuous, then so is f(,c):ABf(-, c) : A \to B for any cAc \in A?

Patrick Massot (Sep 25 2018 at 20:34):

I'm also trying to process it

Patrick Massot (Sep 25 2018 at 20:34):

But I don't think it means what you wrote

Patrick Massot (Sep 25 2018 at 20:35):

but you may be right

Reid Barton (Sep 25 2018 at 20:35):

Oh no I am not right.

Reid Barton (Sep 25 2018 at 20:35):

I see. I had the quantifier involving cc in the wrong place.

Patrick Massot (Sep 25 2018 at 20:36):

Yeah, it's a tricky statement

Patrick Massot (Sep 25 2018 at 20:37):

Still there is an asymmetry between the two A factors, so it's probably not an iff

Patrick Massot (Sep 25 2018 at 20:50):

Anyway, this lemma, in its latest version allows to reduce the crucial proof to:

lemma uniformity_eq_comap_nhds_zero : uniformity = comap (λx:α×α, x.2 - x.1) (nhds (0:α)) :=
begin
  rw [nhds_eq_comap_uniformity, filter.comap_comap_comp],
  refine le_antisymm (filter.map_le_iff_le_comap.1 _) _ ; intros s hs,
  { rcases johannes_lemma uniform_continuous_sub' hs with t, ht, hts,
    refine mem_map.2 (mem_sets_of_superset ht _),
    rintros a, b,
    simpa [subset_def] using hts a b a },
  { rcases johannes_lemma uniform_continuous_add' hs with t, ht, hts,
    refine ⟨_, ht, _⟩,
    rintros a, b, simpa [subset_def] using hts 0 (b - a) a }
end

Patrick Massot (Sep 25 2018 at 20:51):

And I still don't understand the magic trick that seems to have removed the diamond issue (I mean removed from the maths discussion, I'm not even talking about Lean). I guess I'll see it when everything will be in place.

Patrick Massot (Sep 25 2018 at 20:53):

I also don't understand at all https://github.com/leanprover-community/mathlib/commit/85b19e23d45f14a210d0b7491c66477d0c560c9a Why did you remove all this? It contains a lot of maths that don't appear anywhere else

Johannes Hölzl (Sep 26 2018 at 07:41):

Urgs, I removed the wrong file.

Patrick Massot (Sep 26 2018 at 19:39):

@Johannes Hölzl Did you try to go from topological_add_group to the completion and still get everything?

Mario Carneiro (Sep 26 2018 at 19:41):

(deleted)

Reid Barton (Sep 26 2018 at 19:43):

Mario did you just respond to a question asked on the wrong topic with an answer posted on the wrong stream

Mario Carneiro (Sep 26 2018 at 19:44):

yes. yes I did.

Patrick Massot (Sep 26 2018 at 19:44):

This topic was only distantly related to separation stuff anyway

Patrick Massot (Sep 26 2018 at 19:44):

Somehow, deep down, I guess we miss Gitter's mess

Patrick Massot (Sep 26 2018 at 19:52):

The stuff about group topologies generated from a neighborhood filter around zero will probably be very convenient for the perfectoid project, which uses adic topology

Johannes Hölzl (Sep 26 2018 at 20:00):

I didn't work yet on the diamond, I got side tracked by the topological space construction

Patrick Massot (Sep 26 2018 at 20:01):

Ok, I understand.

Johannes Hölzl (Sep 27 2018 at 08:58):

I added now topological_add_comm_group.to_uniform_space_eq. It doesn't look to be directly a diamond. The reason is the following:
For completion α to be a group, we already need to know that α has a uniform space, and that the group structure is compatible with this uniformity (i.e. uniform_add_group).

A diamond would mean we have group_to_uniform ∘ completion = completion ∘group_to_uniform. But completion doesn't work on groups without the uniformity. So we actually have group_to_uniform ∘ completion ∘group_to_uniform = completion ∘group_to_uniform. Now it is enough to prove group_to_uniform ∘ G = G, where G is already a group with compatible uniformity.


Last updated: Dec 20 2023 at 11:08 UTC