H-spaces

Stream: LftCM22

[Filippo A. E. Nuccio]

@Flo I see and I am happy to see that H-spaces seem interesting. How do you want to proceed? We can
1) have a Zoom call
2) I can show you some skeleton of what I would start doing
3) You can start on your own (I suggest picking up the references I provided in Serre's paper-I have the pdf) and write me if you need help.

[Flo]

Hi @Filippo A. E. Nuccio , thanks for having me on the project! Could I get a copy of what you wrote in the pdf? I can probably find Serre's paper, but it you have the pdf, it helps if you send it to me.

Once I have seen again what you want to prove, I will first see if I have any math questions, and then we can meet on Zoom to see how this is going to work (please remember than I am relatively new to Lean!).

Would that work for you and other potential participants in this project?

[Flo]

Oh! it's OK, I kept the link to the pdf file with the projects from heather's talk :)

[Filippo A. E. Nuccio]

And here is Serre's paper: Serre-Homologie-singulière-des-espaces-fibrés.pdf

[Filippo A. E. Nuccio]

Please do not hesitate to contact me: for the time being, you are alone on the project, so we are free.

[Filippo A. E. Nuccio]

How is it going?

[Flo]

Hi @Filippo A. E. Nuccio . So, here is a first take at what I believe the definition of an H-space should look like in Lean.

Mathematically, an H-space is a triple (G,m,e) where G is a topological space m: G \times G \to G is a continuous map such that :
(i) m(e,e) = e.
(ii) the continuous maps m(e,.): G \to G and m(.,e): G \to G are homotopic to id_G.

This is Wikipedia's definition: https://en.wikipedia.org/wiki/H-space. It does not seem equivalent to Serre's definition on Page 474 of his paper (Serre says m is given and then there exists e such that etc).

Let us ignore this issue, as well as the second condition in the definition, for now. Then, based on the analogy with (Lean's definition of a topological group), the definition of an H-space should probably start like this:

structure H-space (G : Type u_1) [topological_space G]
Type u_1
(m : G → G → G) --if I understand correctly, this is a map from G \times G to G in Lean
-- here, I am not sure whether Lean already knows that m is continuous (I guess not)
(e : G)
(m_e_e : m(e,e) = e)

I do not feel confident enough to try that in Lean right now, but it should get us closer to having the definition that we are after.

I think that you said that, after the definition is implemented, the first thing to prove is that topological groups are H-spaces, which sounds great to me.

Perhaps we can meet and try it together at some point? We just need to take into account the different time zones:-) Perhaps we can exchange DMs at the conference tomorrow. Thanks!

[Filippo A. E. Nuccio]

OK, this is the way I am implementing this and what you suggest seems very good indeed. I am happy to chat tomorrow, are you in France right now? When would be a convenient time for you to discuss?

[Flo]

Yes, I am in France right now! Perhaps we can chat during the first coffee break? I am also free an hour before the first talk, but then it is early for you.

[Filippo A. E. Nuccio]

Well, let's see (jet-lag is not really helping...): before the first talk might be possible, otherwise at any rate the second part of the morning is dedicated to checking the projects, so it will be the perfect time.

[Flo]

After the last talk is also fine for me (for about 30-45min)

[Flo]

Filippo A. E. Nuccio said:

Well, let's see (jet-lag is not really helping...): before the first talk might be possible, otherwise at any rate the second part of the morning is dedicated to checking the projects, so it will be the perfect time.

Oh! Great, we can take advantage of that time :-)

[Flo]

In fact, it is probably the best option, isn't it? We start talking during the coffee break, and go into more details during the second session of the morning.

Would that work for you?

[Filippo A. E. Nuccio]

Sure!

[Flo (Florent Schaffhauser)]

Hi @Filippo A. E. Nuccio , are you around? Shall we talk on Zoom?

[Filippo A. E. Nuccio]

Yes, I am around! If you give me 10 minutes, I will find a room and set-up a Zoom call: I will post here the details of the call. Sounds good?

[Flo (Florent Schaffhauser)]

Perfect, thanks!

[Flo (Florent Schaffhauser)]

Note: the next type will appear in the definition of an H-space, one way or another.

structure continuous_map.homotopy {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (f₀ f₁ : C(X, Y)) :
Type (max u v)
to_continuous_map : C(↥unit_interval × X, Y)
map_zero_left' : ∀ (x : X), self.to_continuous_map.to_fun (0, x) = ⇑f₀ x
map_one_left' : ∀ (x : X), self.to_continuous_map.to_fun (1, x) = ⇑f₁ x

continuous_map.homotopy f₀ f₁ is the type of homotopies from f₀ to f₁.

[Filippo A. E. Nuccio]

https://cnrs.zoom.us/j/92506672868?pwd=VWp2Z1p5UFlkMEhXamNOaU9Bak9vdz09

[Filippo A. E. Nuccio]

Everybody interested is free to come!

[Filippo A. E. Nuccio]

class H_space (X : Type u) [topological_space X]  :=
(Hmul : X × X → X)
(e : X)
(cont' : continuous Hmul)
(Hmul_e_e : Hmul (e, e) = e)
(left_Hmul_e : ∀ x : X,
  @continuous_map.homotopy_rel (X) (X) _ _
  ⟨(λ x : X, Hmul (e, x)), (continuous.comp cont' (continuous_const.prod_mk continuous_id'))⟩
  ⟨(λ x : X, Hmul (e, x)), (continuous.comp cont' (continuous_const.prod_mk continuous_id'))⟩
  {e})
