Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Michael Shulman <shulman@sandiego.edu>
To: Ali Caglayan <alizter@gmail.com>
Cc: "HomotopyTypeTheory@googlegroups.com"
	<HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Euler characteristic of a type
Date: Tue, 18 Sep 2018 20:52:39 -0700	[thread overview]
Message-ID: <CAOvivQzc+QRHWT3M1+Y=tRat_QJWx++Hg_EEizOYorj1SD_UQA@mail.gmail.com> (raw)
In-Reply-To: <1ce7df52-a67e-4d52-9acd-962a869562d4@googlegroups.com>

From an abstract homotopical point of view, the "finite types", i.e.
those that have Euler characteristics, are *by definition* those whose
suspension spectrum is dualizable.  The dual object is then just part
of the definition of "dualizable".  Formal arguments applicable to any
symmetric monoidal stable homotopy theory (e.g. (oo,1)-category or
derivator, but which would have to be formalized differently in HoTT)
should imply that such dualizable objects are closed under finite
colimits, hence include all "finite cell complexes" represented as
HITs.  The dual in such a case is constructed formally as a
corresponding limit of duals (since dualization is a contravariant
equivalence on the dualizable objects).

The business of stable normal bundles and Thom spectra is how one
shows that the oo-groupoid presented by a manifold has this formal
dualizability property.  Book HoTT has no known way to go from a
point-set-topological object, like a manifold, to a type (i.e.
synthetic oo-groupoid) that it presents.  It may be possible in a
two-level type theory to construct the "fundamental oo-groupoid" of a
point-set-level space internally as a semisimplicial type and then
take its "realization" to get a single type.  Alternatively, Cohesive
HoTT provides an abstract context in which to talk about
point-set-level spaces "synthetically" in parallel to homotopy-level
spaces, where this presentation operation is represented by the
"shape" modality.  In either of these contexts, one could attempt to
prove, using some analogue of Thom spectra of normal bundles, that the
"shape" of a manifold is a dualizable type.

It may also be possible to study in Book HoTT something with the
"homotopical content" of a vector bundle, e.g. a corresponding
cohomology class regarded as a map into some classifying space, as in
the work of Rijke and Buchholtz on projective spaces.  I don't know
whether this would be helpful for dualizability, however.

On Tue, Sep 18, 2018 at 5:04 PM Ali Caglayan <alizter@gmail.com> wrote:
>
> So I have been reading your exposition and it seems to me the following things will need to be done in order to define the euler characteristic:
>
>  1. Sort out the symmetric monoidal structure on the category of Spectra.
>      - The main obstacle is the cohereance of the smash product (for spectra this follows from spaces I believe?).
>  2. Define the suspension spectrum of a space
>      - This should be simple to define as a prespectrum which can be spectrified.
>  3. Define the "stable normal bundle" of a space
>     - Isn't this something usually done on a manifold?
>  4. Define the Thom spectrum of a vector bundle
>     - I have no idea what this is but I hope it can be defined. I have no idea what a vector bundle in HoTT is however.
>
>
>
> On Tuesday, 18 September 2018 17:13:26 UTC+1, Michael Shulman wrote:
>>
>> Some introductions are:
>> https://ncatlab.org/nlab/show/trace
>> https://arxiv.org/abs/1107.6032
>
> --
> 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.

      reply	other threads:[~2018-09-19  3:52 UTC|newest]

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-09-17 19:11 Ali Caglayan
2018-09-17 22:36 ` Floris van Doorn
2018-09-17 23:07   ` Ali Caglayan
2018-09-18  6:25     ` Michael Shulman
2018-09-18 10:54       ` Ali Caglayan
2018-09-18 16:13         ` Michael Shulman
2018-09-18 19:11           ` Ali Caglayan
2018-09-19  0:04           ` Ali Caglayan
2018-09-19  3:52             ` Michael Shulman [this message]

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAOvivQzc+QRHWT3M1+Y=tRat_QJWx++Hg_EEizOYorj1SD_UQA@mail.gmail.com' \
    --to=shulman@sandiego.edu \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=alizter@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).