From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDF4ZP7WUQGRBSH2WXOQKGQEFPATLYI@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-x33d.google.com (mail-ot1-x33d.google.com [IPv6:2607:f8b0:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d6c8849a for ; Fri, 28 Sep 2018 01:00:58 +0000 (UTC) Received: by mail-ot1-x33d.google.com with SMTP id e69-v6sf5456605ote.17 for ; Thu, 27 Sep 2018 18:00:57 -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=tsw+WvatV0GXJyexQ2skN6MlQQkrZKiD63bCvVBFLVs=; b=d0f+hmgpjT3F2OtYnqm/0aFLWSq/8URFLGT0BRFv3nOqa73nw3lJpXs4yGDMUQd1Jp tld7hopvUYX1nB2TVBFkwEQ5T0iF1IOcETsCZXZs+BN/xCyb0XUU5hcEF+Ciyupi9cmi o2SKbXmIt+qYniTUnRANT28PGSx6b099kwHaTRAXYHt+/syn+o6Zok0Mi1D9HY03oGLP lCONH/kNJnz4Ch/0fcwlhAnT4OPePOzPLqSvMBGVMnpZudthwMZLSIJaPk9MHoFW2fqJ /4s4YV1253e2gpHyo0FwxBOslQWvN0SsYIwD6Fbc3rDmF8yKutwK9GOKUoeHz7hbGEKq acqg== 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=tsw+WvatV0GXJyexQ2skN6MlQQkrZKiD63bCvVBFLVs=; b=keD+TkYVbFMaCjL7LsCk+cSKg/P0vNuipbSVPdrlSsXPeI9mRQjU9+fuea8eF0xCrN OjrCqRYjjorH+jfqqKWY+8ZYRc4EXZhEE3RHgpTUjs8P0gy8N84TL8IA0IxRFeByjSy7 fIPF0tUScpKCLaRWObpy52kjRnFJ8JCqSV7v0FvvXW+6JQ5sKfkgahOboTq/7Ga21N17 1T2SyMdptrUCCDIvB0oZtN2bhEsySsSx2KI4bSPNo0vKasXJOKSPsTKq12ycFv/8EWTZ EwUf4JNaQJQSmNwmR5Yn9wv4ipb7YhNDH567ShP7GnDc74K7XMsIfCeL+Db1ah/vd/h8 4Obg== 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=tsw+WvatV0GXJyexQ2skN6MlQQkrZKiD63bCvVBFLVs=; b=J1iEehCQsPW2ZmowireT6SRkS218mj18RlfO7v+Ft3zDPB+wnANuouNZUzbW6hZ22j 6ylv/pCnKp7nEzdK5pB8awE7S5upZgSIZ2rUZweC359B4zXUhrFTF1VgvP2HSRGoB04n qW1SZ0Ng9ptms5XOcCYmVGJ0/1wTroSexXR53WJzgDSAGaaCMrxGbz5Zup2/tcjmnc5O dfAtrhXHfWbebYwmvl/XRUhKxtQJLyJQk8BMCdN5doqZGBn1zsVgD4IR2quBG57ASbAs pCN6MjE8yBi2cgayTACAV7+jTTTOCY8sOXl0+ogU/rD3sM0fHqo3ClycxLQVeUeUHpba QqUw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfohYAndH/JTd0r90UvufWEuD1zmhBXRaIXBiBLH4uOR4+i6L6GC5 7Wb8ECxqq444pq/F8WK/Ez8= X-Google-Smtp-Source: ACcGV63X4PWHzfIxZUJqmWlmzEa8IQ2u8Gip/RTXKhFEAG3/+tuh5QxI0aVMX3+3n6U93kH+SHlotw== X-Received: by 2002:aca:3094:: with SMTP id w142-v6mr42748oiw.0.1538096456992; Thu, 27 Sep 2018 18:00:56 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1219:: with SMTP id 25-v6ls4335977ois.12.gmail; Thu, 27 Sep 2018 18:00:56 -0700 (PDT) X-Received: by 2002:aca:c656:: with SMTP id w83-v6mr242734oif.2.1538096456606; Thu, 27 Sep 2018 18:00:56 -0700 (PDT) Date: Thu, 27 Sep 2018 18:00:55 -0700 (PDT) From: Juan Ospina To: Homotopy Type Theory Message-Id: In-Reply-To: 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_106_1655092086.1538096456010" X-Original-Sender: jospina65@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_106_1655092086.1538096456010 Content-Type: multipart/alternative; boundary="----=_Part_107_1326560379.1538096456010" ------=_Part_107_1326560379.1538096456010 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Many thanks for your comments which are very instructive. Actually I am= =20 trying to understand anything in the Floris van Doorn's thesis,=20 particularly the formalization in HoTT for the *Atiyah*-*Hirzebruch=20 spectral* sequence and the *Leray*-*Serre spectral* sequence. On Thursday, September 27, 2018 at 7:38:09 PM UTC-5, Ali Caglayan wrote: > > 1. This could be possible once a vector bundle has been fully defined. Th= e=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 y= et=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 th= e=20 > (truncated) set of maps to an Eilenberg-Maclane space. Concering cohomolo= gy=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= =20 > it involves differential structure. Which at the moment it is expected th= at=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. Thi= s=20 > is an important point because many topological/manifoldy theorems are not= =20 > necesserily homotopical in nature. They may depend on extra structure tha= t=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,= =20 > an "elementary" theorem of algebraic topology, the Hurewicz theorem, has= =20 > not 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 spee= d=20 > of the development of HoTT has been considered. > > And one final thing: One of the reasons algebraic topologists are exicite= d=20 > about using and developing HoTT is that it gives a synthetic foundation t= o=20 > many "purely homotopical" ideas used in algebraic topology that have proo= fs=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 abou= t.=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 natu= re. > > 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 spectr= al=20 > sequences for cohomology have been developed in HoTT and formalised in th= e=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 t= o=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 characteristi= c=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_107_1326560379.1538096456010 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Many thanks for your comments which are very instructive.= =C2=A0=C2=A0 Actually I am trying to understand=C2=A0 anything in the Flori= s van Doorn's thesis, particularly the formalization in HoTT for the Atiyah-Hirzebruch spectral sequence=C2= =A0 and the=C2=A0 Leray-Serre spect= ral sequence.

On Thursday, September 27, 2018 at 7:38:09= PM UTC-5, Ali Caglayan wrote:
=
1. This could be possible = once a vector bundle has been fully defined. The idea behind characteristic= classes is to classify certain vector bundles with cohomology. This howeve= r may be a bit in the future as, for example, grassmannians have not yet be= en defined. Also orthogonal groups are not yet defined. So it is impossible= to say right now if this can be done but it seems likely.

2. Cohomology= in HoTT is not by default singular cohomology like in algebraic topology. = In HoTT we take the definition of cohomology to be the (truncated) set of m= aps to an Eilenberg-Maclane space. Concering cohomology operations, this sh= ould definitely be possible. Literature on cohomology has come out in the l= ast few years so expect more to be written about it.

3. Atiyah-Singer wou= ld need quite a lot of work, not to mention the fact it involves differenti= al structure. Which at the moment it is expected that differential cohesive= HoTT may be able to tackle such a theorem. HoTT on it's own is quite g= ood at talking about purely homotopical structure. This is an important poi= nt because many topological/manifoldy theorems are not necesserily homotopi= cal in nature. They may depend on extra structure that HoTT cannot really d= escribe adequately yet. Take for example Riemann-Roch which can be consider= ed a special case of Atiyah-Singer. It would need a good amount of algebrai= c geometry to be defined and/or proven in order to state the theorem. Which= is unliekly to come around in the next few years. This doesn't mean it= couldn't happen.

Just to show you how underdeveloped cohomology in H= oTT is at the moment, an "elementary" theorem of algebraic topolo= gy, the Hurewicz theorem, has not been proven yet. Though I believe it will= be tackled soon.

Types are not topological spaces, they are more litera= lly homotopy types. This is why I personally, found "the Hodge structu= re of a type" to be not within our current viewpoint although Steve Aw= odey's point about the speed of the development of HoTT has been consid= ered.

And one final thing: One of the reasons algebraic topologists a= re exicited about using and developing HoTT is that it gives a synthetic fo= undation to many "purely homotopical" ideas used in algebraic top= ology that have proofs and constructions relient on outside ideas or formal= isms. This isn't necesserily a bad thing (look at cobordisms in stable = homotopy) however some simpler areas of the subject should 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 t= o the ideas you are talking about. HoTT essentially provides a synthetic wa= y to reason about homotopy types, but it isn't an enlightening viewpoin= t for theorems not homotopic in nature.

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

Anywa= y if you have read this for congratulations.

Ali Caglayan

On Thu= rsday, 27 September 2018 14:10:09 UTC+1, Juan Ospina wrote:
Recently, there was a post a= bout the Euler characteristic of a type and other post about Hodge structur= e of a type.=C2=A0 Then my questions are:

1) It is= possible to construct characteristic classes=C2=A0 (Wu, Stiefel-Whitney, C= hern, 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 construct an Aityah-Singer index theorem for an arbitr= ary type (a type fibered with other type).

4) It i= s possible to construct integrality theores for the characteristic numbers = of an arbitrary fibered type?


Many = thanks.

Juan Ospina
Medell=C3=ADn,=C2=A0= Colombia


<= /blockquote>

--
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_107_1326560379.1538096456010-- ------=_Part_106_1655092086.1538096456010--