* [HoTT] Does (co)homology detect inhabitation?
@ 2018-11-27 22:22 Michael Shulman
2018-11-30 5:20 ` [HoTT] " Felix Wellen
` (2 more replies)
0 siblings, 3 replies; 5+ messages in thread
From: Michael Shulman @ 2018-11-27 22:22 UTC (permalink / raw)
To: homotopytypetheory
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.
^ permalink raw reply [flat|nested] 5+ messages in thread
* [HoTT] Re: Does (co)homology detect inhabitation?
2018-11-27 22:22 [HoTT] Does (co)homology detect inhabitation? Michael Shulman
@ 2018-11-30 5:20 ` Felix Wellen
2018-11-30 21:54 ` Felix Wellen
2018-12-04 22:33 ` Ali Caglayan
2 siblings, 0 replies; 5+ messages in thread
From: Felix Wellen @ 2018-11-30 5:20 UTC (permalink / raw)
To: Homotopy Type Theory
[-- 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 --]
^ permalink raw reply [flat|nested] 5+ messages in thread
* [HoTT] Re: Does (co)homology detect inhabitation?
2018-11-27 22:22 [HoTT] Does (co)homology detect inhabitation? Michael Shulman
2018-11-30 5:20 ` [HoTT] " Felix Wellen
@ 2018-11-30 21:54 ` Felix Wellen
2018-12-04 22:33 ` Ali Caglayan
2 siblings, 0 replies; 5+ messages in thread
From: Felix Wellen @ 2018-11-30 21:54 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 908 bytes --]
Thierry caught a mistake in my answer, so both my counterexamples actually
don't work at least for the strong requirement that Z is factor.
The problem is, that the cohomology classes/maps P->Z I use are not
different over Q.
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: 1308 bytes --]
^ permalink raw reply [flat|nested] 5+ messages in thread
* [HoTT] Re: Does (co)homology detect inhabitation?
2018-11-27 22:22 [HoTT] Does (co)homology detect inhabitation? Michael Shulman
2018-11-30 5:20 ` [HoTT] " Felix Wellen
2018-11-30 21:54 ` Felix Wellen
@ 2018-12-04 22:33 ` Ali Caglayan
2018-12-04 23:15 ` Michael Shulman
2 siblings, 1 reply; 5+ messages in thread
From: Ali Caglayan @ 2018-12-04 22:33 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 711 bytes --]
Can it be done with excluded middle?
On Tuesday, 27 November 2018 22:22:30 UTC, Michael Shulman wrote:
>
> 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: 1045 bytes --]
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [HoTT] Re: Does (co)homology detect inhabitation?
2018-12-04 22:33 ` Ali Caglayan
@ 2018-12-04 23:15 ` Michael Shulman
0 siblings, 0 replies; 5+ messages in thread
From: Michael Shulman @ 2018-12-04 23:15 UTC (permalink / raw)
To: Ali Caglayan; +Cc: HomotopyTypeTheory
Of course. WIth excluded middle, either ||X|| or not ||X||, and in
the latter case X is empty too so its homology and cohomology are all
0.
On Tue, Dec 4, 2018 at 2:33 PM Ali Caglayan <alizter@gmail.com> wrote:
>
> Can it be done with excluded middle?
>
> On Tuesday, 27 November 2018 22:22:30 UTC, Michael Shulman wrote:
>>
>> 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.
--
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.
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2018-12-04 23:15 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-11-27 22:22 [HoTT] Does (co)homology detect inhabitation? Michael Shulman
2018-11-30 5:20 ` [HoTT] " Felix Wellen
2018-11-30 21:54 ` Felix Wellen
2018-12-04 22:33 ` Ali Caglayan
2018-12-04 23:15 ` Michael Shulman
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).