From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCHZRD56UYLBBBHSU7OQKGQEGCDUFOQ@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 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-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f7314c82 for ; Tue, 25 Sep 2018 08:59:50 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id j65-v6sf24591536otc.5 for ; Tue, 25 Sep 2018 01:59:49 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1537865989; cv=pass; d=google.com; s=arc-20160816; b=aNWkQ4pvLR0D0Q01Wou8PojAfAMJl2lj3wNPFPBeG+cqeHCvwvj2YUjF2peAg5tMxh /rK+zQPjF8myjnVxqx+JLf5PXOOUmsQU+2OZYWfEKbFADZ/xfxAd46zKY5jRPt5q8D3s 3gQlcphttFw2ZVnYL/XLaSEvsfaT3zjOIg5FXHscEplfSqMbYCAPHsgUIhjOIUn/pPPJ 4e0ZgK32/T9QINPEEoPI4/6qvw2dbj+8B6CcDNUZT6htXBznz1GNnI3/6j+y80FXWjgk huiNsE7S07enOVjJz9tbQVuCWlHeZQdfZN3KPH+/QteN1hRExDG8HA8M8mzFU6Sjg6Dw UcLg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature:dkim-signature; bh=jkhkuxvDyTAv52TosTDyx/AjZXXCUl4f5ClbbhLSiws=; b=PFS4LUhxbR4lkMXc3dbD5oIrDgzEZWIMipaTkzzpPmU1DChO3BdrvjC7R9ZpRzEgey foJx4fzEz30CEyXkgzDb9oBsxGy10/taa0aqUuE/7IDios+ESV8JnjKH9ZhKlu7tLDZa jgmN9ea2bqXhMPX0P/3Ex5XEDRwA0rfpt3Jph/OHks/A0GXGd70gC24RvuA1Lih5zVAj tmyedyWLNmr2d1m+GQtIS+jxnZ3JjCKtyDAEXN76ws44sDHCCBobP7gZ39LTnjK/lgGX 4B9jSO3Qin7DIBrqnmDQ3a3F+OIUkZTS2nFZR0BC3Jjonge9lBFj1zUS0nCUhXIxlFGN 33eQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XsYbCYNd; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::143 as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=jkhkuxvDyTAv52TosTDyx/AjZXXCUl4f5ClbbhLSiws=; b=agOmSPK2Z6tL6/XUdXrf4ETwt8mp2NjK9bHAKn3qKZ35HVhcBOAUiseJvItNKaGVcM 19W6+9UcA/hWzkB56HHBWQFwG+yGpX8aDDgXEFAAAnzzbg2EtmAZbSRVm2iOL85SfqAZ D265c2ahWRxOS+pxSdPmmeH/EIHjltHYb+HiB9WS2PFC041Hx7oyOrrEz3PL9BqRTIfh FsZLeSkxKlCSFcV7sEO6+y1gQr23susye9NCfa6LQagciVellSM+cLSHn7Y6/TegsGUj RL9S1vvBgE6FhcEEE1dq1RX6I18yjeoTrYxal7tpjGYYwmCVARCcABjw6Zdgdpr4X3PL WAAw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=jkhkuxvDyTAv52TosTDyx/AjZXXCUl4f5ClbbhLSiws=; b=GW3VHNtKwCocBQGkVr+ci750B1PMCIXHjAtNNXoFCPsPtd9SQYtlhSaQDvC6zL6ya+ x3Llc86U72OjbkDeGkc2291eSXtDWjNORuL6U2YGnq9SpIRfsw/3qN2+uD4pNxY2Uef/ zoyU1f0MxWgpqVHvI+oe8oGiTJbdXoQTDf/7fhwhz/g5RWYOVLRbKGQuwQLCGaiNYSMg 9Z52gd15sr6d4L2iGpbDvOYI33yjofEX399NfXGRYfhciFPdjfWs0+MCXi7zc7eBVQk9 9TzrElf1dUii6ZMqOl7/XCSKds99LgWu6GiEwI9TUsLJDOq8AM2ClpF1737TwIYQxU3L Hq2Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=jkhkuxvDyTAv52TosTDyx/AjZXXCUl4f5ClbbhLSiws=; b=m6lhKfh3xVZpp0ijpgSeMEL5ry+4yumioyQ9U/h0p+eleJk6nEkvl/4KfznadRdDBx w+9t4h3hfF796V4VpLbP292AanMMjfeieoUAD64rIyqmW3mZzh+gYtA9Dw4JQw5zJHEG +ILNRTGsc1ifZHPMXjLVRn+Y1kIphc8C4U5tsLAdaSwVOQWZtV13Oue5bp+ADBoeqOnQ +2RAczGekI9lzJzQ8DHFT968FAXGH19hk0GZKP5jqAm1WDNhxrNprMlQRUVi36Sg/Elg lgrBnIImJl+9SMwcDzbF0TzTEJd6sbWV/XLOJVKoK0ZafmvEXVt84mLhz3ussuyCCZih D0Sg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfohZU2e9e8utJRfIiKyUiIdg2s4zbvQ+vbZFe86mLfa/RSwVFHDf LzocpqTiMNvQEraD02Q0Oq8= X-Google-Smtp-Source: ACcGV61nIWzEh+YePuNC7yk8jos4/QhJOGxHiSw+T406H9d4ngW627VW0817DSskf5mpqQ5jUQO6aw== X-Received: by 2002:a9d:5c02:: with SMTP id o2-v6mr37otk.7.1537865988933; Tue, 25 Sep 2018 01:59:48 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:cc14:: with SMTP id c20-v6ls3286307oig.14.gmail; Tue, 25 Sep 2018 01:59:48 -0700 (PDT) X-Received: by 2002:aca:ad42:: with SMTP id w63-v6mr2442084oie.31.1537865988508; Tue, 25 Sep 2018 01:59:48 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1537865988; cv=none; d=google.com; s=arc-20160816; b=rvHHxiBDy1DWJzpxG1is+jc3Vd3/WtGOobrwWdp6P9X5dAlgqTwi3f6W6QpWdhBpII 0E+7bpefcOTrrwLvnK7XUwTTpQZw9nseOOkMdBoTH5IMnYvmB0QoEekpV/7HBxu9/xeN QYGsG0hxpaWL9pH4iHZkAwDVg3zwdtBilW8opXbw/24yJjoUTNSrE8fkzZNtyCWXvXX+ 3Jcflurp3/xpzlCABn3K5dAntLN24X5KSEx3a4Hj20bycbjGQIqbbV2keet/eSSin6gb d0OSu1CBKCdgp+pIkn4jJiw086/57hEH2ssmjedmErQInGVJp8TT8tTlHoLL3Fmsmz2w xipg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=e+NBClXbADt0T+DZ2BMQLhnStY2mBmOdpPEISfpkZ4g=; b=s0uxMONAhVnzTDt2Uo8V23rtLWgCOjcm5HyzmZg4ZUsTaoCfImuM03FmYE1nE5zMYd trmqNesQrSWOldBPn571Z0Kxk5KAlPf6nb0jN2DrBHP3gWrdm3DySNm5TTZTpnLeihjc 4v8ZdntZ9f41dgAmLeZBk7pZWAAavXHypn5QethJ1J52eMNNAqemj07gf8jID7YGcXlJ UNVF9xP8pzVXrAQWOJnAl8HjOloDX2676IogVZJQ6Ux1m7kdxZwrkxLgyl/Knhp8xoSi iWgQ7iGMiBufihGAb8MOcxUw+w4XpBd1HAbSETabnrO9m3UpsowmnRVSfAsEI1MhiqE0 VQ5w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XsYbCYNd; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::143 as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x143.google.com (mail-it1-x143.google.com. [2607:f8b0:4864:20::143]) by gmr-mx.google.com with ESMTPS id v11-v6si109321oth.2.2018.09.25.01.59.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 25 Sep 2018 01:59:48 -0700 (PDT) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::143 as permitted sender) client-ip=2607:f8b0:4864:20::143; Received: by mail-it1-x143.google.com with SMTP id m9-v6so804979ita.2 for ; Tue, 25 Sep 2018 01:59:48 -0700 (PDT) X-Received: by 2002:a24:9f07:: with SMTP id c7-v6mr1850838ite.53.1537865988022; Tue, 25 Sep 2018 01:59:48 -0700 (PDT) MIME-Version: 1.0 References: <2d708865-8b2c-416d-9343-b550121e596a@googlegroups.com> <37A3D139-B011-4E22-8F56-799BACDB642E@cmu.edu> In-Reply-To: <37A3D139-B011-4E22-8F56-799BACDB642E@cmu.edu> From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Tue, 25 Sep 2018 04:59:36 -0400 Message-ID: Subject: Re: [HoTT] The Hodge structure of a type To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000eda7dd0576ae536e" X-Original-Sender: josephcmac@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XsYbCYNd; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::143 as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --000000000000eda7dd0576ae536e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > > Michael Shulman wrote: > what "algebraic" information it uses as input. In the case of the Hilbert scheme of n points on X, the information comes from the n-th symmetric power of X: https://arxiv.org/pdf/math/0304302.pdf So, the input are X as an infinite-groupoid and the natural number n. The output is the Hilbert scheme of n points on X as an infinite groupoid. I do not know if there is some nice functoriality in this process which could be expressed in HoTT in a natural way. There are more results about the Hilbert schemes it in Goettsche's homepage: http://users.ictp.it/~gottsche/ Kind Regards, Jos=C3=A9 M. El lun., 24 sept. 2018 a las 19:59, Steve Awodey () escribi=C3=B3: > > On Sep 24, 2018, at 6:30 PM, Ali Caglayan wrote: > > > > However I don't want to discourage you. One possible solution is > (differential?) cohesive homotopy type theory (which is at the moment eve= n > more undeveloped). This may allow you to talk about manifolds and their > structure "synthetically" which would allow for definitions of de Rham > cohomology and possibly with care allow you to talk about hilbert schemes > of some torus. Pessemistically I would add that it would be at least 10 > years before any of this is considered. > > just for perspective: > > - 10 years ago we had the (higher) homotopy group(oid)s, and not much mor= e. > - 5 years ago the HoTT book was just finished. > - 1 year ago the Serre spectral sequence was finished. > > things are moving pretty fast - I would not be so pessimistic. > > Steve > > -- > 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. > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --000000000000eda7dd0576ae536e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Michael Shulman wrote:
what "algebra= ic" information it uses as input.=C2=A0

