From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBM5HTPOQKGQENVXWKFY@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-oi0-x23e.google.com (mail-oi0-x23e.google.com [IPv6:2607:f8b0:4003:c06::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id cfea4e00 for ; Sat, 22 Sep 2018 23:43:49 +0000 (UTC) Received: by mail-oi0-x23e.google.com with SMTP id 13-v6sf15912218oiq.1 for ; Sat, 22 Sep 2018 16:43:48 -0700 (PDT) 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=E+s1zLxyBZc4yxPo+NVTaPhjd3dmtmx/Z/TsebxWpHg=; b=I38B/z/G+KuLYXsXp6veZwkoR76Af65wQnWQbgD7RLj1YNJDZNnKghhLQYZg67Q5xO QJTxUI4QX6mdx25BVscSowlvfoo6gkvIeZpBUKNRpILVPONTQgVUVtXcU4KY5JJ3vXoc Oog4khRkiEJVZcoyVar5jWyhy6A1SnoQZsiLlqYDgExmQEdmyU++78esa5pbbbwWlg0i CyuZm/lWAWpTHAVN9ura9evZSBtobKZeAH/wJ4huwr+OT8ChTuUd5wYlVI+N3wYKRLxS qydfdqFdjHMOw0Ee9Gw/CFViLg3rGcRTdWNlomXfm+Hb9mwk3fzseXfkK8auITCH/5E/ 6PWQ== 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=E+s1zLxyBZc4yxPo+NVTaPhjd3dmtmx/Z/TsebxWpHg=; b=nzYiZHWTdDYOKP7kPNTQNFdgaZ63oHbTCmP45TmhKhGYpfsS7tQ7YB6WvlkL3wPoKI NtClYMQF7FlBOOYefOZcUuXj6zz79xpHHkq0dsPN87Dir5uwzBSHUa4Nsxx58lG4I0tW +vW7OZVvDBrTb60JUze8Mbi1y4/7sOG8s6LQ7mEqcn4jTQyuu+ViKth7VFHE/c8UFNsd EGwso+fbd7lDqZKiNg2uJScty5VumZYiaKAXEeoS8IZX991zssFSBYBX5QjTp6V0QbG8 q9vvdzDwOXHMIu/aDkLrfwdD3m9DK11wptS61sYdRxSVjb1ZY1GjW3+n1IZ0nlAHSuhr Mx0g== 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=E+s1zLxyBZc4yxPo+NVTaPhjd3dmtmx/Z/TsebxWpHg=; b=SiwynmE+V1GDvDESIXDWGHaOPH0Lno2v1zEY2gkSzePXyAvAM/sUfr/xaL4PDO3nKT n1V5LRpZllTOLxjthgXeP3GqwL/uMK/m2E6UmPKJsPJ5nIpq56VJnj5ope5NMiSe94af 5Vn02P4C86TonxrY+sof2OTT1UjACTQ5h1frdT+7rGpzahKMSlPrO8SZUA6SynnP6/eQ yHhls7aksnXNMHdvXHFtxapYfSGFl/RtpMPl1UoXTOXfrpnBNQ9DZVXDbRRlepsfw3zI HCR7BbHAE5ZbVKBJSsP/GXzufcX5G3mWrw6YGfmO7GZmVEY3J+WN1JihkMF7DkXs8/+4 BIeQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51ApBZa9NZw9H/WBZNrsBSQBK1eI0dRSO3T13QE7HHT0wSAmEdyO eTEdbho7x8O7jZf746bO9u0= X-Google-Smtp-Source: ANB0VdZ7j93DdI3Pjhk/2Snohy4v99XFKE3WSWvhrWr5Gqu6a4i8kagQmm+6JG1gS96viJrrW4I3Wg== X-Received: by 2002:aca:d417:: with SMTP id l23-v6mr51347oig.7.1537659827942; Sat, 22 Sep 2018 16:43:47 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:4a2a:: with SMTP id h39-v6ls1931966otf.2.gmail; Sat, 22 Sep 2018 16:43:47 -0700 (PDT) X-Received: by 2002:a9d:618e:: with SMTP id g14-v6mr2098otk.3.1537659827530; Sat, 22 Sep 2018 16:43:47 -0700 (PDT) Date: Sat, 22 Sep 2018 16:43:46 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <0f8ff942-2cd1-4714-b8f7-865caf626fba@googlegroups.com> In-Reply-To: References: Subject: Re: [HoTT] The Hodge structure of a type MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1288_1528460019.1537659826994" X-Original-Sender: alizter@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_1288_1528460019.1537659826994 Content-Type: multipart/alternative; boundary="----=_Part_1289_827959200.1537659826995" ------=_Part_1289_827959200.1537659826995 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I don't think HoTT is any position to be used in algebraic geometry as it= =20 stands currently. There may be a way in via a functor of points approach=20 which is well suited for constructing Hilbert schemes. However I think it= =20 would be impossible to say anything concrete at this point. Homology and=20 cohomology are usually seen as "easy" invariants about spaces to calculate= =20 however in HoTT it is all very new and nobody quite know the best way to go= =20 about reasoning with these things. Let alone thinking about something with= =20 extra structure like Hodge structure. However representation theory, as you have cited, may be more tractable.=20 There are good formal properties of HoTT which may allow it to reason in=20 representation theoretic terms quite concretely. So if you are interested= =20 in studying quiver varieties you may just be able to get away with studying= =20 quiver representations. However this is all speculative at this point. I=20 don't think there are any researchers looking into any of these things yet= =20 as I believe HoTT just is not sophisticated to carry out such reasoning. But this is all my opinion. I would be very suprised if anybody says=20 otherwise. On Saturday, 22 September 2018 17:59:03 UTC+1, Jos=C3=A9 Manuel Rodriguez= =20 Caballero wrote: > > Recently, there was a post about the Euler characteristic of a type. In m= y=20 > case, I am interested in the Hodge structure of the Hilbert scheme of n= =20 > points on a 2-dimensional torus. Does such a topological construction mak= e=20 > sense in HoTT for an arbitrary type, under some general hypothesis? > > Kind Regards, > Jose M > > References about the topological structure that I am studying:=20 > https://www.sciencedirect.com/science/article/pii/S0001870812004008 > --=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. ------=_Part_1289_827959200.1537659826995 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I don't think HoTT is any position to be used in algeb= raic geometry as it stands currently. There may be a way in via a functor o= f points approach which is well suited for constructing Hilbert schemes. Ho= wever I think it would be impossible to say anything concrete at this point= . Homology and cohomology are usually seen as "easy" invariants a= bout spaces to calculate however in HoTT it is all very new and nobody quit= e know the best way to go about reasoning with these things. Let alone thin= king about something with extra structure like Hodge structure.

However representation theory, as you have cited, may be more tract= able. There are good formal properties of HoTT which may allow it to reason= in representation theoretic terms quite concretely. So if you are interest= ed in studying quiver varieties you may just be able to get away with study= ing quiver representations. However this is all speculative at this point. = I don't think there are any researchers looking into any of these thing= s yet as I believe HoTT just is not sophisticated to carry out such reasoni= ng.

But this is all my opinion. I would be very su= prised if anybody says otherwise.

On Saturday, 22 September 2018 17:= 59:03 UTC+1, Jos=C3=A9 Manuel Rodriguez Caballero wrote:
Recently, the= re was a post about the Euler characteristic of a type. In my case, I am in= terested in the Hodge structure of the Hilbert scheme of n points on a 2-di= mensional torus. Does such a topological construction make sense in HoTT fo= r an arbitrary type, under some general hypothesis?

Kind= Regards,
Jose M

References about the to= pological structure that I am studying:=C2=A0https://www.sciencedirect.com/science/art= icle/pii/S0001870812004008

--
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_1289_827959200.1537659826995-- ------=_Part_1288_1528460019.1537659826994--