From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBB4XPWXOQKGQEQDVZT3Q@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-x338.google.com (mail-ot1-x338.google.com [IPv6:2607:f8b0:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3122eb9f for ; Fri, 28 Sep 2018 00:38:12 +0000 (UTC) Received: by mail-ot1-x338.google.com with SMTP id n54-v6sf5443477otb.11 for ; Thu, 27 Sep 2018 17:38:12 -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=LN6hRZFMZ7B99aevsQxR6a8oj00TrRpG6UiDNou724c=; b=CmQWIIA+qnFfDs8CZedWdKfkYlNXQGxbdJw1vZgXlatICyu1YjpVll+sKIuScF1EVz 5dIZk86jIlJg5IqQbu33mk8WXJOaOTDAxpJclY+swNVL50jm3GeoZ5377Ji3igFxyaEh 2mvnO5/QzPu4lKQFQ6s3kbfhMp9nrHLWfuodornG/EM4puCpF9RM2FNENgedttszq2Od 2o5J0Pnn+5j8KCpk9SpjsCJWw4Xd59VZ502M9RTbOz2nNXG9YQYkKBsZwxEIX+KRuWPI 2df+CAyBOkrY5OxOTB0Hwu+HgEL2dNXkWwI0kG+DCmsQn8RCRaa2ngZHBF0xfPOjqP1a eAIA== 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=LN6hRZFMZ7B99aevsQxR6a8oj00TrRpG6UiDNou724c=; b=q7UtRMfr0jfW4znNRbhSX4KlpJEf1PRgaGh/JAeWmnxJSOApwOQrpd8KP1AVDEeTNz Bd1slV5/Z6OcOgss2lthaWViMESLxNLBnCRbS8t4/QfQDM3r7E4BliN5/wWlwGGLWftp nrmGoY3sHll2GWhISDjf38UIMZ00apenRobxq2zanPBeMkoVLhV+Bcd85pbqG1yEzc0i rm2ZWnb662Z3r0VUcDme9Yp7y2Q8vBDdpYdUirSuwNfnfctHxwJlBYbvKA3QPsaTc+80 LSBxi/SlgXQnztCmpuRWZ6jFWwaMzG8uErPGdys0P6aqnlvdfKS6jBoeV+lthlmiKuAS 13TA== 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=LN6hRZFMZ7B99aevsQxR6a8oj00TrRpG6UiDNou724c=; b=ujiaYMbLEMcCvn5qx8IeePKhgOugQsUV9vux0T6Ct6Nafx0Zw866Z77U4Os6QZg0cV l6AN7MHRhttIKFXrxbeGJ/vxo1XMiT5xolVq0XH9H8O93DJhVqbd4QUTVh2T9EUqxYqy bnOGE8/G3lNBDu0TpvdVojGW86nr5qSfRRv35PQ2dJSi7LG7LJbw+HHrl9DLacaNznZ6 i7jY9PF2p7wb7dwh0yv+LEf/89WHlNQmCBqkL8XUPyJZaW1YwSRInybD4gMVtT0FtW98 zcdPlHBlKgwVYGkvC49kqGy1Sp/21qP9vjYnwFaj5/3Q/QTnRj4ipvDcEqdDmGuRaKNE ArHA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfoiK6sNuhJii0r6vE4DalfYBj30t+ia5Ei/QPDgIuRsFcMVscHb3 k//xq9os8HLMc+9H8naBiSA= X-Google-Smtp-Source: ACcGV60c/UNVvSdfxJJLPSHcmaY4k3m1HuNX7vvUnAdOrVKQeDptwHK6U3DnrSyXJZ1JTYT32s+vxw== X-Received: by 2002:aca:fc85:: with SMTP id a127-v6mr233524oii.6.1538095090226; Thu, 27 Sep 2018 17:38:10 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1803:: with SMTP id h3-v6ls4567021oih.13.gmail; Thu, 27 Sep 2018 17:38:10 -0700 (PDT) X-Received: by 2002:aca:eb91:: with SMTP id j139-v6mr240396oih.4.1538095089614; Thu, 27 Sep 2018 17:38:09 -0700 (PDT) Date: Thu, 27 Sep 2018 17:38:08 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: In-Reply-To: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> Subject: [HoTT] Re: Characteristic Classes for Types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_125_1996505488.1538095088892" 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_125_1996505488.1538095088892 Content-Type: multipart/alternative; boundary="----=_Part_126_891461344.1538095088893" ------=_Part_126_891461344.1538095088893 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 1. This could be possible once a vector bundle has been fully defined. The= =20 idea behind characteristic classes is to classify certain vector bundles=20 with cohomology. This however may be a bit in the future as, for example,= =20 grassmannians have not yet been defined. Also orthogonal groups are not yet= =20 defined. So it is impossible to say right now if this can be done but it=20 seems likely. 2. Cohomology in HoTT is not by default singular cohomology like in=20 algebraic topology. In HoTT we take the definition of cohomology to be the= =20 (truncated) set of maps to an Eilenberg-Maclane space. Concering cohomology= =20 operations, this should definitely be possible. Literature on cohomology=20 has come out in the last few years so expect more to be written about it. 3. Atiyah-Singer would need quite a lot of work, not to mention the fact it= =20 involves differential structure. Which at the moment it is expected that=20 differential cohesive HoTT may be able to tackle such a theorem. HoTT on=20 it's own is quite good at talking about purely homotopical structure. This= =20 is an important point because many topological/manifoldy theorems are not= =20 necesserily homotopical in nature. They may depend on extra structure that= =20 HoTT cannot really describe adequately yet. Take for example Riemann-Roch= =20 which can be considered a special case of Atiyah-Singer. It would need a=20 good amount of algebraic geometry to be defined and/or proven in order to= =20 state the theorem. Which is unliekly to come around in the next few years.= =20 This doesn't mean it couldn't happen. Just to show you how underdeveloped cohomology in HoTT is at the moment, an= =20 "elementary" theorem of algebraic topology, the Hurewicz theorem, has not= =20 been proven yet. Though I believe it will be tackled soon. Types are not topological spaces, they are more literally homotopy types.= =20 This is why I personally, found "the Hodge structure of a type" to be not= =20 within our current viewpoint although Steve Awodey's point about the speed= =20 of the development of HoTT has been considered. And one final thing: One of the reasons algebraic topologists are exicited= =20 about using and developing HoTT is that it gives a synthetic foundation to= =20 many "purely homotopical" ideas used in algebraic topology that have proofs= =20 and constructions relient on outside ideas or formalisms. This isn't=20 necesserily a bad thing (look at cobordisms in stable homotopy) however=20 some simpler areas of the subject should be able to hold their own. (As I= =20 understand).=20 Therefore it stands to reason that it is unlikely that HoTT will bring=20 anything new to the table when it comes to the ideas you are talking about.= =20 HoTT essentially provides a synthetic way to reason about homotopy types,= =20 but it isn't an enlightening viewpoint for theorems not homotopic in nature= . And really finally this time: Have a look around at what people are doing= =20 in HoTT at the moment. For example Floris van Doorn's thesis where spectral= =20 sequences for cohomology have been developed in HoTT and formalised in the= =20 Spectral library for the Lean proof assistant. The agda formalisation of=20 HoTT also usually has a lot of the latest gadgets of snythetic homootpy=20 theory. Which is a fascinating subject if I do say so myself, but it isn't= =20 algebraic topology. There is a massive intersection but don't take them to= =20 be the same thing. Anyway if you have read this for congratulations. Ali Caglayan On Thursday, 27 September 2018 14:10:09 UTC+1, Juan Ospina wrote: > > Recently, there was a post about the Euler characteristic of a type and= =20 > other post about Hodge structure of a type. Then my questions are: > > 1) It is possible to construct characteristic classes (Wu,=20 > Stiefel-Whitney, Chern, Pontryagin classes) for an arbitrary type in= =20 > HoTT? > > 2) It is possible to construct singular cohomology for a type and the=20 > corresponding Steenrod operations? > > 3) It is possible to construct an Aityah-Singer index theorem for an=20 > arbitrary type (a type fibered with other type). > > 4) It is possible to construct integrality theores for the characteristic= =20 > numbers of an arbitrary fibered type? > > > Many thanks. > > Juan Ospina > Medell=C3=ADn, Colombia > > > --=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_126_891461344.1538095088893 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
1. This could be possibl= e once a vector bundle has been fully defined. The idea behind characterist= ic classes is to classify certain vector bundles with cohomology. This howe= ver may be a bit in the future as, for example, grassmannians have not yet = been defined. Also orthogonal groups are not yet defined. So it is impossib= le to say right now if this can be done but it seems likely.

2. Coho= mology in HoTT is not by default singular cohomology like in algebraic topo= logy. In HoTT we take the definition of cohomology to be the (truncated) se= t of maps to an Eilenberg-Maclane space. Concering cohomology operations, t= his should definitely be possible. Literature on cohomology has come out in= the last few years so expect more to be written about it.

3. Atiyah= -Singer would need quite a lot of work, not to mention the fact it involves= differential structure. Which at the moment it is expected that differenti= al cohesive HoTT may be able to tackle such a theorem. HoTT on it's own= is quite good at talking about purely homotopical structure. This is an im= portant point because many topological/manifoldy theorems are not necesseri= ly homotopical in nature. They may depend on extra structure that HoTT cann= ot really describe adequately yet. Take for example Riemann-Roch which can = be considered a special case of Atiyah-Singer. It would need a good amount = of algebraic geometry to be defined and/or proven in order to state the the= orem. Which is unliekly to come around in the next few years. This doesn= 9;t mean it couldn't happen.

=
Just to show you how underdeveloped = cohomology in HoTT is at the moment, an "elementary" theorem of a= lgebraic topology, the Hurewicz theorem, has not been proven yet. Though I = believe it will be tackled soon.

=
Types are not topological spaces, th= ey are more literally homotopy types. This is why I personally, found "= ;the Hodge structure of a type" to be not within our current viewpoint= although Steve Awodey's point about the speed of the development of Ho= TT has been considered.

And one final thing: One of the reasons a= lgebraic topologists are exicited about using and developing HoTT is that i= t gives a synthetic foundation to many "purely homotopical" ideas= used in algebraic topology that have proofs and constructions relient on o= utside ideas or formalisms. This isn't necesserily a bad thing (look at= cobordisms in stable homotopy) however some simpler areas of the subject s= hould be able to hold their own. (As I understand).=C2=A0

Therefore= it stands to reason that it is unlikely that HoTT will bring anything new = to the table when it comes to the ideas you are talking about. HoTT essenti= ally provides a synthetic way to reason about homotopy types, but it isn= 9;t an enlightening viewpoint for theorems not homotopic in nature.

A= nd really finally this time: Have a look around at what people are doing in= HoTT at the moment. For example Floris van Doorn's thesis where spectr= al sequences for cohomology have been developed in HoTT and formalised in t= he Spectral library for the Lean proof assistant. The agda formalisation of= HoTT also usually has a lot of the latest gadgets of snythetic homootpy th= eory. Which is a fascinating subject if I do say so myself, but it isn'= t algebraic topology. There is a massive intersection but don't take th= em to be the same thing.

Anyway if you have read this for congratulat= ions.

Ali Caglayan

On Thursday, 27 September 2018 14:10:09 U= TC+1, Juan Ospina wrote:
Recently, there was a post about the Euler characteristic = of a type and other post about Hodge structure of a type.=C2=A0 Then my que= stions are:

1) It is possible to construct charact= eristic classes=C2=A0 (Wu, Stiefel-Whitney, Chern, Pontryagin classes) =C2= =A0=C2=A0 for an arbitrary type in HoTT?

2) It is = possible to construct singular cohomology for a type and the corresponding = Steenrod operations?

3) It is possible to construc= t an Aityah-Singer index theorem for an arbitrary type (a type fibered with= other type).

4) It is possible to construct integ= rality theores for the characteristic numbers of an arbitrary fibered type?=


Many thanks.

<= div>Juan Ospina
Medell=C3=ADn,=C2=A0 Colombia

<= /div>

--
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_126_891461344.1538095088893-- ------=_Part_125_1996505488.1538095088892--