fiber sequences

[RobertHarper]

At the start of section 8.4 we start by considering a fibration E ->> B and "its fiber F", which confused me. Probably the specialist knows what this means, but it is only explained a few paragraphs later as meaning, apparently, the fiber over the base point of B, it being assumed to have one. Perhaps this should be clarified.

[mikeshulman]

Good point, thanks; is this good enough?

[RobertHarper]

Looks good!

[RobertHarper]

I'm still finding the section on fiber sequences to be a bit murky. When speaking of "the fiber of the fiber of f" in Lemma 8.4.4, it seems that we're really depending on two things, that the fiber of f is pointed (by <x0,f0> in the notation of that section), and that the second fiber is of the projection from the fiber of f to X. It feels a bit strange to me to call this the "fiber of the fiber" since the "of" part is a type, not a fibration, but there is an evident fibration involved and an evident induced fiber given by the implied base point. Or else I am just confused, but maybe that's indicative if so. The thrice-iterated fiber would be similarly better explained. Or please correct me!

[mikeshulman]

That's an abuse of language that's very common among homotopy theorists and category theorists, at least: when speaking of things like fibers, cofibers, kernels, and cokernels, which are objects that come equipped with a natural morphism from or to something else, we use the same word for the object and for the object equipped with that canonical morphism. I'm glad you brought it up, because it wouldn't have occurred to me that this wouldn' t be a familiar usage to everyone. Let me try adding a bit more explanation.

[awodey]

keep in mind that as long as the base space is connected, all the fibers are equivalent (via transport) -- so suppressing the dependence on the basepoint is reasonable.

On Jun 12, 2013, at 2:26 PM, Robert Harper notifications@github.com wrote:

I'm still finding the section on fiber sequences to be a bit murky. When speaking of "the fiber of the fiber of f" in Lemma 8.4.4, it seems that we're really depending on two things, that the fiber of f is pointed (by in the notation of that section), and that the second fiber is of the projection from the fiber of f to X. It feels a bit strange to me to call this the "fiber of the fiber" since the "of" part is a type, not a fibration, but there is an evident fibration involved and an evident induced fiber given by the implied base point. Or else I am just confused, but maybe that's indicative if so. The thrice-iterated fiber would be similarly better explained. Or please correct me!

— Reply to this email directly or view it on GitHub.

[mikeshulman]

Although, even if the base space and total space are connected, the fiber may not be, so it matters what basepoint we equip it with.

[RobertHarper]

Not to niggle, but in the proof of Lemma 8.4.4 there is mentioned a map k that we "have", which is not defined, and types F_0 and F', which are not defined up to that point.

[RobertHarper]

I suggest that we merge the sentence after Definition 8.4.5 into the definition itself as follows:

Moreover, if the sets $X_n$ were groups, then we require that the maps be group homomorphisms.

In any case I think it should be "were/be", not "are/are", since the conditional is a counterfactual.

[mikeshulman]

I'm trying to fix this section and it is just a mess. I think the definition of fiber sequence is still not even right: the homotopies have to be based homotopies, otherwise the canonical map from X_{n+1} to the fiber of f_n is not a pointed map. Plus it is really hard to find a good notation for "the basepoint of X_n" given that we usually write x_0 for the basepoint of X. I'm leaning towards not defining a general notion of "a fiber sequence" at all, instead just defining the fiber sequence associated to a based map.

[RobertHarper]

I'm glad you agree, I found this section very hard to follow.

(sent from handheld)

On Jun 12, 2013, at 17:17, Mike Shulman notifications@github.com wrote:

I'm trying to fix this section and it is just a mess. I think the definition of fiber sequence is still not even right: the homotopies have to be based homotopies, otherwise the canonical map from X_{n+1} to the fiber of f_n is not a pointed map. Plus it is really hard to find a good notation for "the basepoint of X_n" given that we usually write x_0 for the basepoint of X. I'm leaning towards not defining a general notion of "a fiber sequence" at all, instead just defining the fiber sequence associated to a based map.

— Reply to this email directly or view it on GitHub.

[mikeshulman]

I have reworked this section substantially -- in addition to the problems of exposition mentioned previously, and the problem of based homotopies and fiber sequences, there was another problem of minus signs that needed addressing. Is this more readable?

[dlicata335]

@guillaumebrunerie (who I think wrote the original version), can you make sure that there aren't any knock-down effects of this that need to happen where this gets used in the hopf fibration?

[guillaumebrunerie]

I only use the fact that the Hopf fibration does give rise to a long exact sequence of homotopy groups, so it’s fine. Sorry for the mess and thanks for fixing it.

[RobertHarper]

thanks, mike, vastly improved from my point of view!

On Jun 15, 2013, at 12:49 AM, Mike Shulman wrote:

I have reworked this section substantially -- in addition to the problems of exposition mentioned previously, and the problem of based homotopies and fiber sequences, there was another problem of minus signs that needed addressing. Is this more readable?

— Reply to this email directly or view it on GitHub.