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

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

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

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.