Re: [HoTT] The Hodge structure of a type

[Ali Caglayan <alizter@gmail.com>]

[-- 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 --]