Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Euler characteristic of a type
@ 2018-09-17 19:11 Ali Caglayan
  2018-09-17 22:36 ` Floris van Doorn
  0 siblings, 1 reply; 9+ messages in thread
From: Ali Caglayan @ 2018-09-17 19:11 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 1243 bytes --]

We currently have enough machinary to (kind of) define Betti numbers (for 
homology see Floris van Doorn's thesis 
<http://florisvandoorn.com/papers/dissertation.pdf>). I am confident that 
soon we can start compting Betti numbers of some types. This would allow us 
to define the euler characterstic E : U --> N of a type. If classical 
algebraic topology tells us anything this will satisfy a lot of neat 
identities.

In fact consider U as a semiring with + and * as the operations. E is a 
semiring homomorphism to N (the initial semiring (is this relavent?)). In 
other words we should have

E(X + Y) = E(X) + E(Y)
E(X * Y) = E(X)  E(Y)

and even maybe, subject to some conditions, a given type family P : X --> U 
would satisfy E( (x : X) * P(x) ) = E(X) * E(P(x_0))

This would be a cool invariant to have. Unfortunately as it stands, 
homology is a bit unwieldy. Perhaps rationalising spaces would help?

Any thoughts or suggestions?

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

[-- Attachment #1.2: Type: text/html, Size: 1577 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread

* Re: [HoTT] Euler characteristic of a type
  2018-09-17 19:11 [HoTT] Euler characteristic of a type Ali Caglayan
@ 2018-09-17 22:36 ` Floris van Doorn
  2018-09-17 23:07   ` Ali Caglayan
  0 siblings, 1 reply; 9+ messages in thread
From: Floris van Doorn @ 2018-09-17 22:36 UTC (permalink / raw)
  To: Ali Caglayan; +Cc: Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 1993 bytes --]

Clearly we cannot define E on the whole universe, but only on a
subuniverse.
For example, we could define it on the subuniverse of types with finitely
generated homology groups. For the Euler characteristic we will also need
that the betti numbers are eventually 0. Other than that, I agree that
these properties should hold in HoTT.

On Mon, 17 Sep 2018 at 21:11, Ali Caglayan <alizter@gmail.com> wrote:

> We currently have enough machinary to (kind of) define Betti numbers (for
> homology see Floris van Doorn's thesis
> <http://florisvandoorn.com/papers/dissertation.pdf>). I am confident that
> soon we can start compting Betti numbers of some types. This would allow us
> to define the euler characterstic E : U --> N of a type. If classical
> algebraic topology tells us anything this will satisfy a lot of neat
> identities.
>
> In fact consider U as a semiring with + and * as the operations. E is a
> semiring homomorphism to N (the initial semiring (is this relavent?)). In
> other words we should have
>
> E(X + Y) = E(X) + E(Y)
> E(X * Y) = E(X)  E(Y)
>
> and even maybe, subject to some conditions, a given type family P : X -->
> U would satisfy E( (x : X) * P(x) ) = E(X) * E(P(x_0))
>
> This would be a cool invariant to have. Unfortunately as it stands,
> homology is a bit unwieldy. Perhaps rationalising spaces would help?
>
> Any thoughts or suggestions?
>
> --
> 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.

[-- Attachment #2: Type: text/html, Size: 2743 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread

* Re: [HoTT] Euler characteristic of a type
  2018-09-17 22:36 ` Floris van Doorn
@ 2018-09-17 23:07   ` Ali Caglayan
  2018-09-18  6:25     ` Michael Shulman
  0 siblings, 1 reply; 9+ messages in thread
From: Ali Caglayan @ 2018-09-17 23:07 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 787 bytes --]

This would be some subuniverse of "compact" spaces I assume.

On Monday, 17 September 2018 23:37:03 UTC+1, Floris van Doorn wrote:
>
> Clearly we cannot define E on the whole universe, but only on a 
> subuniverse. 
> For example, we could define it on the subuniverse of types with finitely 
> generated homology groups. For the Euler characteristic we will also need 
> that the betti numbers are eventually 0. Other than that, I agree that 
> these properties should hold in HoTT.
>

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

