search

HoTT / book

A textbook on informal homotopy type theory
2.04k stars 360 forks source link

Indexing of maps in fiber and exact sequences #1155

Closed EricWay1024 closed 9 months ago

EricWay1024 commented 9 months ago

In Definitions 8.4.3 (fiber sequence) and 8.4.5 (exact sequence), the indexing of the maps follows the pattern f^(n) : X^(n+1) -> X^(n). This is certainly valid but differs from what one would usually see in algebraic topology (e.g. https://en.wikipedia.org/wiki/Chain_complex), where the index of a map in a sequence would be the same as the index of its domain, i.e. f^(n) : X^(n) -> X^(n-1).

I am not sure if a change is needed but if so, I am happy to submit a PR.

Alizter commented 9 months ago

There is a difference between the indexing in algebraic topology and the one here however. In algebraic topology one might start with 1 as the first natural number, although this seems to be less common than it used to be. Since our natural numbers start with 0, it would be annoying having to special case f^(0). Therefore shifting the indexing by one, let's you have a "cleaner" indexing.

mikeshulman commented 9 months ago

Yeah, I'm inclined to stick with the current convention for that reason. It's not even that the f^n : X^n -> X^(n-1) convention chooses to start with 1 rather than 0, but it's inconsistent about where it starts: the X's start from 0, but the f's start from 1.

EricWay1024 commented 9 months ago

Thank you with your responses and I can see the rationale better now. I'll close the issue since nothing needs to be done.