Homotopy Theory

@ArnavTripathy: it's fairly weak, it's in the behrens-lawson manuscript in the same section where they describe infinitesimal deformations of p-divisible groups

Jon Beardsley

good-evening

Arnav Tripathy

ah

Eric

8.1.4 this other document says

Will

now we have to star every post before Jon gets back
although it would be better if we could remotely enable his desktop notifications for this

Arnav Tripathy

ok

ManishEarth

8:31 AM

← 265 messages moved from Homotopy Theory

@WillJagy Fixed now. I merged the rooms

Harry Gindi

9:25 AM

hi there

Will Jagy

5:29 PM

@ManishEarth, thanks. If I go from Main to Meta, I now see this on the right as one of two MO owned chatrooms.

@Eric, see your icon move in, I put a note on Google+ about this room. People were talking about a new HOTT book there, maybe a week ago.

Eric

cool, maybe it'll attract some attention

Will Jagy

Possibly. People are not looking to me for homotopy stuff.

Dominic Michaelis

6:08 PM

I think most people just waiting for some math to happen :D

Will Jagy

I'm guessing they will do mostly chitchat and schedule more serious discussions once a week.

Jon Beardsley

yeah so far it's mostly been just chillin

i mean, i'm certainly one that is happy to talk about math at any time, and start asking questions any time, but i think people already see enough of me on MO proper

I don't want to become pest, so to speak. i also gchat @Eric every day, lol

Will

then again you own this room

Jon Beardsley

i'm busy unstarring nonsense

Will Jagy

Hi, Jon. Some stuff was fixed overnight...I don't think it is even possible to have a pure subject discussion 24/7 in this environment, Main is better for beginning each focussed question. I like the idea from the Physics, guy, an attempt at a more serious discussion on a schedule. After a few eeks of that, you have something to advertise to senior people who would dislike pure chitchat.

Jon Beardsley

6:19 PM

yeah

Will Jagy

a few weeks of that.

Jon Beardsley

no i agree. i think it'd be good to have... i dunno, time every week that we have subject based discussion purely

the rest of the time this room can perhaps be a place for homotopy theorists, and associated crazies, to chat, or whatever

we could have mini-Talbot workshops, haha, where we discuss a specific topic. i dunno if it'd work or not

one idea is that I could send out e-mails and schedule experts, i.e. non-graduate-students, to be here for one hour, hosting a discussion on something

i don't know if this would work, or if it's even something i want to put that much effort into

however, "Owner of Mathoverflow Homotopy Theory Chat Room" is definitely going on my CV

;)

ManishEarth

@WillJagy yw :) Note, only the two recently used rooms will show up. Not more

Jon Beardsley

I guess I could ask some of the people that are somewhat active on MO, like Peter May, Charles Rezk, Jacob Lurie, Greg Stevenson, Tom Goodwillie, ummmmmm who else....

Will Jagy

Sounds good. Time zones play a part in scheduling.
SCheduled seminar discussions. Good. But do not lead those yourself, you have a thesis to do.
On the whole i would gusee that the age of participants will rise only gradually, on average. For the momnet, graduate students. The invited hosts is a really good idea. Get such people at least posting a "Hello World"

Jon Beardsley

6:24 PM

haha yeah

Will Jagy

Yes, already on MO, best to start that way.

Jon Beardsley

i think i will try to post a link to this on the algebraic topology email listserv

Evan Jenkins

Wouldn't G+ hangouts work better for that sort of thing?

Will Jagy

I know Peter May a little, he would not likley just chat, but host a chat seminar he certainly would.

Jon Beardsley

@EvanJenkins, I dunno I mean, I guess i've already got this thing up and going. plus you can do latex here. will chatJax work with latex?

Will Jagy

6:26 PM

I can't get G+ to work right for anything. This is more clearly linked to MO with the possibility of instantly posting a really juicy question on Main that may be figued out here.

Jon Beardsley

that's true. another idea is that we could do something like have discussions about particularly interesting unanswered questions on MO

and try to answer them

and perhaps create a user on MO called "Homotopy Chat Room" that answers questions communally!

Sean Tilson

Now it works!!

Success

Will Jagy

@JonBeardsley, the first thing you need is the room, the ability to advertise the room. You have that now. G+ has no Latex and will not impress the Peter May's of the world

Jon Beardsley

yeah. Peter will not be impressed

by a G+ chat room

Sean Tilson

I totally missed all the fun last night.

Jon Beardsley

6:28 PM

I don't think

yeah you did!!!

Sean Tilson

Are we doing a homotopy chat room to impress peter?

Jon Beardsley

sean's supposed to be writing a thesis, so this will provide a good distraction

well, not really, hahahah

we were thinking about having hosted topical discussions, with invited speakers, like Peter May, or Jacob, or someone like that

Evan Jenkins

I don't think Peter is going to be impressed.

Sean Tilson

I dunno how bob feels about it, but I feel good.

Evan Jenkins

I can tell him about it, though.

Jon Beardsley

6:29 PM

I mean hell, we could even start with grad students and postdocs

Sean Tilson

I have spent the whole day, almost, trying to get a copy of my passport notarized.

Eric

productive

Jon Beardsley

hahah, well, make it clear, we're not doing this to impress anyone. at least i'm not. but it would be really cool to talk to people who know things.

Will Jagy

Charles R is around, he had trouble with new MO account

Jon Beardsley

we could even start with @Seantilson doing a discussion on powwer ops, or @Eric doing a discussion on the determinental sphere

Sean Tilson

6:30 PM

I think the the way to get people who know things in here is to talk about math and start linking to discussions in here on the main site.

Jon Beardsley

that's true

Will

yeah and make sure we star the relevant discussions

Jon Beardsley

and people will be like "see so-and-so's comment in the homotopy chat room for a better explanation"

Sean Tilson

or even @Eric doing a discussion on power operations and @JonBeardsley doing a talk on the detrimental sphere!

Jon Beardsley

the sphere is detrimental to us all

power ops = power ups

Sean Tilson

6:32 PM

anyway, gotta go get a money order and go to fed ex.

Jon Beardsley

okay latez bro

Will Jagy

@Sean, part of the idea is that people doing dissertations do not lead the discussion or prepare as a seminar talk,

Jon Beardsley

glad you made it!!!

Sean Tilson

just wanted to see if my thing worked on here yet and say hello.

@WillJagy I think I am confused by your statement, can you clarify? did you mean "do not" for both?

Eric

i'd prefer to be invited to JHU or wherever to speak about the determinantal sphere :P

Jon Beardsley

6:34 PM

oh yeah, well, i'm working on that

i got sean invited

Let's be honest, the thing that really attracted me to mathematics was the social scene.

Sean Tilson

Did you now? @JonBeardsley thanks bro!

Jon Beardsley

Hahah, I mean, I dunno, Vitaly and I both

we are allowed to put in suggestsions

we were pushing hard for you and andrew

but andrew is too busy

Will Jagy

Jon, I starred your two (sub)-messages.
@Sean, right, Jon says he is doing a dissertation, and worries about the time involved leading this. My idea is that he organizes this, participates primarily as a student, and if a seminar type thing works out, he does not spend extra time leading on the mathematics. Just putting a face to the room,

@Sean, I starred Jon's two comments, look on the right

Arnav Tripathy

get this andrew salch guy on here

he has been a shadowy mysterious figure for far too long

Jon Beardsley

yeah, fricker salch. i think he doesn't want to get on MO

i try to get him to do all this stuff

Arnav Tripathy

6:39 PM

oh well ok then

ManishEarth

I see no homotopy theory being discussed here (but that's OK, it's your room!)

Or are you all homotopy theorists?

Jon Beardsley

but, i dunno, considering that andrew writes really long, thought out responses to my math questions that i email him, i suspect he might be concerned with spending way too much time on MO if he joined

i dunno, i'm a grad student. i'm trying to grow into an algebraic geometer, i think. or someone who lives in the phantom zone of mathematics

not that that is where AG'ers live, but that I kind of want to inhabit the interstices

Will Jagy

@Manish, except me. See starred messages on right. It seems scheduled serious discussions may be the way to go

ManishEarth

Yep. I think you guys should do it in the main room, but wait a bit for the dust to settle.

Jon Beardsley

oh, i'd also really like to get Mike Shulman in here to talk about HOTT, he's pretty active online

Arnav Tripathy

6:42 PM

what's the deal with hott

Jon Beardsley

i mean, proofs are paths bro

Arnav Tripathy

yeah so then what

Jon Beardsley

it's like

i dunno, in my mind, we can sort of think of a proof is being something like a path between two propositions in some space

i read a lot about it a while ago and have forgotten quite a bit of it

but it helps to have some familiarity with type theory, which i also read about and forgot

Arnav Tripathy

wait this is all ok but then what is the upshot

Will

I think the basis is that intensional Martin Löf type theory naturally leads to higher homotopy

