Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] The Hodge structure of a type
@ 2018-09-22 16:58 José Manuel Rodriguez Caballero
  2018-09-22 23:43 ` Ali Caglayan
  2018-09-24 22:30 ` Ali Caglayan
  0 siblings, 2 replies; 5+ messages in thread
From: José Manuel Rodriguez Caballero @ 2018-09-22 16:58 UTC (permalink / raw)
  To: HomotopyTypeTheory

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

Recently, there was a post about the Euler characteristic of a type. In my
case, I am interested in the Hodge structure of the Hilbert scheme of n
points on a 2-dimensional torus. Does such a topological construction make
sense in HoTT for an arbitrary type, under some general hypothesis?

Kind Regards,
Jose M

References about the topological structure that I am studying:
https://www.sciencedirect.com/science/article/pii/S0001870812004008

-- 
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: 1097 bytes --]

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

* Re: [HoTT] The Hodge structure of a type
  2018-09-22 16:58 [HoTT] The Hodge structure of a type José Manuel Rodriguez Caballero
@ 2018-09-22 23:43 ` Ali Caglayan
  2018-09-24 22:30 ` Ali Caglayan
  1 sibling, 0 replies; 5+ messages in thread
From: Ali Caglayan @ 2018-09-22 23:43 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I don't think HoTT is any position to be used in algebraic geometry as it 
stands currently. There may be a way in via a functor of points approach 
which is well suited for constructing Hilbert schemes. However I think it 
would be impossible to say anything concrete at this point. Homology and 
cohomology are usually seen as "easy" invariants about spaces to calculate 
however in HoTT it is all very new and nobody quite know the best way to go 
about reasoning with these things. Let alone thinking about something with 
extra structure like Hodge structure.

However representation theory, as you have cited, may be more tractable. 
There are good formal properties of HoTT which may allow it to reason in 
representation theoretic terms quite concretely. So if you are interested 
in studying quiver varieties you may just be able to get away with studying 
quiver representations. However this is all speculative at this point. I 
don't think there are any researchers looking into any of these things yet 
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 
otherwise.

On Saturday, 22 September 2018 17:59:03 UTC+1, José Manuel Rodriguez 
Caballero wrote:
>
> Recently, there was a post about the Euler characteristic of a type. In my 
> case, I am interested in the Hodge structure of the Hilbert scheme of n 
> points on a 2-dimensional torus. Does such a topological construction make 
> sense in HoTT for an arbitrary type, under some general hypothesis?
>
> Kind Regards,
> Jose M
>
> References about the topological structure that I am studying: 
> https://www.sciencedirect.com/science/article/pii/S0001870812004008
>

-- 
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: 3063 bytes --]

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

* Re: [HoTT] The Hodge structure of a type
  2018-09-22 16:58 [HoTT] The Hodge structure of a type José Manuel Rodriguez Caballero
  2018-09-22 23:43 ` Ali Caglayan
@ 2018-09-24 22:30 ` Ali Caglayan
  2018-09-24 23:59   ` Steve Awodey
  1 sibling, 1 reply; 5+ messages in thread
From: Ali Caglayan @ 2018-09-24 22:30 UTC (permalink / raw)
  To: Homotopy Type Theory


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

However I don't want to discourage you. One possible solution is 
(differential?) cohesive homotopy type theory (which is at the moment even 
more undeveloped). This may allow you to talk about manifolds and their 
structure "synthetically" which would allow for definitions of de Rham 
cohomology and possibly with care allow you to talk about hilbert schemes 
of some torus. Pessemistically I would add that it would be at least 10 
years before any of this is considered.

-- 
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: 974 bytes --]

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

* Re: [HoTT] The Hodge structure of a type
  2018-09-24 22:30 ` Ali Caglayan
@ 2018-09-24 23:59   ` Steve Awodey
  2018-09-25  8:59     ` José Manuel Rodriguez Caballero
  0 siblings, 1 reply; 5+ messages in thread
From: Steve Awodey @ 2018-09-24 23:59 UTC (permalink / raw)
  To: Ali Caglayan; +Cc: Homotopy Type Theory

> On Sep 24, 2018, at 6:30 PM, Ali Caglayan <alizter@gmail.com> wrote:
> 
> However I don't want to discourage you. One possible solution is (differential?) cohesive homotopy type theory (which is at the moment even more undeveloped). This may allow you to talk about manifolds and their structure "synthetically" which would allow for definitions of de Rham cohomology and possibly with care allow you to talk about hilbert schemes of some torus. Pessemistically I would add that it would be at least 10 years before any of this is considered.

just for perspective:

- 10 years ago we had the (higher) homotopy group(oid)s, and not much more.
- 5 years ago the HoTT book was just finished.
- 1 year ago the Serre spectral sequence was finished.

things are moving pretty fast - I would not be so pessimistic.

Steve

-- 
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] 5+ messages in thread

* Re: [HoTT] The Hodge structure of a type
  2018-09-24 23:59   ` Steve Awodey
@ 2018-09-25  8:59     ` José Manuel Rodriguez Caballero
  0 siblings, 0 replies; 5+ messages in thread
From: José Manuel Rodriguez Caballero @ 2018-09-25  8:59 UTC (permalink / raw)
  To: HomotopyTypeTheory

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

>
> Michael Shulman wrote:
>
what "algebraic" information it uses as input.


In the case of the Hilbert scheme of n points on X, the information comes
from the n-th symmetric power of X: https://arxiv.org/pdf/math/0304302.pdf

So, the input are X as an infinite-groupoid and the natural number n. The
output is the Hilbert scheme of n points on X as an infinite groupoid. I do
not know if there is some nice functoriality in this process which could be
expressed in HoTT in a natural way.  There are more results about the
Hilbert schemes it in Goettsche's homepage: http://users.ictp.it/~gottsche/

Kind Regards,
José M.


El lun., 24 sept. 2018 a las 19:59, Steve Awodey (<awodey@cmu.edu>)
escribió:

> > On Sep 24, 2018, at 6:30 PM, Ali Caglayan <alizter@gmail.com> wrote:
> >
> > However I don't want to discourage you. One possible solution is
> (differential?) cohesive homotopy type theory (which is at the moment even
> more undeveloped). This may allow you to talk about manifolds and their
> structure "synthetically" which would allow for definitions of de Rham
> cohomology and possibly with care allow you to talk about hilbert schemes
> of some torus. Pessemistically I would add that it would be at least 10
> years before any of this is considered.
>
> just for perspective:
>
> - 10 years ago we had the (higher) homotopy group(oid)s, and not much more.
> - 5 years ago the HoTT book was just finished.
> - 1 year ago the Serre spectral sequence was finished.
>
> things are moving pretty fast - I would not be so pessimistic.
>
> Steve
>
> --
> 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: 3424 bytes --]

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

end of thread, other threads:[~2018-09-25  8:59 UTC | newest]

Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-09-22 16:58 [HoTT] The Hodge structure of a type José Manuel Rodriguez Caballero
2018-09-22 23:43 ` Ali Caglayan
2018-09-24 22:30 ` Ali Caglayan
2018-09-24 23:59   ` Steve Awodey
2018-09-25  8:59     ` José Manuel Rodriguez Caballero

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