From: Felix Wellen <felix.wellen@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Re: Does (co)homology detect inhabitation?
Date: Thu, 29 Nov 2018 21:20:35 -0800 (PST) [thread overview]
Message-ID: <90646d1d-a0aa-4ebb-a7b8-f73fd9956259@googlegroups.com> (raw)
In-Reply-To: <CAOvivQwZnc0_LFFXTFqfVabBWE0tARLDd929rF4z3Gei1VRZtg@mail.gmail.com>
[-- Attachment #1.1: Type: text/plain, Size: 3300 bytes --]
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||?
>
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #1.2: Type: text/html, Size: 3852 bytes --]
next prev parent reply other threads:[~2018-11-30 5:20 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-11-27 22:22 [HoTT] " Michael Shulman
2018-11-30 5:20 ` Felix Wellen [this message]
2018-11-30 21:54 ` [HoTT] " Felix Wellen
2018-12-04 22:33 ` Ali Caglayan
2018-12-04 23:15 ` Michael Shulman
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=90646d1d-a0aa-4ebb-a7b8-f73fd9956259@googlegroups.com \
--to=felix.wellen@gmail.com \
--cc=HomotopyTypeTheory@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).