just because you have identity types between identity types etc

Jon Beardsley

6:45 PM

right

Will

somehow it doesn't feel to me like it's a "revolutionary new idea", more like simply the proper context for talking about intensional type theory

Jon Beardsley

i agree

Will

but then I guess the other side of it is that univalence manages to capture a lot of the "theorems for free" aspect you have in programming languages

Jon Beardsley

i mean, when i first read about the Curry-Howard isomorphism years ago, it seemed to me like it should be done with homotopy theory

so Will, can you help me understand the univalence axiom

?

Arnav Tripathy

ok so like, what is the coolest thing that can or should come out of hott

Jon Beardsley

6:47 PM

like..... it says something like if $P\simeq Q$ then $P=Q$ or somethign???

Will

not any better than the HoTT book can

Jon Beardsley

haha yeah i downloaded that

Will

@Arnav I think it's just a good context for doing mathematics

Jon Beardsley

yeah, i mean, it's "foundations" haha

Will

I guess this is more an argument for type theory

but "let x be an integer" should really be an atomic statement, not "let x be a thing, and let this thing be an element of the thing of all things that are integers"

Jon Beardsley

6:48 PM

moreover, I think one hopes that the two disciplines will inform eachother in some way? homotopy theory could give some intuition to type theory that wasn't there before?

Arnav Tripathy

so if I do not already care about logic

should I also not care about hott

Will

but then people who know more about this than I do say that this is the natural language for doing stuff in infinity toposes

Jon Beardsley

right i mean, it's sort of a natural generalization. that is, we do logic in topoi, so.... what 's the internal logic of an $\infty$-topos? it should be HOTT right?

that seems like a really good question that's just interesting for its own sake, to me

Arnav Tripathy

ah ok

Jon Beardsley

also, any connection between logic/set theory and homotopy theory really gets me amped

because logic and set theory are so sort of..... ethereal and mystical and beautiful, but often seem to have difficulty being cared about

people say "why should i care whether or not such and such a large cardinal exists?" or whatever. so i was really excited by casacuberta et. al.'s result about Vopenka's principle and localizing subcategories. finally something you can see in non-foundational mathematics that seems to depend on large cardinal axioms

i got a badge for talking a lot in chat.....

Arnav Tripathy

6:53 PM

hmm I do not know about this result

what is it

Jon Beardsley

see Greg's answer here: mathoverflow.net/questions/88555/…

Arnav Tripathy

do you need a certain amount of rep to start a room

Jon Beardsley

i dunno

also, the theorem from nlab that i'm interested in is: Theorem. The VP implies the statement:

Let C be a left proper combinatorial model category and Z∈Mor(C) a class of morphisms. Then the left Bousfield localization LZW exists.

Arnav Tripathy

hm ok

Jon Beardsley

this seems like it should be true of course, but I guess it's not always

Jon Beardsley

7:09 PM

Does anyone know what is meant by "Waldhausen's unfolding"?

Jack Morava refers to this in one of his papers, I think it has something to do with going from $K(\mathbb{Z})$ to $K(\mathbb{S})$?

Arnav Tripathy

well you know what I wish people did more of

noncommutative topology

Jon Beardsley

what does that mean

Arnav Tripathy

I want there to be a realisation map from noncommutative geometry over some appropriate base to noncommutative topology

Jon Beardsley

hmmmmmmmm, well, i mean, endomorphism spaces are non-commutative

Arnav Tripathy

ironically, if you ask more generally just to some motivic noncommutative thing then that might already exist but it might also be a bit tautologous

hmm

so not in the sense of H-spaces with noncommutative multiplications or whatever

Jon Beardsley

7:18 PM

so, like, i dunno, i was thinking about this a while ago, looking at the homology of certain spectra of endomorphisms

Sean Tilson

@WillJagy Thank you for clarifying. I agree with you.

Arnav Tripathy

but in the sense that topological spaces are somehow commutative

like you can think of them as functions on some dude

and then you want to deform that to be noncommutative

apparently there is an approach (maybe even already decided to be the right approach ?) using C^* algebras or something of this sort

Jon Beardsley

well, i mean, how are you thinking of a space as a function on some dude?

Sean Tilson

@ArnavTripathy People do noncommutative topology.

Jon Beardsley

yes, there's C^* homotopy theory

Sean Tilson

7:19 PM

The typically call it .. yeah what @JonBeardsley said.

Jon Beardsley

and that's actually pretty interesting, i've wanted to look into that a little bit. Jack thinks that this spectrum $M\Xi$ might have something to do with noncommutative FGLS

and so, I've wondered if it could be like, the noncommutative version of $MU$ or something

Arnav Tripathy

yes sweet

tell me more

also

there are derived witt groups

man

Sean Tilson

But not exactly, in that people were doing what they call noncommutative topology before the model structures on C^* algebras were developed by Ostvaer, and Joachim-Johnson (whose work is different)

Jon Beardsley

(where $M\Xi$ is the Thom spectrum of $\Omega\Sigma \mathbb{C}P^\infty$ that Birgit Richter and others have studied)

Arnav Tripathy

what's the deal with that

sean ??

Sean Tilson

7:21 PM

Deal with what?

Jon Beardsley

derived Witt groups? I dunno.

Arnav Tripathy

yeah

Sean Tilson

I mean, people do it. There are roadblocks though. There are people doing awesome stuff too. I should mention that Tabuada and Dell'Ambrogio have work that is also related.

Dell'Ambrogio has his own stuff, and then there is joint work of his with Tabuada.

Arnav Tripathy

hm I guess I fundamentally don't understand why analysis needs to enter

analysis doesn't need to enter when we want to noncommutativise algebraic geometry

Sean Tilson

Anyway, I wanted to mention that such a thing was real.

Jon Beardsley

7:27 PM

Hey @seantilson remember the paper you referred me to by Alan Robinson in which he describes spectra as sheaves of pointed sets on "stabilized" finite polytopes?

Sean Tilson

arxiv.org/pdf/math/0702140.pdf

@JonBeardsley yeah

Jon Beardsley

any clue how that's connected to $\Gamma$-spaces?

I mean, $\Gamma$-spaces only gives us connective spectra right? but somehow the constructions are super similar

Sean Tilson

Sorry, I don't know

Jon Beardsley

oh alright, no worriez

sort of a random question

Sean Tilson

Also, @ArnavTripathy, Ostvaer's approach to C^* homotopy theory is to look at how motivic homotopy theory was developed, you might want to check it out.

Jon Beardsley

7:32 PM

Man, we got a lot of people in here! Cool!

Sean Tilson

@BerenSanders might be better at talking about some of this stuff.

yeah! @BerenSanders!

anyway, laters

byebye

so is there some kind of context in homotopy type theory

where when you create types for algebraic varieties

you actually get the correct homotopy type?

e.g. taking the solutions of polynomial equations in complex affine space

and the type of solutions is not just a type but is a higher inductive type with the right homotopical properties?

Jon Beardsley

7:40 PM

sounds like a question for a HOTT guy....

i haven't heard about creating types corresponding to algebraic varieties before

Will

well that's what you do for anything, right

if I have a system of polynomial equations I put them together into a type which encodes solving the system

Jon Beardsley

could you say more about that? I mean... i don't see it. pardon my ignorance.

though it sounds pretty cool

Will

I just mean the way you do set comprehension in type theory

$ \{ (x,y) \in \mathbb{R}^2 : x^2 + y^2 = 1 \} $ becomes $ \sum_{x,y : \mathbb{R}} (x^2 + y^2 =_{\mathbb{R}} 1) $ where the equality is itself a type and sum is a sum of types

just that the thing on the right there is like a disjoint union of individual points and has no homotopical information to it

Jon Beardsley

right. but.... hmmmmm... yeah i don't really understand most of type theory, beyond the few tag lines i've heard. so.... why do you need to sum over x,y?

anyway.... you don't have to explain this to me, hah, i certainly can't answer your question

i imagine there are people around that can, however

Will

$ x^2 + y^2 =_{\mathbb{R}} 1$ is itself a type, for any two real numbers x and y

and it is either inhabited or empty, what they call a "mere proposition" in the book

Jon Beardsley

7:49 PM

ah okay. sure.

Will

so then the set of solutions is just adding up all those types

Jon Beardsley

i see. all essentially all inhabitants

Will

kind of a silly way to write the circle as a disjoint union of its points

Jon Beardsley

hmmmmmmmm sure

now, i mean, when we say that the type is inhabited... each inhabitant, in HOTT, is supposed to be a point in the space corresponding to that type right?

Will

yes

Jon Beardsley

7:51 PM

so in this case, it's this space of pairs satisfying the equation

okay

and you're okay summing over ALL of $\mathbb{R}^2$ since the pairs that don't satisfy it don't "add points" to your space

in somse sense

cool

Will

yes

Jon Beardsley