basics on homotopy cofibers

[Alizter]

Here is a start on homotopy cofibers. I have more work waiting, but it will be some time before I can clean it up.

@jdchristensen feel free to push any changes as you see fit here. There will probably be some name/style differences with whatever you have.

This builds on

• add functoriality lemmas for pushout #2163

[jdchristensen]

My work is in the attached file, and isn't polished. Maybe you can merge the two together?

Cofiber.txt

[Alizter]

@jdchristensen Do you want me to take a stab at applying Blakers-Massey to get that connectivity result?

[jdchristensen]

@jdchristensen Do you want me to take a stab at applying Blakers-Massey to get that connectivity result?

Sure, that would be great!

[Alizter]

I derived the 8.10.2 HoTT Book Blakers-Massey from the one we had. I'm not yet certain this is enough for the cofiber result, but this is probably something we should cleanup and open a PR for.

[jdchristensen]

I haven't looked at the proof of this carefully, but I suspect that parts of it should be separate lemmas.

[jdchristensen]

I still haven't looked at it carefully, but I'm surprised that it's so long. It should mostly be fairly formal. I'll make a couple of comments for now, but will think more about it later.

[jdchristensen]

Here's an idea that might work. Suppose we have f : X -> Y, g : X -> Z and an equivalence e : X' <~> X. Then you can take a pushout involving X or a pushout involving X'. Then take the corresponding pullbacks P and P', and you get two comparison maps, X -> P and X' -> P'. The claim is that if the first is k-connected, then so is the second. Since this is phrased as a general statement, you should be able to prove it using equivalence induction, i.e. by assuming that e is the identity equivalence, in which case I think it is trivial. (It also shouldn't be too hard to prove this by showing that a square involving X' -> X -> P and X' -> P' -> P commutes.)

Then you apply this to the case where one of them is X and the other is the double-sigma type of Q, and the result you want should follow. (You'd still need to factor out the lemma I suggested in a different comment that says that for the SPushout, the iterated sigma of the spglue map is appropriately connected.)

[jdchristensen]

The idea in the previous comment might work, and might save us the one homotopy in the current proof, but that homotopy is pretty straightforward, so I think it's ok to leave it like it is and not try this idea.

[Alizter]

I've done the review suggestions and factored out some parts of the Blakers-Massey proof. It's possible there are more lemmas to factor out. I added comments explaining what is going on in the proof.

[Alizter]

I managed to prove the connectivity of cofibers using the same argument as the one for suspensions. It didn't use Blakers-Massey and generalised pretty nicely. I'm not sure what we should do with the BM stuff, I struggled to apply it in this case anyway.

[Alizter]

Oh nevermind about my comment about BM I just realised you wanted that to be applied to something else. I'll have a go at that now.

  (** Blakers-Massey implies that the comparison map is highly connected. *)
  Definition isconnected_fiber_to_cofiber (n m : trunc_index)
    {ac : IsConnected n.+1 A} {fc : IsConnMap m.+1 f} (b : B)
    : IsConnMap (m +2+ n) (@fiber_to_cofiber b).
  (** TODO: is m +2+ n correct? *)
  Admitted.

[jdchristensen]

I still haven't looked at it carefully, but I'm surprised that it's so long. It should mostly be fairly formal. I'll make a couple of comments for now, but will think more about it later.

[Alizter]

I pushed a commit simplifying the proof of Freudenthal. There is no more hard-to-understand SPushout wrangling. It is now more obviously a direct corollary.

[Alizter]

I pushed another that uses make_equiv but I'm not sure if that is worth it here.

[Alizter]

I am having trouble with universe variables and I don't have too much time to debug. Most likely a per-version change is required. I managed to prove the connectedness of the comparison map, which is essentially inbetween BM and Freudenthal.

[jdchristensen]

I am having trouble with universe variables and I don't have too much time to debug. Most likely a per-version change is required.

Since the Freudenthal result is down to ~6-8 universe variables, maybe the best thing to do is to improve the real proof rather than using a wrapper? Even if we left it with 6-8 universe variables for now, that would be fine, but it might also be possible to reduce that a bit with a few easy annotations.

I haven't looked at the recent commits yet, as I'm just starting a trip, but I like that the pushout version of Blakers-Massey turned out to be useful to simplify Freudenthal.

[jdchristensen]

I was able to directly get it down to two universe variables, but I think there are still some improvements that can be made, which I'll leave as comments.

[jdchristensen]

This works, but maybe it's also easy to reduce the universe variables needed by blakers_massey_po? (Not worth spending much time on if it isn't trivial.)

[jdchristensen]

Well, it still doesn't work with all versions, so maybe blakers_massey_po requires different numbers of universe variables with different versions? Sorry, no more time to think about this.

[Alizter]

That's a bit annoying. I haven't been able to test this myself locally since Coq 9.0 broke the master setup I had with nix, but I don't have the time to go and fix that now. I say we ignore this for now and fix it before we undraft.

[Alizter]

@jdchristensen Thanks for writing down the unit lemmas for pullbacks. Anything else about cofibers that comes to mind that you would like to see included here?

I tried to write down the equivalence between the cofiber of the suspension functor and the suspension of the cofiber but it got a bit involved. Doing it directly wasn't easy and it might be possible to do it via yoneda but the proof is getting long. I suspect it is going to be a little shorter than the trijoin proof. It is also a direct application of the 3x3 lemma for pushouts with 7 units and f coming out from the center. Interested to know if you have any ideas how to tackle this, but perhaps its best left for a later time.

[jdchristensen]

Anything else about cofibers that comes to mind that you would like to see included here?

Nothing leaps to mind right now.

I tried to write down the equivalence between the cofiber of the suspension functor and the suspension of the cofiber but it got a bit involved. [...] Interested to know if you have any ideas how to tackle this, but perhaps its best left for a later time.

I haven't thought about it and don't have any good ideas. As you suggest, it should follow from Yoneda and the dual fact about fibre sequences. But maybe the best approach long term is to get the 3x3 lemma done. (But of course not in this PR.)

I think this PR could be merged now. About the universe variables, I think the simplest is to just remove the annotations from the current version, and let Coq generate however many universes it wants. It won't be too large, since Blakers-Massey just needs around 9. Then, when we are at a point where the Coq versions we support behave the same way, we could look into simplifying the universe variables in Blakers-Massey.

[Alizter]

I've removed the universe annotations from Freudenthal.v. Should we just merge this with BlakersMassey.v at this point?

[jdchristensen]

Should we just merge this with BlakersMassey.v at this point?

Good point. Yes, that makes sense to me.