@AaronMazel-Gee following numdam.org/article/CTGDC_2002__43_3_221_0.pdf I think that if you want to talk about PROPs and so forth, you probably want to put a sort of double category structure on Fin_* and then have a "Mackey functor straightening/unstraightening" type of thing

I.e. a commutative and cocommutative bialgebra in a category should be a Mackey functor out of a suitable double category structure on Fin_*, and you want to codify this as a double category structure on C^⊗ which plays well with the double category structure on Fin_* so that sections of whatever this weird map C^⊗→Fin_* is are precisely Mackey functors Fin_*→C^⊗

Oh I guess to make it fit with modern usage I should say "pre-Mackey functor"

@JonathanBeardsley right, this is encoding the compatibility between multiplication and comultiplication. nice find! i think your types are slightly off, though: it looks like the new prop (i'm going to stop yelling that word), which is just spans, is such that symmetric monoidal functors out of it are equivalent to mackey functors out of the original prop. e.g. a bicommutative bialgebra is a mackey functor on $Fin_*$.

is anybody aware of a summary of basic lie algebra theory in categorical terms? i'd like to organize the words nilpotent, solvable, semisimple, simple, reductive, etc. for instance, it seems like there is something like a recollement of the form:

{solvable lie algebras} <--> {lie algebras} <--> {semisimple lie algebras}

@AaronMazel-Gee well a bicommutative bialgebra is a mackey functor out of Fin, not Fin_*, I think

@JonathanBeardsley right, my mistake

the corresponding operad to $(Fin,\sqcup)$ is $Fin_{**}$, so that's what we'd need to upgrade ("spanify")

in re Lie algebras above, we have the (noncanonically split) short exact sequence $rad(g) \hookrightarrow g \twoheadrightarrow g_{ss}$

and there are no hom's from semisimples to solvables

similarly, reductives turn out to always split as a product abelian x semisimple; this is like a sub-recollement, with some additional categorical feature

to be clear, i don't think it's quite a recollement (depending on one's definition) -- i don't think there are six functors around, anyways

Isn't a prop just a symmetric monoidal infinity-category whose underlying symmetric monoidal infinity-groupoid is free? E.g. the prop corresponding to an infty-operad is its symmetric monoidal envelope.

@RuneHaugseng yeah but since there isn't, say, a bialgebra ∞-operad, I think maybe the general case requires a bit of care

But yeah I mean, the bialgebra prop should be "the free monoidal ∞-category containing a bialgebra"

Sure, not every such object arises from an operad

It would also be interesting, it seems to me, to be able to define all of this in terms of some kind of data in C^\otimes and its dual simultaneously

What is C?

@RuneHaugseng yeah I think it might be cool to do it the way Lack does with distributive laws for monads too, since that might more obviously generalize