I guess the answer is no for cohomology, here is why:
I can sketch examples of cohomologically nontrivial schemes over a base field k, without any k-points. Such a scheme is an object X in the oo-topos of sheaves on the zariski site and its propositional truncation ||X|| will be empty at k (||X||(k)=0). So ||X|| can't be the unit type.
For me, the questions makes already sense for the 0th-cohomology group. Don't know if that was included in your question.
So for n=0, we can do the following:
Take k=Q (the rationals) and let P=Spec(Q[X]/(X^2-2)) (=Spec(Q(sqrt(2)))).
Then P has no Q-point, since there is no square root of 2 in Q. Now look at the sheaf Z constantly the integers. Its value are
Z(U)={Zariski-locally constant functions U -> Z}
So Z(P)=Z which implies Mor(P,Z)=Z for the external functions and staring at it for some time convinced me, that there should also be Z-many distinct global sections of
P->Z = ||P->Z||_0 = H^0(P,Z)
Now n=1:
For a scheme having still no Q-points but cohmology in degree 1, I propose to use projective space over Q(sqrt(2)) as a Q-scheme.
First, let L:=Spec(Q[X,Y]/(Y^2-2)) (=Spec(Q(sqrt(2))[X]). Then L has still no Q-points, for almost the same reason as above.
Now let L\{0}:=Spec(Q[X,Y]/(Y^2-2)_(X)), where "_(X)" denotes the localization at the multiplicative system given by everything that is not in the ideal generated by X.
And construct projective space (over Q(sqrt(2))) as a pushout:
L\{0} -> L
| |
v v
L ---> P(Q(sqrt(2)))
Where we use the inclusion and the inversion after inculsion as span.
P(Q(sqrt(2))) has still no Q-points.
We will look at cohomology with coefficents in GL_1=Spec(Q[X,1/X]). So for the first cohomology group, we have
H^1(M,GL_1)=||P(Q(sqrt(2)))->BGL_1||_0
But Mor(P(Q(sqrt(2))),BGL_1)=Pic(P(Q(sqrt(2))))=Z is a known fact.
Avoiding this reference and using some fishy mix between internal and external reasoning, one could also argue:
Use the recursion rule of the pushout (as a HIT) to see that maps
P(Q(sqrt(2)))->BGL_1
are pairs of maps f,g : L->BGL_1 together with an equality f(x)=g(1/x) for all x in L\{0}. So no matter what choice of maps f,g : L -> BGL_1 we can make (in reality, there is only one), we get a different map for each choice of family of equality that glues them.
Let's choose constant maps for f and g, then a family of equalities
(x : L\{0}) -> f(x)=g(1/x)
is given by a map
L\{0} -> GL_1
or
Q[X,1/X] -> Q[X,Y]/(Y^2-2)_(X)
And for each k in Z, we have such a map given by X |-> X^k, and they are all different, so Z is a factor of H^1(P(Q(sqrt(2))), GL_1).
Am Dienstag, 27. November 2018 17:22:30 UTC-5 schrieb Michael Shulman:
Suppose I have an (unpointed) type X such that (unreduced) H_n(X) or
H^n(X) is nonzero for some n. In the application I have in mind, this
group is nonzero in a very strong sense, e.g. it has the integers as a
direct summand. Can I conclude (without using excluded middle) that
||X||?