continuity of continuous composition

Stream: Is there code for X?

[Roberto Alvarez]

Hi everyone,

I'm trying to write a term like

example C( C(X,Y) , C( C(Y,Z),  C(X, Z))) := ⟨λ f g,  g.comp f, by sorry⟩

How do I show the continuity of continuous_map.comp?

[Kevin Buzzard]

What's the topology on C(X,Y)? Is it the compact open topology? Do you know the maths proof of what you want?

[Eric Wieser]

docs#continuous_map.continuous_comp, maybe? I think that only helps with continuity in one argument though.

[Junyan Xu]

I suggested using the compact-open topology to define the group structure on homotopy groups, but I thought docs#homeomorph.curry would be enough (not even the homeomorphism, just the equiv). I'm surprised to learn docs#continuous_map.continuous_comp holds unconditionally!

[Eric Wieser]

Note that as written I don't think ⟨λ f g, g.comp f, by sorry⟩ is even correctly typed, it needs to be more like ⟨λ f, ⟨λ g, g.comp f, sorry⟩, sorry⟩ as you have two continuity obligations

[Roberto Alvarez]

What's the topology on C(X,Y)?

It is indeed the compact open topology,

[Roberto Alvarez]

I don't think ⟨λ f g, g.comp f, by sorry⟩ is even correctly typed

You're correct, what I actually need is like docs#continuous_map.continuous_comp but for each argument
I might be able to write the other proof from the source.

[Oliver Nash]

Looking quickly, it looks like you've identified a small gap in the library. For the sake of giving a MWE, I'll post:

import topology.compact_open

variables (X Y Z : Type*) [topological_space X] [topological_space Y] [topological_space Z]

example : C(C(X,Y) , C(C(Y,Z),  C(X, Z))) :=
{ to_fun := λ f,
  { to_fun := λ g, g.comp f,
    continuous_to_fun := by
    { -- Functorality of `C(-, Z)`: looks like it's missing.
      sorry, }, },
  continuous_to_fun := sorry, }

[Eric Wieser]

docs#continuous_linear_map.compL looks relevant, but is obviously linear too, which you didn't ask for

[Oliver Nash]

Good point. Mathematically this should be a special case of the gap (maybe modulo linear maps being a closed subset of continuous maps).

[Oliver Nash]

Oh wait, docs#continuous_linear_map.compL is the covariant functor analogous to docs#continuous_map.comp (which we have).

[Roberto Alvarez]

it looks like you've identified a small gap in the library

I have the version of the continuity argument I need now, should this be in the library?

code

section
variables {α : Type*} {β : Type*} {γ : Type*}
variables [topological_space α] [topological_space β] [topological_space γ]
variables (f : C(α, β))

private lemma preimage_gen {s : set α} (hs : is_compact s) {u : set γ} (hu : is_open u) :
  (λ (g : C(β, γ)), g.comp f) ⁻¹' (continuous_map.compact_open.gen s u) =
    continuous_map.compact_open.gen (f '' s) u :=
begin
  ext ⟨g, _⟩, unfold continuous_map.compact_open.gen,
  simp only [set.image_subset_iff, set.preimage_set_of_eq, continuous_map.coe_comp,
    set.mem_set_of_eq, continuous_map.coe_mk],
  rw ← set.preimage_comp,
end

/-- C(-, γ) is a functor. -/
lemma continuous_comp' : continuous (λ g, g.comp f : C(β, γ) → C(α, γ)) :=
continuous_generated_from $ assume m ⟨s, hs, u, hu, hm⟩,
by { rw [hm, preimage_gen f hs hu], exact continuous_map.is_open_gen (hs.image f.2) hu }

end

[Oliver Nash]

Awesome, I'm afraid I have to run to a meeting now but I expect yes: this would be a great addition!

[Oliver Nash]

(Disclaimer: I've only really glanced at this thread.)

[Roberto Alvarez]

I've opened a PR, the proofs need golfing

[Eric Wieser]

Thanks!

[Reid Barton]

Roberto Alvarez said:

Hi everyone,

I'm trying to write a term like

example C( C(X,Y) , C( C(Y,Z),  C(X, Z))) := ⟨λ f g,  g.comp f, by sorry⟩

Is this true in general? I thought you would need at least one of the spaces to be locally compact

[Oliver Nash]

I was wondering the same thing!

[Reid Barton]

oh I guess I was uncurrying it in my head, I don't know about this version.

[Oliver Nash]

Oh I guess it’s easy to see that we don’t need finite-dimensionality in the continuous linear case so presumably we don’t need locally compact in the continuous case.

[Kevin Buzzard]

Oliver Nash said:

I was wondering the same thing!

Yes me too, that was why I explicitly asked the OP if they had a math proof.

[Junyan Xu]

This StackExchange answer shows that there is such a term of type C(C(X,Y) × C(Y,Z), C(X,Z)) assuming just locally_compact_space Y (it's an exercise on Munkres). Once we have this, we also get C(C(X,Y), C(C(Y,Z), C(X,Z))) and C(C(Y,Z), C(C(X,Y), C(X,Z))) unconditionally using docs#continuous_map.curry.

(The answer has a Hausdorff assumption on Y but a comment shows the Hausdorff assumption is unnecessary, if we take "locally compact" to mean that every neighborhood of a point contains a compact neighborhood of the point, as is the case in mathlib. If we take the Wikipedia definition (every point has a compact neighborhood), Wikipedia says we need at least preregularity (weaker than Hausdorff and doesn't seem to exist in mathlib). There is also a more general notion of core-compactness that I can't find in mathlib.)

As for whether C(C(X,Y), C(C(Y,Z), C(X,Z))) and C(C(Y,Z), C(C(X,Y), C(X,Z))) could be constructed under other conditions, I am convinced that C(C(Y,Z), C(C(X,Y), C(X,Z))) can be constructed assuming t2_space X and locally_compact_space X. t2_space is for the following to work: "If X is Hausdorff and S is a subbase for Y (i.e. the topology on Y is generate_from S), then the collection {V(K, U) : U ∈ S, K compact} is a subbase for the compact-open topology on C(X, Y)." (cf. Wikipedia link above) (Update: upon seeing the proof, the mathlib locally_compact_space is also sufficient for this subbase condition to hold.) and locally_compact_space is for the evaluation C(X,Y) × X → Y to be continuous. I am unable to find a weaker or alternative condition for the original question of constructing C(C(X,Y), C(C(Y,Z), C(X,Z))).

[Filippo A. E. Nuccio]

Junyan Xu said:

I suggested using the compact-open topology to define the group structure on homotopy groups, but I thought docs#homeomorph.curry would be enough (not even the homeomorphism, just the equiv). I'm surprised to learn docs#continuous_map.continuous_comp holds unconditionally!

@Junyan Xu Are you making progress in the direction of defining this group structure on the homotopy groups? Because as part of a project for the Lean for Curious Mathematicians, with @Ángel González Prieto and @Flo (Florent Schaffhauser) we are working on something similar, and I would like to avoid overlapping.

[Filippo A. E. Nuccio]

More generally, is there any progress towards constructing this proof? What I have in mind is Bourbaki's Topologie Générale Chap. X, n. 4, Prop 9 saying that given topological spaces $X,Y,Z$ with $Y$ locally compact, the composition map

$$C(X,Y) \times C(Y,Z)\longrightarrow C(X,Z)$$

is continuous. What we have so far in #15068 is continuity in the second variable for a given $f : C(X,Y)$ (and this without the loc. compact assumption on Y).

[Filippo A. E. Nuccio]

I am happy to open a PR if nobody is working on it.

[Junyan Xu]

I only came up with the idea and @Roberto Alvarez is the one who's actually working on it. #14724 was recently merged, giving the underlying type of the homotopy groups but not the group structure. It seems he's making some progress but no PR was opened in the last 20 days.

[Junyan Xu]

In particular, I have not constructed the term of type C(C(X,Y) × C(Y,Z), C(X,Z)) in Lean, but I don't know about @Roberto Alvarez. Do you need it for homotopy groups?

[Filippo A. E. Nuccio]

No, I need it for the proof that the path space is a H-space (so I need multiplication=composition of paths is continuous). I wrote a full proof but have sorried this statement, and now I am wondering what to do.

[Filippo A. E. Nuccio]

Opening a PR with the definition and basic properties of H-spaces might be a first step, and then once we will have the above Bourbaki statement we can add the fact that the path space is an example of an H-space.

[Filippo A. E. Nuccio]

I can also simply prove it myself and then add it to the first PR, I simply wanted to avoid overlapping. I might wait a bit to see if @Roberto Alvarez has news.

[Filippo A. E. Nuccio]

Thanks for the update, at any rate.

[Roberto Alvarez]

Hi!, I have the group instance and I've recently shown commutativity (I haven't PR it because I was working on making the proofs more legible, the proof of commutativity itself is almost 40 loc).
I will open a PR as it is now to make public the intermediate steps I made.

[Roberto Alvarez]

Junyan Xu said:

In particular, I have not constructed the term of type C(C(X,Y) × C(Y,Z), C(X,Z)) in Lean, but I don't know about Roberto Alvarez. Do you need it for homotopy groups?

In addition to the definition here #15068 I also needed some specifics, e.g.

/-- Composition with insert as a continuous map.-/
abbreviation c_comp_insert (i : fin (n+1)) : C( C(I^(n+1),  X ), C( I×I^n,  X)) :=
⟨λ f, f.comp (cube.insert i), (cube.insert i).continuous_comp_left⟩

which might be a corollary.

[Roberto Alvarez]

Filippo A. E. Nuccio said:

More generally, is there any progress towards constructing this proof?

I gave an equivalence to paths for each component so that the group structure is easily shown from what is already defined on transitivity of paths. The additional operation needed to define commutativity is also easy to define, and the proof uses eckmann_hilton.comm_group by which I only need to show distributivity.

[Roberto Alvarez]

The PR with the group and comm_group instances is open: #15681

[Filippo A. E. Nuccio]

Roberto Alvarez said:

Junyan Xu said:

In particular, I have not constructed the term of type C(C(X,Y) × C(Y,Z), C(X,Z)) in Lean, but I don't know about Roberto Alvarez. Do you need it for homotopy groups?

In addition to the definition here #15068 I also needed some specifics, e.g.

/-- Composition with insert as a continuous map.-/
abbreviation c_comp_insert (i : fin (n+1)) : C( C(I^(n+1),  X ), C( I×I^n,  X)) :=
⟨λ f, f.comp (cube.insert i), (cube.insert i).continuous_comp_left⟩

which might be a corollary.

Yes, I agree this might be a corollary. I hope to PR a construction of the term by tonight, and I will update you if this gets merged. Thanks for the update and congratulations for your work!

[Junyan Xu]

Hi @Roberto Alvarez, congratulations and thanks for your amazing work! I have reviewed the code and was able to make some simplifications and golf many proofs in this branch.

The main thing that was unnecessarily complicated is about inserting a coordinate into a point in the n-cube to get a point in the (n+1)-cube, and you need to take care of the order of the inserted coordinate relative to other coordinates. However, this really has nothing to do with the order, and works for arbitrary (possibly infinite) unordered type, and you can simply use {j : fin (n+1) // j ≠ i} instead of fin n as the indexing type, once the definition of cube is generalized to allow an arbitrary type in place of fin n. The insertion-extraction homeomorph is now called merge_split in my code. (To be cleaned up: docstrings that refers to n remain unchanged; some insert/contract lemmas haven't been renamed.)

The second thing is that I defined

def homotopy_group_equiv_fundamental_group (i : N) :
  homotopy_group N x ≃ fundamental_group (gen_loop {j // j ≠ i} x) gen_loop.const

and use it to transfer the group instance from the RHS to the LHS. I'm not sure the definitions concat, reverse etc. are still necessary, as they are almost defeq with the transferred instance:

lemma concat_eq (p q : π_(n+1) x) : concat 0 q p = p * q :=
by { rcases p, rcases q, refl }

The switched order of p and q is due to the definition of docs#category_theory.Aut.group. I have no idea why people decided to insert the flip! In any case our definition should agree with fundamental_group.

[Junyan Xu]

Another to-do is to make an add_comm_group instance on π_(n+2) x; docs#additive should work but it might be possible to avoid it.

[Roberto Alvarez]

Junyan Xu said:

I have reviewed the code and was able to make some simplifications and golf many proofs in this branch.

Excellent! :tada: I'll be merging the changes shortly, thanks a lot!

[Junyan Xu]

@Roberto Alvarez Glad to hear that! I have now supplied the proof that an arbitrary product of compact, locally compact spaces is locally compact. I also added many comments about which file each definition should go into, and I'd appreciate everyone's help to PR those into mathlib.

[Roberto Alvarez]

I've PR'd two of your suggestions; #15707 and #15708

[Filippo A. E. Nuccio]

I've created #15721 with the proof that when $Y$ is locally compact, the composition induces a continuous map $C(X,Y) \times C(Y,Z)\rightarrow C(X,Z)$.

[Filippo A. E. Nuccio]

Thanks to @Junyan Xu for very useful comments and improvements to the PR!

[Filippo A. E. Nuccio]

#16029 contains the definition of H-space and the proof that the path space is an H-space but it is blocked by #15721.