From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a27d8882 for ; Fri, 30 Nov 2018 05:20:39 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id u41sf2232749otc.10 for ; Thu, 29 Nov 2018 21:20:39 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Mvu/nxEHcgOTio/y6vLBSzaeE7EQeidLixJ1JunX33E=; b=cCQ0+VWM+yMrC8z09rqVPcypMqVG5hVvoQbkad6uC1Y4YTdq7DoDQb32+gZvhJin3q fVnmxy0v010lfdkX1Xn3OQ4AzscjqtsIigztpl5GVAkWNxnmrzfx9pOOXIj3VLDwJsLC gBIYdr8u0h98FXZJZTxCkhPZ/KopVXtyMshnmYRP1yJb/tTDHKwvpMPrOcDtCdP2Yp06 q2nwx2qFMuvb5RdlVoL4CsASCTRGwKyH6qmdH4ewQwKK9su+EqeYYil/QTrbBR6EVrmY 8CwmfpT0wzaxQahROP1YuW20oDypuklW7yx3LW8rGLjk9pJpjRbtyZpk0fK0ByySVQIn xkfA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=Mvu/nxEHcgOTio/y6vLBSzaeE7EQeidLixJ1JunX33E=; b=RaoBnTshSQ9LcXCrv0SSpubU1GjGX/MztvYJXgwQdqVY1vCDKujD1ivr+pZDmy0O4w iah7baDy/Baib3iC2t8G+EsQNvR0IdkzCUiZ9SRIpSuMTp09WFbOp57qBrR+AdO87tNv K3bAh34LxafR4/voQrrDaS6179XlV9b2A1UScWwtjQGqkAeJC9UbT7JpQR9kyQgdoeS/ DjQxUqnoggdKwUof9Yvthyv56+QN6FbA+PoTrxrvh0kqY5ktiTupcp4HfwwgDCqv0Sjr DIY8D9qDt2GmAryvnNEfSiinPTZo8cU5zJxCsaUjOe0mmE0DlX2MG8sKymroRSgco4kd 61rw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=Mvu/nxEHcgOTio/y6vLBSzaeE7EQeidLixJ1JunX33E=; b=NXgq/N1p+15Dd5kVaFlfqDo/qkMK1yka+OGBuyGUM2WDOTLsRWT0r3/0iRH8hI6iiF EJrCRpYhG5FZyEKAFGh6VqbbEtvz7QQmzMMEcQpZje4YUvx92OhpuOeWQXC9Dm8sK1JV WNiKQlWpOS/ebFbpXxKo8uUp7x+JVzK3YnNaYyTmHcVHHnAPY2sZWSDgW4M5cwkwDJyl xhUppkUnJEFkStl4GLJbUcJWumAi66f13d7ZVVgjlVInARCCWAsTIRThdHPWn5zmfxx+ wSKNHfYRfOG5lYrcbp3klyvPbaPYUPlqS8ECARdR+wZiR8Oa2Jn6OCE6SKE4r/PhaIET PcSg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AA+aEWbKIvZGYOE86jUp4ZrMWHYDLHLag0XU41wBtsWLXPyhUBI+bnQX 08YWLpDygJpNmNfel0DaBhA= X-Google-Smtp-Source: AFSGD/V2Y7k5Rujk55qhnPxwB+w4OhzJR/D4XiuCNPuFw1HbkrAy/+cQHisAtMUGpQZQwslq8Fxgtg== X-Received: by 2002:aca:5803:: with SMTP id m3-v6mr62175oib.4.1543555238070; Thu, 29 Nov 2018 21:20:38 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:c49:: with SMTP id 67ls2563590otr.4.gmail; Thu, 29 Nov 2018 21:20:37 -0800 (PST) X-Received: by 2002:a9d:2c22:: with SMTP id f31mr58366otb.4.1543555237204; Thu, 29 Nov 2018 21:20:37 -0800 (PST) Date: Thu, 29 Nov 2018 21:20:35 -0800 (PST) From: Felix Wellen To: Homotopy Type Theory Message-Id: <90646d1d-a0aa-4ebb-a7b8-f73fd9956259@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: Does (co)homology detect inhabitation? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_3312_52891385.1543555235911" X-Original-Sender: felix.wellen@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_3312_52891385.1543555235911 Content-Type: multipart/alternative; boundary="----=_Part_3313_938716220.1543555235911" ------=_Part_3313_938716220.1543555235911 Content-Type: text/plain; charset="UTF-8" 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. ------=_Part_3313_938716220.1543555235911 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I guess the answer is no for cohomology, here is why:
<= br>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)=3D0). 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=3D0, we = can do the following:
Take k=3DQ (the rationals) and let P=3DSpec(Q[X]/(= X^2-2)) (=3DSpec(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)=3D{Zariski-locally constant functions U -> Z}
=
So Z(P)=3DZ which implies Mor(P,Z)=3DZ for the external functions and s= taring at it for some time convinced me, that there should also be Z-many d= istinct global sections of

P->Z =3D ||P->Z||_0 =3D H^0(P,Z)

Now n=3D1:
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-schem= e.
First, let L:=3DSpec(Q[X,Y]/(Y^2-2)) (=3DSpec(Q(sqrt(2))[X]). Then L = has still no Q-points, for almost the same reason as above.
Now let L\{0= }:=3DSpec(Q[X,Y]/(Y^2-2)_(X)), where "_(X)" denotes the localizat= ion at the multiplicative system given by everything that is not in the ide= al generated by X.
And construct projective space (over Q(sqrt(2))) as a= pushout:

L\{0} -> L
=C2=A0|=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0 |
=C2=A0v=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 v
=C2=A0L --->= =C2=A0 P(Q(sqrt(2)))

Where we use the inclusion and the inversion af= ter inculsion as span.
P(Q(sqrt(2))) has still no Q-points.
We will l= ook at cohomology with coefficents in GL_1=3DSpec(Q[X,1/X]). So for the fir= st cohomology group, we have

H^1(M,GL_1)=3D||P(Q(sqrt(2)))->BGL_1= ||_0

But Mor(P(Q(sqrt(2))),BGL_1)=3DPic(P(Q(sqrt(2))))=3DZ is a know= n fact.
Avoiding this reference and using some fishy mix between intern= al 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<= br>
are pairs of maps f,g : L->BGL_1 together with an equality f(x)= =3Dg(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)=3Dg(1/x)

is given by a map

L\{0} -> GL_1
<= br>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 2= 018 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. =C2=A0In 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. =C2=A0Can I conclude (without using excluded middle) th= at
||X||?

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_3313_938716220.1543555235911-- ------=_Part_3312_52891385.1543555235911--