I just read Mike Shulman's blog post the other night, discussing the definition of cohomology in Homotopy Type Theory. I really enjoyed the new (to me) perspective, but I had a few questions on technicalities.

Given types $X$ and $Y$, Mike defines

$$H^n(X; Y) :\equiv \| X \to \Omega^{-n} Y \|_0.$$

This agrees with the definition given in the nLab article on cohomology. Here is where my first question comes up:

  1. Although it's not stated in the article, I assume that for $n \neq 0$ we need $Y$ to be a pointed type, since (if I understand correctly) looping/delooping requires a choice of basepoint? Or does it not matter?

(Mike does explain in the article that for $n>0$ we need to specify choices of deloopings, since deloopings might not exist and might not be unique, and that we usually just take $Y$ to be a spectrum so that this works.)

However, in section 1.1 of this paper on Eilenberg-MacLane spaces in HoTT by Daniel Licata and Eric Finster they seem to be saying that the definition above actually produces reduced cohomology, since they write: enter image description here

On the other hand, in his blog post Mike writes defines reduced cohomology for pointed types $X$ and $Y$ by $$\tilde{H}^n(X; Y) :\equiv \| \operatorname{Map}_*(X, \Omega^{-n} Y) \|_0.$$ (He technically defines it only in the case that $Y$ is a spectrum, but I'm extrapolating here.) So this leads me to my second question:

  1. What is the correct definition for reduced cohomology in HoTT?

1 Answer 1

  1. In order for the notation $\Omega^{-n} Y$ to make sense for $n \ge 1$, $Y$ must be a grouplike $E_n$-space, which in particular means it has a basepoint (the identity of the $E_n$ multiplication). For $n \le -1$ we also need a basepoint to define the based loop space. However note that $X$ does not need to have a basepoint.

  2. As far as I can tell, the excerpt from Licata-Finster is incorrect; it gives ordinary cohomology, not reduced cohomology. Mike Shulman's definition is the correct one.

  • $\begingroup$ Thank you! Appreciate the clarification. $\endgroup$
    – ಠ_ಠ
    Commented Dec 10, 2020 at 0:52

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .