guys here's a quote about eggplant "You can eat eggplant every day, in season at least, and all it’s going to do is make you happy,"

ain't errbody even know about TAF

who starred that

oh wait apparently skullpatrol's thing is posting darth vader pics in general

who wants to know

not me

that is so sweet

i have to give a talk on friday

though i think it is star-worthy

I know, you can't star your own posts

on eggplant ?

ya

that's nonsense

UNSTARRED

bazinga

okay that's out of control

you can unstar ??

guys

i can kill that stuff

let's not get out of control here

please calm down, i was just trying to bring some eggplant chat to the table

@JonBeardsley sweet check this out

YOU CAN PERFORM THIS ACTION AGAIN IN 1 SECONDS

WTF this is so irritating

check what out

I replied to one of your earlier chats

hover over the arrow

oh i see

bam

yeah that's cool

now you know

um, so, should i just kick will out then?

what why

this is pretty unpleasant

he's starring the shit out of everything

oh no that's me

I can stop

hahahhaa

I was just trying out buttons

thanks Jon

I used to trust you

i thought it was him, because he posted "you can perform this action again in 1 seconds"

i.e. starring wildly

well, at least now we know, if we need to go to a chat room and irritate people

that's how to do it. you can't chat furiously, but you can star furiously

I'm not even sure why you find it so irritating

i don't either

jon hates stars

antiaster

lol

just set some polynomials equal to eachother alright

frick

whoa there's also an eric in the anime+manga room

how will we tell them apart

probably it's EP

oh nice

who put manga in my homotopy theory

is that a polynomial, jon

who put homotopy theory in my manga

homotopy pudding

that's some art i made

you're welcome. for my art. and to my art.

it's a bat.

Why is Dorami afraid of cockroaches?

pinata

pinyata

math.berkeley.edu/~ericp/latex/msri-2013.pdf notes without a punchline :(

the aristocrats

oho I have determined that it is not the same eric

aristocats

baristacats

whoops

need some subscripts DAWG

@ERic i emailed neil strickland, but i will probably not hear back from him

@ERic

regarding the cofiber of $X(n)\to X(n+1)$

erm

i think the most of a reply i've ever gotten from neil is "that's neat. i might read it someday."

fiber

yeah

callan said he probably won't respond. so, oh well.

and my e-mail was pretty.... i dunno... possibly confusing

as i am wont to be

you gotta be kidding me with these chat speed restrictions. i type fast as hecke. i need to send more frequently

now you can tell him you are the room master

that will impress him

that's true

yeah is it like once we get enough rep we can get around these restrictions

or what is the deal here

yeah, if he sees me up here, managing this room with aplomb, he will probably like me a lot

you might have heard of me from that MO chatroom, it's kind of a big deal

yeah, i kind of like, convinced someone else to start it, i dunno if you know about that

funny story actually

Jon "aplomb chat management" Beardsley

ACM, if you will

i will not

god, crap, yeah this transcript is going to be saved

there goes my career....

what's jacob's representability criterion

I hope Neil reads it

well, he requires that you have passed the BAR at least

commence grovelling in 3... 2... 1...

lawl

okay, my future-wife (whoa, is she a wife from the future???) is telling me it's time to go to bed

it's almost 4am here

what no

it's like 3:17

okay Arnav, that's enough.

is johns hopkins in its own time zone

yes

which is like half an hour advanced

@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

good-evening

ah

8.1.4 this other document says

ok

← 265 messages moved from Homotopy Theory

@WillJagy Fixed now. I merged the rooms

hi there

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

cool, maybe it'll attract some attention

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

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

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

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

then again you own this room

i'm busy unstarring nonsense

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.

yeah

a few weeks of that.

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

;)

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

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

haha yeah

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

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

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

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

@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?

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.

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!

Now it works!!

Success

@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

yeah. Peter will not be impressed

by a G+ chat room

I totally missed all the fun last night.

I don't think

yeah you did!!!

Are we doing a homotopy chat room to impress peter?

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

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

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

I can tell him about it, though.

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

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

productive

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.

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

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

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.

that's true

yeah and make sure we star the relevant discussions

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

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

the sphere is detrimental to us all

power ops = power ups

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

okay latez bro

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

glad you made it!!!

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?

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

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.

Did you now? @JonBeardsley thanks bro!

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

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

get this andrew salch guy on here

he has been a shadowy mysterious figure for far too long

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

i try to get him to do all this stuff

oh well ok then

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

Or are you all homotopy theorists?

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

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

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

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

what's the deal with hott

i mean, proofs are paths bro

yeah so then what

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

wait this is all ok but then what is the upshot

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

right

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

i agree

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

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

?

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

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

not any better than the HoTT book can

haha yeah i downloaded that

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

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

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"

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?

so if I do not already care about logic

should I also not care about hott

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

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

ah ok

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

hmm I do not know about this result

what is it

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

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

i dunno

hm ok

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

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})$?

well you know what I wish people did more of

noncommutative topology

what does that mean

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

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

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

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

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

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

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

@ArnavTripathy People do noncommutative topology.

yes, there's C^* homotopy theory

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

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

yes sweet

tell me more

also

there are derived witt groups

man

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)

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

what's the deal with that

sean ??

Deal with what?

derived Witt groups? I dunno.

yeah

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.

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

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

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?

arxiv.org/pdf/math/0702140.pdf

@JonBeardsley yeah

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

Sorry, I don't know

oh alright, no worriez

sort of a random question

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.

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

@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?

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

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

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

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

though it sounds pretty cool

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

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

$ 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

ah okay. sure.

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

i see. all essentially all inhabitants

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

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?

yes

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

yes

right, soooooo i see, you're interested now in the homotopy type of this space

yes, because obviously the circle as a topological space is not the disjoint union of its points

haha yeah

chouette

en effet

so then in homotopy type theory, well as you said types are spaces

yeah..... so to some equations we can make a space

so you have a type which is actually the circle

with the correct homotopical information

and in the type theory well it's kind of like CW complexes

yeah

it's the type generated by a point and a loop

hmmmmmmm. what types do those correspond to?

i mean, not a loop right? but an interval, with something corresponding to an "attaching map"?

well it's the type generated by a point $ P : S^1$

and by a loop $loop : (P =_{S^1} P)$

so.... here, that $S^1$ doesn't have a meaning, exactly, i mean, to start with

you're sort of saying.... here's a type called $S^1$

yes

okay

yeah, and an "identity type" between P and P

which is inhabited

yes

but so then, is all this happening in some ambient space

it doesn't jibe with me, drawing loops in places that there's nothing to draw it on

well no that's a big part of type theory

hmmmmmm, okay, i'll accept that, haha

it that sense it's similar to when you do ECTS

you can't just take the union of any two sets in ECTS, that makes no sense