last day (1969 days later) » 

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 ??
 
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
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
 
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
 
I hope Neil reads it
 
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.
@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.
 
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 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.
 
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 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
 
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,
 
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
 
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
 
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"
 
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?
 
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.....
 
6:53 PM
hmm I do not know about this result
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.
 
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?
 
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
 
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
 

  last day (1969 days later) »