@IanColey I'm having a jolly time watching it sit at the bottom of my to-do list while I deal with about a million other things.

A question for the motivic crowd: Is the category of smooth schemes of finite type over a finite-dimensional noetherian base scheme skeletally small? (I don't think it is but thought it best to ask before I give up hope on what I wanted to do.)

@NiallTaggart: This just means essentially small, right? Then the answer is yes. (Reduce to finite type affine schemes over an affine scheme, and observe that by definition those are specified by a countable amount of data.)

@TomBachmann ah yes of course, thanks!

@IanColey not really! unless by "jolly" you mean "omfg this is one of the worst parts of being a mathematician"?

in may's "concise course" treatment of groupoid van kampen (math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf page 17 (or p25 of the pdf)), it seems that the proof doesn't use connectedness at all. am i missing something? (i'd like to apply this to a cover of $S^1$ by two connected opens, but their intersection won't be connected. of course, certainly the conclusion is still true.)

@LiamKeenan cool, that sounds reasonable. looking back, i see that this is in sam raskin's recent treatment of the DGM theorem (1807.06709) -- perhaps that's even where you got it

@AaronMazel-Gee No, it's fine. Groupoid van Kampen has no connectedness hypothesis and the application you want is the standard example. Beware of computing the pushout in groupoids properly though.

By the way I like the presentation of that theorem in tom Dieck's Algebraic Topology (although it really would need homotopy colimits to do it properly)

@DenisNardin awesome, thanks for the the confirmation. what do you mean by your warning? (note that May looks at strict colimits of groupoids. i think in the background here is the canonical model structure on Cat (or Gpd), and the fact that for inclusions of topological spaces the map on $\Pi_1$ is a cofibration (injective on objects).)

@AaronMazel-Gee I just meant that computing the pushout in groupoids (or more generally in cats) is not the easiest thing to do -- after all this is where the Z comes from! And yeah, I know that May (as tom Dieck) uses the strict pushout, which makes it a bit awkward when you want to, e.g., replace the groupoid with an equivalent one..

gotcha. of course this is for my algtop class, and i think i will just make an unproved assertion about replacing the diagram by an equivalent one (keeping its morphisms cofibrations).