[-- Attachment #1.2: Type: text/html, Size: 1136 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread

* Re: [HoTT] Euler characteristic of a type
  2018-09-17 23:07   ` Ali Caglayan
@ 2018-09-18  6:25     ` Michael Shulman
  2018-09-18 10:54       ` Ali Caglayan
  0 siblings, 1 reply; 9+ messages in thread
From: Michael Shulman @ 2018-09-18  6:25 UTC (permalink / raw)
  To: Ali Caglayan; +Cc: HomotopyTypeTheory

A more "homotopical" way to define the Euler characteristic is as the
trace of an identity map of a suspension spectrum in the symmetric
monoidal category of spectra.  It also generalizes to a definition of
the Lefschetz number, and many of the formal properties of Euler
characteristic follow formally from this definition and the properties
of trace.  I suspect this would also be a useful version of the
definition in HoTT, although of course there are currently technical
obstacles to working with such things as the symmetric monoidal smash
product of spectra.
On Mon, Sep 17, 2018 at 4:07 PM Ali Caglayan <alizter@gmail.com> wrote:
>
> This would be some subuniverse of "compact" spaces I assume.
>
> On Monday, 17 September 2018 23:37:03 UTC+1, Floris van Doorn wrote:
>>
>> Clearly we cannot define E on the whole universe, but only on a subuniverse.
>> For example, we could define it on the subuniverse of types with finitely generated homology groups. For the Euler characteristic we will also need that the betti numbers are eventually 0. Other than that, I agree that these properties should hold in HoTT.
>
> --
> 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.

^ permalink raw reply	[flat|nested] 9+ messages in thread

* Re: [HoTT] Euler characteristic of a type
  2018-09-18  6:25     ` Michael Shulman
@ 2018-09-18 10:54       ` Ali Caglayan
  2018-09-18 16:13         ` Michael Shulman
  0 siblings, 1 reply; 9+ messages in thread
From: Ali Caglayan @ 2018-09-18 10:54 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 1142 bytes --]

This is a nice idea. If we could somehow overcome the lack of coherance of 
smashes how would we go about defining the trace of an object in a 
symmetric monoidal category? 

On Tuesday, 18 September 2018 07:26:04 UTC+1, Michael Shulman wrote:
>
> A more "homotopical" way to define the Euler characteristic is as the 
> trace of an identity map of a suspension spectrum in the symmetric 
> monoidal category of spectra.  It also generalizes to a definition of 
> the Lefschetz number, and many of the formal properties of Euler 
> characteristic follow formally from this definition and the properties 
> of trace.  I suspect this would also be a useful version of the 
> definition in HoTT, although of course there are currently technical 
> obstacles to working with such things as the symmetric monoidal smash 
> product of spectra. 
>

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

[-- Attachment #1.2: Type: text/html, Size: 1493 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread

* Re: [HoTT] Euler characteristic of a type
  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
  0 siblings, 2 replies; 9+ messages in thread
From: Michael Shulman @ 2018-09-18 16:13 UTC (permalink / raw)
  To: Ali Caglayan; +Cc: HomotopyTypeTheory

Some introductions are:
https://ncatlab.org/nlab/show/trace
https://arxiv.org/abs/1107.6032
On Tue, Sep 18, 2018 at 3:54 AM Ali Caglayan <alizter@gmail.com> wrote:
>
> This is a nice idea. If we could somehow overcome the lack of coherance of smashes how would we go about defining the trace of an object in a symmetric monoidal category?
>
> On Tuesday, 18 September 2018 07:26:04 UTC+1, Michael Shulman wrote:
>>
>> A more "homotopical" way to define the Euler characteristic is as the
>> trace of an identity map of a suspension spectrum in the symmetric
>> monoidal category of spectra.  It also generalizes to a definition of
>> the Lefschetz number, and many of the formal properties of Euler
>> characteristic follow formally from this definition and the properties
>> of trace.  I suspect this would also be a useful version of the
>> definition in HoTT, although of course there are currently technical
>> obstacles to working with such things as the symmetric monoidal smash
>> product of spectra.
>
> --
> 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.

^ permalink raw reply	[flat|nested] 9+ messages in thread

* Re: [HoTT] Euler characteristic of a type
  2018-09-18 16:13         ` Michael Shulman
@ 2018-09-18 19:11           ` Ali Caglayan
  2018-09-19  0:04           ` Ali Caglayan
  1 sibling, 0 replies; 9+ messages in thread
From: Ali Caglayan @ 2018-09-18 19:11 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 530 bytes --]

Thank you for the paper Mike, it is very cool indeed!

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.

[-- Attachment #1.2: Type: text/html, Size: 1790 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread

* Re: [HoTT] Euler characteristic of a type
  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
  1 sibling, 1 reply; 9+ messages in thread
From: Ali Caglayan @ 2018-09-19  0:04 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 1217 bytes --]

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.

[-- Attachment #1.2: Type: text/html, Size: 2623 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread

* Re: [HoTT] Euler characteristic of a type
  2018-09-19  0:04           ` Ali Caglayan
@ 2018-09-19  3:52             ` Michael Shulman
  0 siblings, 0 replies; 9+ messages in thread
From: Michael Shulman @ 2018-09-19  3:52 UTC (permalink / raw)
  To: Ali Caglayan; +Cc: HomotopyTypeTheory

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.

^ permalink raw reply	[flat|nested] 9+ messages in thread

end of thread, other threads:[~2018-09-19  3:52 UTC | newest]

Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-09-17 19:11 [HoTT] Euler characteristic of a type 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 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).