(right_Hmul_e : ∀ x : X,
  @continuous_map.homotopy_rel (X) (X) _ _
  ⟨(λ x : X, Hmul (x, e)), (continuous.comp cont'(continuous_id'.prod_mk continuous_const))⟩
  ⟨(λ x : X, Hmul (x, e)), (continuous.comp cont'(continuous_id'.prod_mk continuous_const))⟩
  {e})

[Flo (Florent Schaffhauser)]

test

[Ángel González Prieto]

Hi Florent! I really enjoyed our meeting today. Can you share the file please, so I can play with it?

[Flo (Florent Schaffhauser)]

Hi @Ángel González Prieto ! Yes, today was a lot of fun for me too! Sure, I'll post the code below.

But actually, I wanted to ask @Filippo A. E. Nuccio to create a repository on which we can all work (although I'm not yet sure how this works in practice), so that we can make progress on the file and continue working on this after this week. Also, is anybody else is interested in joining us, they could just go to the repository, right?

import topology.homotopy.path

noncomputable theory

class H_space (G : Type*) [topological_space G] :=
--(m : G → G → G)
(m : G × G → G)
(e : G)
--(m_e_e : m e e = e)
(m_e_e : m(e,e) = e)
-- m is continuous
(cont_m : continuous m) -- this is a term of type continuous m
(m_e_dot_homotopic_to_id : ∀ g : G,
  continuous_map.homotopy_rel
  ⟨(λ g : G, m (e, g)), (continuous.comp cont_m (continuous.prod_mk continuous_const continuous_id'))⟩
  --⟨(λ g : G, g), continuous_id'⟩
  ⟨id, continuous_id'⟩
  {e})
(m_dot_e_homotopic_to_id : ∀ g : G,
  continuous_map.homotopy_rel
  ⟨(λ g : G, m(g, e)), (continuous.comp cont_m (continuous.prod_mk continuous_id' continuous_const))⟩
  ⟨id, continuous_id'⟩
  {e})

lemma top_group_is_H_space (G : Type*) [topological_space G] [group G][topological_group G] : H_space G :=
begin
fconstructor,
{ exact (has_mul G).mul,

}
end

--#check H_space.mk

[Filippo A. E. Nuccio]

Hi @Flo (Florent Schaffhauser) Sure, the repository is already there, and I will soon grant both of you access to it. I am just a bit busy now, but I will do this later this afternoon.

[Filippo A. E. Nuccio]

Can you give me your github name?

[Flo (Florent Schaffhauser)]

Filippo A. E. Nuccio said:

Can you give me your github name?

matematiflo

[Filippo A. E. Nuccio]

@Flo (Florent Schaffhauser) @Ángel González Prieto : You should ask the maintainers for an access to the mathlib repository, the project is a branch there.

[Filippo A. E. Nuccio]

@Flo (Florent Schaffhauser) Well, rather than forking you can simply obtain mathlib (via leanproject get mathlib) and then checkout to the branch

[Filippo A. E. Nuccio]

The branch name is fae_fundamental_group_lftcm22

[Filippo A. E. Nuccio]

I am working on this right now and the code is very messy.

[Filippo A. E. Nuccio]

At any rate, I have integrated what we did this morning.'

[Flo (Florent Schaffhauser)]

OK, I am more or less following (I don't know what checkout means or does). Maybe I wait until our next reunion and we do it all together?

[Filippo A. E. Nuccio]

Sure; at any rate, checkout is a basic git command that allows you to switch branch. Its usage is

git checkout fae_fundamental_group_lftcm22

to access the required branch, but if you have never used git we can discuss this live, it will be easier.

[Flo (Florent Schaffhauser)]

I still have not figured out how to use the multiplication from the group G to prove that G has a map m of the type that we need to prove that it is an H-space.

[Filippo A. E. Nuccio]

Try with function.uncurry has_mul.mul: does it work?

[Flo (Florent Schaffhauser)]

Combining it with the exact tactic, yes, it works! Thanks :-)

[Filippo A. E. Nuccio]

Oh, sorry, I was in term mode (exact is not needed there)

[Flo (Florent Schaffhauser)]

Then I did this and it closed the second goal:

{
 exact has_one.one,
}

[Flo (Florent Schaffhauser)]

Anyway, I'm done for the day. Hope we can resume our discussion tomorrow! Also with @Ángel González Prieto

[Ángel González Prieto]

Hi Florent! I've been talking to Filippo. Do you want to connect in 3 minutes to talk about this stuff? I think Filippo has to work on a different project now, but we can discuss these things.

[Flo (Florent Schaffhauser)]

Yes, perfect! I will send you the Zoom address as a private message.

[Ángel González Prieto]

Cool!!! I'm ready now

[Flo (Florent Schaffhauser)]

Me too! I sent you the address as a PM.

[Ángel González Prieto]

Hi Filippo! We're having a situation with the git branch. I can access it and your code, but for some reason, the kernel is not able to finish the computation and the computation doesn't finish. I think you had a similar problem yesterday. Do you know what is going on?

[Ángel González Prieto]

Hi guys! I think I managed to prove that a topological space is a H-space. I posted the proof at git. Not a very important advance, but I think I'm getting clearer ideas now!

[Filippo A. E. Nuccio]

I hope you proved that a top group is a H-space....doing it for every topologicl space seems too much, no? :grinning:

[Filippo A. E. Nuccio]

Thank you, at any rate, I will have a look and we can discuss this the next time!

[Ángel González Prieto]

Oh! Sure! Top. groups, obviously!