In the case of the Hilbert scheme of n points on X, the information comes= from the n-th symmetric power of X:=C2=A0https://arxiv.org/pdf/math/0304302.pdf

=
So, the input are X as an infinite-groupoid and the natural numb= er n. The output is the Hilbert scheme of n points on X as an infinite grou= poid. I do not know if there is some nice functoriality in this process whi= ch could be expressed in HoTT in a natural way.=C2=A0 There are more result= s about the Hilbert schemes it in Goettsche's homepage:=C2=A0http://users.ictp.it/~gottsche/
=

Kind Regards,
Jos=C3=A9 M.


E= l lun., 24 sept. 2018 a las 19:59, Steve Awodey (<awodey@cmu.edu>) escribi=C3=B3:
> On Sep 24, 2018, at 6:30 PM, Ali Caglayan <alizter@gmail.com> w= rote:
>
> However I don't want to discourage you. One possible solution is (= differential?) cohesive homotopy type theory (which is at the moment even m= ore undeveloped). This may allow you to talk about manifolds and their stru= cture "synthetically" which would allow for definitions of de Rha= m cohomology and possibly with care allow you to talk about hilbert schemes= of some torus. Pessemistically I would add that it would be at least 10 ye= ars before any of this is considered.

just for perspective:

- 10 years ago we had the (higher) homotopy group(oid)s, and not much more.=
- 5 years ago the HoTT book was just finished.
- 1 year ago the Serre spectral sequence was finished.

things are moving pretty fast - I would not be so pessimistic.

Steve

--
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 https://groups.google.com/d/optout.

--
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.
--000000000000eda7dd0576ae536e--