7:00 AM
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

7:00 AM
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

7:01 AM
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

7:02 AM
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

yeah that's cool

7:03 AM
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

7:04 AM
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

7:05 AM
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

7:07 AM
is that a polynomial, jon

who put homotopy theory in my manga

homotopy pudding
you're welcome. for my art. and to my art.
it's a bat.

Why is Dorami afraid of cockroaches?

pinata
pinyata

7:09 AM
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
$\delta(B_4)=(-3 a4+ 2 a5) x^2 y z+ (3 a6 - 3 a4) x y^2 z + (3 a6 -2 a5) x y z^2$

baristacats

whoops
need some subscripts DAWG
@ERic i emailed neil strickland, but i will probably not hear back from him

7:11 AM
@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

7:13 AM
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

7:15 AM
i will not

god, crap, yeah this transcript is going to be saved
there goes my career....

what's jacob's representability criterion

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

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

7:16 AM
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

which is like half an hour advanced

7:17 AM
@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

8.1.4 this other document says

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

1 hour later…
8:31 AM
265 messages moved from Homotopy Theory
@WillJagy Fixed now. I merged the rooms

9:25 AM
hi there

8 hours later…
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.

cool, maybe it'll attract some attention

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

6:08 PM
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.

6:19 PM
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....

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"

6:24 PM
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?

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.

that's true. another idea is that we could do something like have discussions about particularly interesting unanswered questions on MO
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.

6:28 PM
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.

6:29 PM

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

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.

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

6:32 PM
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,

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

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.

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

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

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

6:39 PM
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

6:42 PM
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

6:45 PM
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

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

not any better than the HoTT book can

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

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?

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

6:53 PM
what is it

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

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.

hm ok

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

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

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

7:18 PM
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

7:19 PM
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 ??

7:21 PM
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.

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?

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

7:32 PM
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?

7:40 PM
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

7:49 PM
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

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

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

7:53 PM
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)$

7:57 PM
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

7:59 PM
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