Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: general

Topic: Clowder Updates

Emily (she/her) (Nov 19 2024 at 14:37):

A new update on Clowder is live. You can see a general outline of the changes here.

Some of the more interesting additions:

• A section on internal Homs of powersets
• A section on a six-functor formalism for (power)sets
• A new chapter, Chapter 3: Monoidal Structures on the Category of Sets, in which a universal property for $(\mathsf{Sets},\times,\mathrm{pt})$ as the unique (in an appropriate sense) closed symmetric monoidal structure on $\mathsf{Sets}$ having $\mathrm{pt}$ as its monoidal unit is proven.

Tim Hosgood (Nov 19 2024 at 15:12):

• Began a complete overhaul of all proofs which read “Clear.” and the like. All proofs must now read either “Omitted” or be properly justified, no matter how “trivial” the details are.

this is a very much appreciated perspective!

Tim Hosgood (Nov 19 2024 at 15:13):

the six-functor formalism for sets is really interesting! i've not seen this before — did you have a reference for where you first saw this?

Jean-Baptiste Vienney (Nov 19 2024 at 15:17):

I guess she invented this herself ahah

Emily (she/her) (Nov 19 2024 at 15:37):

Tim Hosgood said:

the six-functor formalism for sets is really interesting! i've not seen this before — did you have a reference for where you first saw this?

I think there isn't a single reference (besides Clowder) collecting all such things in a single place. I saw some of the things in that section scattered around different places, e.g.:

• Beck–Chevalley for powersets is on nLab, https://ncatlab.org/nlab/show/Beck-Chevalley+condition#images_and_preimages
• The projection formula is on MO, https://mathoverflow.net/questions/67228/where-do-all-these-projection-formulas-come-from
• The adjoint triple $f_*\dashv f^{-1}\dashv f_!$ seems to be due to Lawvere, and is discussed on nLab (along with the projection formula and Beck–Chevalley) here: https://ncatlab.org/nlab/show/interactions+of+images+and+pre-images+with+unions+and+intersections.
• I've seen Internal Homs of powersets mentioned here: https://math.stackexchange.com/questions/267365/show-that-the-powerset-partial-order-is-a-cartesian-closed-category

That said, some of the things I wrote in that section were not previously written down as far as I'm aware (which doesn't mean much, I didn't really search the literature that much), like the second projection formula, strong closed monoidality of $f^{-1}$, the external tensor product and related formulas like $U\cap V=\Delta^{-1}_X(U\boxtimes_{X\times Y}V)$, or viewing $\emptyset$ as a dualizing object for $\mathcal{P}(X)$.

Jean-Baptiste Vienney (Nov 19 2024 at 15:58):

Is there a general definition of what is a six-functor formalism?

Tim Hosgood (Nov 19 2024 at 16:00):

Jean-Baptiste Vienney said:

Is there a general definition of what is a six-functor formalism?

there are many! it's a very busy topic of research at the moment

John Baez (Nov 19 2024 at 17:24):

This is great stuff, @Emily (she/her)! I think the way algebraic geometers discovered things like the "six functor formalism" and "projection formula" may have made them investigate the category of commutative rings (or its opposite, affine schemes) more thoroughly than the category of sets. So you're finding a neglected chest of jewels and displaying it to the world.

Kevin Carlson (Nov 19 2024 at 18:05):

I love the idea of a non-abelian six functor formalism!

Emily (she/her) (Nov 19 2024 at 18:06):

Jean-Baptiste Vienney said:

Is there a general definition of what is a six-functor formalism?

I think the closest to a general definition there's now is Mann (et al.)'s definition via $\infty$-categories of spans, developed here, here and here

Emily (she/her) (Nov 19 2024 at 18:06):

John Baez said:

This is great stuff, Emily (she/her)! I think the way algebraic geometers discovered things like the "six functor formalism" and "projection formula" may have made them investigate the category of commutative rings (or its opposite, affine schemes) more thoroughly than the category of sets. So you're finding a neglected chest of jewels and displaying it to the world.

Thanks, John!

Emily (she/her) (Nov 19 2024 at 18:06):

I've found lots of neglected stuff like this has been showing up as I try to systematically develop everything from scratch on Clowder (which is the main reason I've been doing so much basic stuff there)

Emily (she/her) (Nov 19 2024 at 18:06):

So far I've found stuff like a number of analogies between powersets and category of presheaves which hadn't been written down before (Item 2 here), new notions of tensor products leading to near-rings as categories of monoids (TBW), interesting 2-categorical properties of relations (Item 4 here), skew composition of relations (Item 5 here), new stuff on Isbell duality (TBW), notions of "cyclic co/ends" (TBW), new stuff on traces of categories (TBW), and the list goes on and on...

Emily (she/her) (Nov 19 2024 at 18:06):

It really ends up being super nice to write/develop things this way!

Mike Shulman (Nov 19 2024 at 18:14):

A lot of the "six functor formalism" makes sense in the context of an arbitrary indexed monoidal category (= monoidal fibration), particularly with cartesian base. In particular, I studied the external tensor product in this generality in my paper on Framed bicategories and monoidal fibrations.

The internal-hom of powersets in particular, with $\emptyset$ as a dualizing object, is well-known in constructive mathematics and topos theory, where powersets are in general a [[Heyting algebra]] rather than a Boolean algebra.

Emily (she/her) (Nov 19 2024 at 18:33):

Mike Shulman said:

A lot of the "six functor formalism" makes sense in the context of an arbitrary indexed monoidal category (= monoidal fibration), particularly with cartesian base. In particular, I studied the external tensor product in this generality in my paper on Framed bicategories and monoidal fibrations.

Oh, that's pretty cool!

Emily (she/her) (Nov 19 2024 at 23:32):

Emily (she/her) said:

So far I've found stuff like a number of analogies between powersets and category of presheaves which hadn't been written down before (Item 2 here), new notions of tensor products leading to near-rings as categories of monoids (TBW), interesting 2-categorical properties of relations (Item 4 here), skew composition of relations (Item 5 here), new stuff on Isbell duality (TBW), notions of "cyclic co/ends" (TBW), new stuff on traces of categories (TBW), and the list goes on and on...

By the way, another interesting thing that that came up while I was working on this specific update was this MO question, on algebras for the powerset intersection (oplax) monad.

Morgan Rogers (he/him) (Nov 20 2024 at 06:30):

Mike Shulman said:

The internal-hom of powersets in particular, with $\emptyset$ as a dualizing object, is well-known in constructive mathematics and topos theory, where powersets are in general a [[Heyting algebra]] rather than a Boolean algebra.

I second this: you're discovering (and making pleasingly explicit, I might add) a special case of "thin category theory": a lot of what you've discovered will work for posets, with the powerset replaced with the frame of downsets :D