[HoTT] Does (co)homology detect inhabitation?

[HoTT] Does (co)homology detect inhabitation?

[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.

[HoTT] Re: Does (co)homology detect inhabitation?

[Felix Wellen]

[-- 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 --]

[HoTT] Re: Does (co)homology detect inhabitation?

[Felix Wellen]

[-- 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 --]

[HoTT] Re: Does (co)homology detect inhabitation?

[Ali Caglayan]

[-- 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 --]

Re: [HoTT] Re: Does (co)homology detect inhabitation?

[Michael Shulman]

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.