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: learning: questions

Topic: [0, 1] → X vs X → [0, 1]


view this post on Zulip Alex Kreitzberg (Apr 19 2025 at 05:43):

Technical art uses parameteric equations and scalar fields. Depending on which is easier for the problem to be solved.

I like to imagine parametric equations as roughly modeling drawing, and scalar fields as roughly modeling painting.

When you give explicit function signatures, it's clear these concepts are dual.

There's lots of flexibility in our choices, but a representative example of this duality is

[0,1]XX[0,1][0, 1] \rightarrow X \leftrightsquigarrow X \rightarrow [0, 1]

Where XX is some topological space.

In my mind an example of a function on the left can be visualized as a "drawing":

c218a217-cb9f-418c-bfc2-e5a94b97e7f8.png

And a function on the right can be visualized as a "painting":

5224d3a7-01c5-4c62-b67e-ee639be2f6d4.png

If X=[0,1]2X = [0, 1]^2 then you'd be drawing or painting on a square paper.

My intuition, is "drawings" and "paintings" are related. You can make a map of countries by drawing their borders, or if you have at least four colors you can paint a map of countries.

Irrespective of my intuition. This duality seems to be really important in category theory. The "drawings" correspond to Lawvere's notion of "figures", the "paintings" correspond to his notion of "cofigures".

They're both examples of representable Functors.

In [[space and quantity]], if I'm understanding it right, what I call a set of "paintings" is a presheaf on topological spaces, or a "generalized space".

And what I call a set of "drawings" is a copresheaf, or a generalized quantity.

Whether you think of these as scalar fields vs parametric functions or "paintings" vs "drawings", these dual perspectives are clearly closely related, even mutually convertible.

Where should I start, or what should I think about, to get a better understanding of these categorical definitions and their duality? Are presheafs and copresheafs a good place to start for example?

view this post on Zulip John Baez (Apr 19 2025 at 06:16):

In physics I like to think of a function RX\mathbb{R} \rightarrow X as a 'particle' and a function XR X \rightarrow \mathbb{R} as a 'field', where XX is 'spacetime'. Particles and fields give dual ways of thinking about matter. I'd never noticed that particles are like drawings and fields are like paintings. Nice!

A space XX with a function [0,1]X[0,1] \to X is called a space 'under' [0,1][0,1], and the category of all spaces under [0,1][0,1] is an example of an 'under category'.

A space XX with a function X[0,1] X \rightarrow [0,1] is called a space 'over' [0,1][0,1], and the category of all spaces over [0,1][0,1] is an example of an 'over category'.

So one way to learn more is to learn about properties of [[over categories]] (also called 'slice categories') and [[under categories]] (also called 'coslice categories').

Lawvere wanted 'spaces', of a very general sort, to be objects of a topos. Then there's a nice theorem that the over category of any object in a topos is again a topos. This is often called the fundamental theorem of topos theory.

It doesn't work like this for under categories! The under category of an object in a topos is not usually a topos. So there's a built in asymmetry in the concept of topos (and other aspects of our concepts of space). If your category of spaces XX is a topos, then the category of spaces over [0,1][0,1] (spaces XX equipped with a map X[0,1]X \to [0,1]) is a topos, but the category of spaces under [0,1][0,1] (spaces XX with a map [0,1]X[0,1] \to X) is usually not.

So, if you set things up nicely, you can get a topos of paintings, but maybe not a topos of drawings.

view this post on Zulip Mike Shulman (Apr 19 2025 at 06:39):

However, if you are willing to discard the requirement that a drawing sits on a pre-existing "canvas", then you can get a topos of "abstract drawings", namely the topos of (pre)sheaves on the category of "drawable shapes".

view this post on Zulip Alex Kreitzberg (Apr 19 2025 at 07:04):

I don't normally think of a mathematician's chalk line drawings as being more limited than shaded chalk "paintings", but ya'll have got me thinking they may be in some subtle way.

Shulman I'm extremely curious about your comment, but I don't quite understand it. What's the category of "drawable shapes"? Did I implicitly define that?

view this post on Zulip Alex Kreitzberg (Apr 19 2025 at 07:06):

Is it the under category [0,1]X[0, 1] \rightarrow X?

view this post on Zulip Alex Kreitzberg (Apr 19 2025 at 07:08):

(And I'm resisting the urge to ask Baez about particle wave duality here, these answers are pulling my brain in a million directions, I'm working hard to restrain myself :joy:)

view this post on Zulip John Baez (Apr 19 2025 at 20:46):

Alex Kreitzberg said:

Is it the under category [0,1]X[0, 1] \rightarrow X?

Note that [0,1]X[0,1] \to X is not an under category! The under category of [0,1][0,1] is a category with all maps f:[0,1]Xf: [0,1] \to X for all spaces XX as objects.

Puzzle. The morphisms in the under category XX are the 'obvious things'. What are they?

view this post on Zulip Alex Kreitzberg (Apr 19 2025 at 20:51):

A morphism between g:[0,1]Xg: [0, 1] \rightarrow X and h:[0,1]Yh: [0, 1] \rightarrow Y is a function f:XYf : X \rightarrow Y such that

fg=h f \circ g = h

view this post on Zulip Alex Kreitzberg (Apr 19 2025 at 20:54):

So a (maybe silly) example of an ff would be one that bends flat paper into a cylinder. Then hh is the drawing you get on the cylinder after bending the drawing you made on the flat paper with gg.

view this post on Zulip John Baez (Apr 19 2025 at 21:07):

Exactly! Or you could have a 3d "drawing" and then project it down to two dimensions.

view this post on Zulip John Baez (Apr 19 2025 at 21:09):

I don't normally think of a mathematician's chalk line drawings as being more limited than shaded chalk "paintings", but ya'll have got me thinking they may be in some subtle way.

It would be wonderful if this mathematical fact - that the over category of an object in a topos is always a topos, but not the under category - was the reason why art museums tend to have a lot more paintings than drawings. But I kinda doubt it.

view this post on Zulip Alex Kreitzberg (Apr 19 2025 at 21:20):

I doubt it too!

I'm more confused what verbs scaler fields could have that parametric functions apparently lack.

view this post on Zulip Alex Kreitzberg (Apr 19 2025 at 21:51):

Assuming I understand what it means to be a topos, there's a mystery (to me) here.

view this post on Zulip Alex Kreitzberg (Apr 19 2025 at 22:11):

And then Shulman's observation reads to me as suggesting if we replace what I called drawings by something slightly more abstract, we get the missing verbs back.

It's all very dramatic and exciting, I wish I understood it better :joy:, perhaps that would diffuse the excitement.

view this post on Zulip John Baez (Apr 19 2025 at 23:01):

I recommend reading those nLab articles on the properties of over and under categories, for starters...

view this post on Zulip Mike Shulman (Apr 19 2025 at 23:06):

If the only things you're drawing are intervals [0,1], then the category of "drawable shapes" will have just one object, [0,1]. Its morphisms will be whatever "sub-intervals" and "reparametrizations" you want to allow on your drawn intervals.

In the simplest case there are none (except the identity) and the category of drawable shapes is the [[point]]. In this case, an "abstract drawing" consists of nothing but a set of "drawn intervals". There's no "canvas" on which they're drawn, they're just "abstractly drawn" in space and have no relation to each other. So in this case the category of "abstract drawings" is equivalent to Set.

Of course you may want to be able to do things like "draw a circle". How can we draw a circle with intervals? We can draw two intervals as long as they match up at the endpoints. If our category of drawable shapes includes the two functions [0,1][0,1][0,1] \to [0,1] that are constant at the endpoints, then we can "draw a circle" abstractly by saying that there are two "drawn intervals", say α\alpha and β\beta, such that if you restrict α\alpha along the constant-at-0 function to get a "constant drawn interval", you get the same thing as if you did that to β\beta, and likewise for the constant-at-1 functions. So we can "draw a circle" abstractly without having any canvas on which to have drawn it.

If you take this to an extreme, you can let the morphisms in your category of drawable shapes to be all continuous functions [0,1][0,1][0,1]\to [0,1], or all smooth functions. Eventually this direction leads to fancy things like [[smooth sets]].

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 04:15):

A glance at the nLab articles indicates that apparently you can do a ton more with over categories than with under categories. I'll try to give some concrete examples of what that means for "paintings"

But for now, let's see if I can follow Shulman's outline.

PSh(C):=[Cop,Set]PSh(C) := [C^{op}, \text{Set}] is the category of Functors from the opposite category of CC into SetSet.

If we have a "drawable shapes" category with one object [0,1][0, 1] and just the identity, this is the trivial category, so PSh([0,1])PSh()SetPSh([0, 1]) \cong PSh(\cdot) \cong \text{Set} formally, because the point maps to a set, and the natural transformations are functions between sets, satisfying naturality vacuously.

We can intuitively think of one presheaf F:[0,1]opSetF : [0, 1]^{op} \rightarrow \text{Set} as mapping the interval to a set of various abstract curves, which is an "abstract drawing". No relationship between these curves in a set is indicated by the formalism. A map between abstract drawings maps curves to curves.

It's not clear to me where this intuition comes from, I hope I'm relating the intuition to the right parts.

To get more sophisticated "abstract drawings", we need to add maps to our category of one object [0,1][0, 1]. To draw a circle we need to be able to glue the ends of our segments together. So we add c0:[0,1][0,1]c_0 : [0, 1] \rightarrow [0, 1] and c1:[0,1][0,1]c_1 : [0, 1] \rightarrow [0, 1] both defined so cx(t)=xc_x(t) = x.

Now a functor F:[0,1]opSetF : [0, 1]^{op} \rightarrow \text{Set} like before maps to a set of curves, but now one such set could have two curves α\alpha and β\beta acting as two halves of a circle. They represent this abstractly by requiring αcx=βcx\alpha \circ c_x = \beta \circ c_x.

Now a natural transformation between such functors must map circles to circles. Because it preserves the structure given by cxc_x.

I hope I wrote that out correctly. A lot of how I understood/interpreted that was via "pattern matching". In particular, I'm not sure why these presheafs can be visualized as making sets of curves from [0,1][0, 1].

view this post on Zulip Mike Shulman (Apr 20 2025 at 05:59):

That seems about right, except that I wouldn't write [0,1] for the category, rather [0,1] is the unique object in that category.

view this post on Zulip Mike Shulman (Apr 20 2025 at 06:01):

Alex Kreitzberg said:

I'm not sure why these presheafs can be visualized as making sets of curves from [0,1][0, 1].

Maybe it would help to think about the case of representable presheaves. If you have an object XX of some category that contains [0,1], like topological spaces, then there is a presheaf Hom(,X)Hom(-,X) that sends the object [0,1] to the set of maps [0,1]X[0,1]\to X in that category. So in that case, the elements of the presheaf certainly are "curves". The point is to generalize that intuition so that for an arbitrary presheaf you think of the elements as "curves", but in some abstract sense rather than in some concrete canvas XX.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 06:47):

Oooooh representable presheaves don't form a topos, but presheaves do. So it's fortunate we can have a common intuition for all presheaves.

I'll sit on this (and circle back to over categories)

view this post on Zulip Simon Burton (Apr 20 2025 at 13:40):

Thankyou @Alex Kreitzberg for asking these questions, it's all very interesting... I'm always afraid to ask stuff like this here because i'm never quite sure what my question is, and the answer tends to be "all of category theory".

One thing i'd like to mention is how the Hom's inherit (algebraic?) structure from the target, so for example, the space of paintings Hom(XX,[0,1]) inherits algebraic operations from [0,1]. You can for example take the minimum of two paintings (or maximum) and this gives a new painting. You can also multipy two paintings.

There's a big theme in mathematics about when/if/how you can recover the points (drawings) of XX from the paintings on XX, such as Hom(XX,[0,1]), or Hom(XX,R\mathbb{R}) etc.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 14:10):

I appreciate you saying that, I'll end up thinking of one of these questions and spend weeks trying find the right way to phrase it.

I felt like I was only doing okay, so it's a relief to know somebody else finds my questions useful. :laughter_tears:

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 14:15):

The inherited algebraic structure on the hom(X,[0,1])\text{hom}(X, [0, 1]) you described looks like blending modes!

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 14:31):

Actually I want to add a point to the "blending mode" observation. Those operations also work for "digital brushes", which fake paint mixing on the canvas.

But even with real art material - your choice between dry pigments, transparent paint, or opaque paint, determines how "additive - average" vs "subtractive" the color mixing behaves. The terminology "burn" and "dodge" came from analog photography, etc. So even with real material you have a concept of "blending mode". You don't need computers for these ideas to be useful.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 15:49):

In light of Simon's comments, I guess the following thought belongs here as well

Here's a trick using "additive blending"

Suppose I have a drawing :[0,1]R2\ell : [0, 1] \rightarrow R^2, and a "brush" b:R2[0,1]b : R^2 \rightarrow [0, 1], like b(x,y)=ex2+y2b(x, y) = e^{-x^2 + -y^2} for example. Then I can get a painting h(x,y)=01b((x,y)(t))dth(x, y) = \int_0^1 b((x,y) - \ell(t))dt, by "drawing" \ell with the "brush" bb.

I want to write some product notation analogous to b\langle \ell | b \rangle for this (but bracket returns a scalar not a function). I'm not sure what it should be assuming it already exists.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 16:14):

In any case, one question I've been lightly thinking about is whether you can factor out \ell and bb from a painting. Or think about a painting as a decomposition iciibi"\sum_i c_i``\langle \ell_i | b_i \rangle", etc.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 16:40):

I guess simply integrating over a path is the more important basic concept here though, if I think about this in a physics motivated way:

Then the notation is just
f\int_\ell f which is fun because of stokes theorem df=f\int_{\ell} df = \int_{\partial \ell} f, so maybe there's some cute way to relate this stuff.

Anyways, I guess I'm half rambling about what this stuff makes me think about. Things like the signatures

RX×XRRR \rightarrow X \times X \rightarrow R \rightarrow R,

or

[0,1]X×X[0,1]X[0,1][0, 1] \rightarrow X \times X \rightarrow [0, 1] \rightarrow X \rightarrow [0, 1]

etc.

view this post on Zulip David Egolf (Apr 20 2025 at 16:53):

On the topic of "curves" without an explicit canvas - that reminds me of an approach towards imaging reconstruction I explored some years ago. The context was this: we were trying to make an image of some "dots", and aiming to correctly locate the dots even when some of them were very very close to one another.

It ended up being beneficial in multiple ways to represent an image in terms of a list of dot locations (and "brightnesses"), instead of using a function that assigned a brightness value to each point in some discrete gridding of the area to be imaged.

view this post on Zulip David Egolf (Apr 20 2025 at 16:55):

Or maybe this was switching to a drawing instead of a painting? I'd have to think about this more carefully.

Anyways, thought it might be a fun example to mention.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 17:05):

Yeah! R2[0,1]R^2 \rightarrow [0, 1] is different than Z2[0,1]Z^2 \rightarrow [0, 1], is different than (R2×[0,1])(R^2 \times [0, 1])^* (where the * indicates we want a free monoid)

But they all involve [0,1][0, 1] in a way that makes it feel like an "output". Which makes these all feel like they're related to presheafs somehow, imo.

view this post on Zulip Simon Burton (Apr 20 2025 at 17:11):

@David Egolf aha, this reminds me of the distinction between rasterized graphics (bitmaps) versus vector graphics! There's always interesting reasons to choose one over the other...

view this post on Zulip John Baez (Apr 20 2025 at 18:02):

Alex Kreitzberg said:

A glance at the nLab articles indicates that apparently you can do a ton more with over categories than with under categories.

That's not exactly right, because every under category is the opposite of some over category, and vice versa.

Puzzle. Why?

However, the answer to the puzzle explains a bit about why over categories are commonly favored.

view this post on Zulip John Baez (Apr 20 2025 at 18:48):

@Mike Shulman got me to fix the wording of my puzzle.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 20:26):

Solution?

The over category C/cC / c has various properties depending on the properties of CC.

If CC is a topos, then C/cC / c is a topos. If CC is a Grothendeick topos, then C/cC / c is a Grothendeick topos. The slice of presheaves is a presheaves on a slice.

Apparently the slice topos over a monoid object is a monoidal topos (which I suppose is where some of the blending modes above come from)!

These properties aren't preserved when constructing under categories.

So one way to answer this question is to note, that for whatever reason, topoi and presheaves are more important than their duals. In particular Set is incredibly important, and a topos, whereas the nlab article [[cotopos]] currently has recorded a single much less important example.

This feels like playing the "why?" game though. It's not entirely clear to me why a cotopos would necessarily be less important, so maybe I'm missing a deeper reason.

(A possibly related exchange question/answer for this: https://math.stackexchange.com/questions/3168833/why-are-presheaves-more-important-than-copresheaves)

view this post on Zulip John Baez (Apr 20 2025 at 21:05):

I wouldn't say a cotopos is less important than a topos; in algebraic geometry toposes let us study geometry while cotoposes let us study commutative algebra: these are dual viewpoints on the same subject. It's just that every theorem about toposes gives a theorem about cotoposes, and vice versa, in a very straightfoward way. So we don't need a big fat book about cotopos theory to put next to our big fat book about topos theory, containing dualized versions of all the theorems.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 21:19):

So under categories should be really common in commutative algebraic settings.

Then over categories might be more popular because Set is more popular/a common foundation (but not more important)?

Or am I still missing the point?

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 21:26):

I guess over categories are probably more popular in Set, but you're allowed to make under categories in Set as well, they just aren't as nice.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 21:30):

Whether over categories are more popular, in general, isn't as important or interesting mathematically.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 21:46):

But hom\text{hom} is a functor into Set, so Set does seem especially important in category theory.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 21:57):

The yoneda embedding lets you realize a category CC as a full subcategory inside its category of presheaves, which is a topos.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 22:01):

The contravariant yoneda embedding is just the same operation over CopC^{op} which still gives a topos.

So in the way we usually do category theory, isn't it easier to get a topos?

view this post on Zulip John Baez (Apr 20 2025 at 22:31):

Alex Kreitzberg said:

So under categories should be really common in commutative algebraic settings.

Yes. But when algebraic geometers think about commutative algebra, they often work with the opposite of the category CommAlg\mathsf{CommAlg} of commutative algebras, which they call the category of "affine schemes", AffSch\mathsf{AffSch}. Then they focus on over categories!

But an over category of an affine scheme is just the opposite of the under category of a commutative algebra. So it's just a matter of preference which you study. Do you like thinking geometrically, or algebraically? Grothendieck's works are largely phrased in terms of schemes and over categories, and this viewpoint led him to invent topos theory as a generalization of set theory, instead of "cotopos theory" as a generalization of "co-set theory".

You're right, our fondness for set theory pushes us to like toposes more than cotoposes. The opposite of the category of sets is the category of complete atomic boolean algebras, and these are very nice, but less famous than sets.

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 23:00):

Is there an opposite version of category theory that uses complete atomic boolean algebras for arrowsᵒᵖ instead of sets?

view this post on Zulip John Baez (Apr 20 2025 at 23:14):

Are you talking about cocategories?

view this post on Zulip Alex Kreitzberg (Apr 20 2025 at 23:35):

I don't know :laughing:. I'm imagining a mirrored universe and history of mathematics done with only incidental uses of Set\text{Set}, but heavy usage of Setop\text{Set}^{op}.

So if in this mirror universe they discover cocategories first, then I guess so!

Anyways this is incidental, I'll circle back to thinking about over categories (and under categories).

view this post on Zulip John Baez (Apr 20 2025 at 23:41):

Anyway, a cocategory is a category object in Setop\mathsf{Set}^{\text{op}}, so if you take the definition of category where you've got a set of objects and a set of morphisms and replace Set\mathsf{Set} by Setop\mathsf{Set}^{\text{op}}, you get the definition of cocategory.

view this post on Zulip Alex Kreitzberg (Apr 21 2025 at 00:05):

You know, I think I subconsciously interpreted an internal category as dependent on the definition of a category, which I'm understanding as depending on Set.

I'm struggling to imagine what it's like to do mathematics/category theory without sets.

Like Setop\text{Set}^{op} has sets of arrows for homsets in my intuition. It's a member of CatCat. For this question I was trying to imagine how it could be interpreted as a cocategory belonging to the 2-cocategory CoCatCoCat, with no reference to Set and therefore Categories.

If a category internal to Setop\text{Set}^{op} automatically does this, or allows this, that's super cool.

(I suspect I'm confusing myself with category theory's primordial ooze)

view this post on Zulip Mike Shulman (Apr 21 2025 at 00:05):

You can't really do mathematics without sets or some set-like things.

view this post on Zulip Alex Kreitzberg (Apr 21 2025 at 00:07):

That makes sense to me! Is it possible to explain why that is?

view this post on Zulip Alex Kreitzberg (Apr 21 2025 at 00:10):

That's something I've just taken for granted, but it feels equally weird for that to be true, and for Setop\text{Set}^{op} to be less commonly used.

view this post on Zulip Mike Shulman (Apr 21 2025 at 00:10):

Well, I wouldn't go so far as to say there's no possible mathematics that can be done without sets. I mean, simple arithmetic doesn't really use any sets. And maybe some aliens somewhere have invented a kind of higher mathematics that doesn't use sets or any set-like things. But it's an empirical observation that most advanced mathematics that humans have invented uses sets. Probably it's intrinsic to the way we think, organizing things by categorizing and grouping them together.

view this post on Zulip John Baez (Apr 21 2025 at 00:14):

Alex Kreitzberg said:

That's something I've just taken for granted, but it feels equally weird for that to be true, and for Setop\text{Set}^{op} to be less commonly used.

I made this point before but I'll do it again: working in the opposite of a category is just another way of thinking about working in that category. We don't need a big fat book about Setop\mathsf{Set}^{\text{op}} because there's a 1-1 correspondence between theorems about Setop\mathsf{Set}^{\text{op}} and theorems about Set\mathsf{Set}. For example the theorem "Setop\mathsf{Set}^{\text{op}} has products" is another way of saying "Set\mathsf{Set} has products". So it's not like we're missing out on anything by talking a lot more about Set\mathsf{Set} than Setop\mathsf{Set}^{\text{op}}.

view this post on Zulip Mike Shulman (Apr 21 2025 at 00:16):

That's true formally, but I think Alex still has a point. When we introduce a structure in mathematics, we generally define it in terms of sets and functions, not op-sets and op-functions, and I don't think that's just an accident of history.

view this post on Zulip John Baez (Apr 21 2025 at 00:18):

I agree. People like to think about bunches of things.

view this post on Zulip John Baez (Apr 21 2025 at 00:20):

Objects in Setop\mathsf{Set}^{\text{op}} are "bunches of predicates" (my rough term for complete atomic boolean algebras), and people also like to think about bunches of predicates - in fact we use them to talk about bunches of things!

view this post on Zulip Mike Shulman (Apr 21 2025 at 00:21):

But, of course, a CABA is a set equipped with various operations on it.

view this post on Zulip John Baez (Apr 21 2025 at 00:22):

You're making me want to redo all of mathematics without sets, just to win this argument, but I don't have time.

view this post on Zulip Mike Shulman (Apr 21 2025 at 00:22):

Haha!

view this post on Zulip Mike Shulman (Apr 21 2025 at 00:22):

Are we having an argument?

view this post on Zulip John Baez (Apr 21 2025 at 00:23):

It felt like it, just then.

view this post on Zulip John Baez (Apr 21 2025 at 00:26):

I'm not really against the idea that there's some sort of primacy of set theory; I'm more trying to get Alex to see that you can flip any statement about Set\mathsf{Set} into a statement about Setop\mathsf{Set}^{\text{op}} and that this is an example of the duality between geometry and commutative algebra - an example where the "commutative algebra" is a kind of boolean algebra, which is the algebra we often use for logic.

view this post on Zulip John Baez (Apr 21 2025 at 00:27):

And it would be nice if he took this idea and somehow used it to develop more ideas about the duality between what he was calling "drawings" and "paintings", or what I call "particles" and "fields".

view this post on Zulip Oscar Cunningham (Apr 21 2025 at 06:17):

(Tangentially related: you can use groups instead of sets as the foundation of mathematics.)

view this post on Zulip Kevin Carlson (Apr 21 2025 at 17:39):

Well, assuming you believe that you haven't used the concept of "set" at all in describing formal theories clearly enough to try to establish ETCS (ETCG) as a foundation in the first place--that is, you can use groups rather than sets as a foundation relative to a formalization of first-order logic that somehow manages to exist outside the foundation you're in the middle of establishing, which is not obviously what it means to give a foundation of mathematics.

view this post on Zulip Kevin Carlson (Apr 21 2025 at 17:39):

(But that's a tangent to a tangent, so it should probably spin out to a new thread if people want to engage with it.)

view this post on Zulip Alex Kreitzberg (May 22 2025 at 07:38):

I have been thinking about this a lot, and it's been hard to move forward, but this reference really helped [[Set : Opposite Category]].

So I wanted to make a note on this

You can take a function f:XYf : X \rightarrow Y to a function P(f):f1(Y)f1(X)P(f) : f^{-1}(Y) \rightarrow f^{-1}(X) via the contravariant power set functor PP. You can think of the power sets as complete atomic boolean algebras.

In the reverse direction, given a map of complete atomic boolean algebras g:ABg : A \rightarrow B, you can pretend their domain and codomain are given by powersets. You define a map by associating to a given atomic element bb in BB, the atomic elements aa of AA which "maps" to bb. But there are a handful of technical points to make this a proof.

In any case, you can prove statements about products in the category of CABAs, and those will automatically be proofs of statements about coproducts, or disjoint unions, in Set.

A "drawing" under this transformation is a map that takes subsets of the plane to intervals that map to that subset.

A "painting" gets transformed into a map that takes subsets of the interval and gives back subsets of the plane that take colors in the given subsets of the interval.

I'm sure more can be said, but this example was slow going, so it might take me a bit to say something more specific and interesting.

view this post on Zulip John Baez (May 22 2025 at 08:02):

There's a lot of beautiful stuff about the relation between sets and CABAs (=complete atomic boolean algebras). For example there are adjoint functors between Set\mathsf{Set} and CABA\mathsf{CABA}, since every CABA has an underlying set and every set has a free CABA on it. And these adjoint functors turn out to be something you know.

But you may not want to head in this direction!

view this post on Zulip Alex Kreitzberg (May 23 2025 at 07:56):

I keep coming around to this at 1 am, so please forgive any mistakes.

There's a handful of analogies I'm seeing lately that feel related, but I can't tell to what extent or in what way.

The most notable one, is that a vector in a real vector space VV can be approximately identified by a linear map RV\mathbb{R} \rightarrow V, and arrows are commonly used in path integration via a dot product.

However, when generalizing to arbitrary dimensions, it's evidently much better to find the associated linear functional (I guess a one form or convector) of VRV \rightarrow \mathbb{R}, and have that eat the elements in sections of tangent bundles, etc.

I don't understand these technical devices as much as I'd like, in particular when I was younger I was thrown off by the transition from a geometric concept of a vector to the algebraic concept of a one-form.

Is this an analog of the duality between CABAs and Set? Between the two sorts, [0,1]X[0, 1] \rightarrow X, X[0,1]X \rightarrow [0, 1] can I see the "painting" as "more algebraic", like the one forms, and find some connection between it and CABAs by seeing paintings as dual to drawings?

view this post on Zulip John Baez (May 23 2025 at 08:11):

The question is vague; I find it's good to ask mathematicians precise questions carefully chosen to maximize my information gain.

The opposite of Set\mathsf{Set} is CABA\mathsf{CABA}; the first category is very 'geometrical' and the second is very 'commutative-algebraic', as you can see by this fact: in Set\mathsf{Set} we have

A×(B+C)A×B+A×C A \times (B + C) \cong A \times B + A \times C

but in CABA\mathsf{CABA} that's false, and since it's the opposite category the roles of product and coproduct are reversed, so

A+(B×C)(A+B)×(A+C) A + (B \times C) \cong (A + B) \times (A + C)

On the other hand the category FinVect\mathsf{FinVect} of finite-dimensional vector spaces is its own opposite. In this category we have

A×BA+B A \times B \cong A + B

and neither of the two operations distributes over the other. So it's neatly balanced in the middle between the geometric and the commutative-algebraic!

view this post on Zulip David Corfield (May 23 2025 at 09:13):

Is that so clear that where

A+(B×C)(A+B)×(A+C)A + (B \times C) \cong (A + B) \times (A + C)

holds, we're in a commutative-algebraic situation? I mean a basic way to think of the cotopos that reverses SetSet's morphisms is given at [[cotopos]]

A binary relation RR between sets AA and BB is injective if for all aAa \in A, bAb \in A, and cBc \in B, if R(a,c)R(a, c) and R(b,c)R(b, c) then a=ba = b. A binary relation RR between sets AA and BB is onto if for all bBb \in B there exists an element aAa \in A such that R(a,b)R(a, b). The category of sets and injective onto binary relations is a cotopos.

But why should we describe this setting as 'commutative-algebraic'?

view this post on Zulip John Baez (May 23 2025 at 12:06):

As you probably know, the category of commutative algebras over a field (or over any commutative ring) has

A+(B×C)(A+B)×(A+C)A + (B \times C) \cong (A + B) \times (A + C)

and its opposite, which is a category of affine schemes, has

A×(B+C)A×B+A×CA \times (B + C) \cong A \times B + A \times C

Similarly CABA, which is a category of commutative algebras of a different sort, obeys the first law and Set, its opposite, obeys the second.

So, I think of these two distributive laws as signs pointing to whether our category is more on the "geometry" or "commutative algebra" side of the famous algebra-geometry duality.

To the extent that a topos resembles Set, the corresponding cotopos will resemble CABA.

But okay, let's get serious: what's the generalization to an arbitrary topos of the theorem that SetopCABA\mathsf{Set}^{\text{op}} \simeq \mathsf{CABA} ? The nLab defines an intuitionistic generalization of CABAs - is that at all helpful here?

That is, define a CABA to be (not a complete atomic boolean algebra but) a frame X such that the locale maps X→1 and X→X×X (which in the category of frames are maps 0→X and X+X→X) are open (as locale maps). (Of course, that X→1 is open is the condition that X is overt.) Then it should be (I will check) a classical theorem that CABAs and complete atomic boolean algebras are the same, and a constructive theorem that CABAs and power sets are the same (in the same functorial manner as above).

view this post on Zulip Morgan Rogers (he/him) (May 23 2025 at 12:13):

It happens that I came across the comments on this MO question this week where Ingo Blechschmidt provides an answer: you want to be working with "Complete Atomic Heyting Algebras" in general, since the lattice of subobjects of an object in a topos need not be a Boolean algebra.

view this post on Zulip John Baez (May 23 2025 at 12:31):

So, to be ultra-explicit about it (just so if I'm wrong someone will speak up), Ingo Blechschmidt seems to be claiming that for any elementary topos E\mathcal{E}, Eop\mathcal{E}^{\text{op}} is the category of complete atomic Heyting algebras in E\mathcal{E}.

If so, that counts as 'commutative-algebra-like' in my book, since a Heyting algebra has a commutative associative 'multiplication' \wedge that distributes over the commutative associative 'addition' \vee.

view this post on Zulip David Corfield (May 23 2025 at 13:13):

Hmm. But a Heyting algebra is a [[distributive lattice]] where both distributive laws hold:

image.png

Why can't I also call them 'geometric' then?

view this post on Zulip David Corfield (May 23 2025 at 13:16):

Anyway, isn't it more about how the Heyting algebras relate to each other, their product and coproduct, rather than the properties of the elements of one of them?

view this post on Zulip John Baez (May 23 2025 at 13:42):

It sounds like in the end you're agreeing with me in an argumentative tone of voice, so I will repeat what I said in a similarly argumentative tone.

Yes, both distributive laws hold in a Heyting algebra. So what? I said the category of Heyting algebras leans on the commutative algebraic side because coproducts distribute over products and not vice versa in the category of Heyting algebras. I was talking about the macrocosm there, not the microcosm.

And I said Heyting algebras are a kind of commutative algebra - or more precisely commutative rig. That's where the microcosm comes in. Yes, it's a funky kind of rig where addition and multiplication both distribute over each other, but it's still a commutative rig, so ideas from commutative algebra apply.

view this post on Zulip David Corfield (May 23 2025 at 14:26):

So much more fun to agree argumentatively!

view this post on Zulip John Baez (May 23 2025 at 14:40):

No, it is!

view this post on Zulip Alex Kreitzberg (May 23 2025 at 19:29):

Whenever Baez says "More precise!" I can't help but think "Yes coach!"

I'm going to keep thinking about the above discussion. And about the adjunction alluded to between CABA\text{CABA} and Set\text{Set}

I'm assuming these will help me form statements about over and under categories per Baez's suggestion. But I'm struggling to make headway.

Here's what I can say so far:

The over category Set/[0,1]\text{Set}/\left[0, 1\right] is a Topos because Set\text{Set} is a Topos. The under category [0,1]/Set\left[0, 1\right] / \text{Set} is complete and cocomplete because Set\text{Set} is.

I'm assuming I can say more about [0,1]/Set\left[0, 1\right] / \text{Set} If I understand CABA\text{CABA} better, is that true?

view this post on Zulip John Baez (May 23 2025 at 20:34):

I wasn't really claiming that anything I've been talking about lately will help you form statements about over and under categories. I was just telling you about fun important stuff! Let's see, I guess you're trying to point out that

[0,1]/Set(Setop/[0,1])op [0,1]/\textsf{Set} \simeq (\mathsf{Set}^{\text{op}}/[0,1])^{\text{op}}
(CABA/P[0,1])op \simeq (\mathsf{CABA}/P[0,1])^{\textsf{op}}

since the object in CABA\mathsf{CABA} corresponding to [0,1]Setop[0,1] \in \mathsf{Set}^{\text{op}} is the power set P[0,1]P[0,1]. But I'm not sure how useful this is.

view this post on Zulip Alex Kreitzberg (May 23 2025 at 20:48):

Thank you for sketching that out! That is what I was trying to do, but yes I wasn't sure whether that was useful. This all has been very fun and interesting to think about. I really appreciate you sharing these topics.

But just to be clear, did you have specific relationships involving particles, fields, Set\text{Set} and CABA\text{CABA} in mind when you said this?
John Baez said:

...I'm more trying to get Alex to see that you can flip any statement about Set\mathsf{Set} into a statement about Setop\mathsf{Set}^{\text{op}} and that this is an example of the duality between geometry and commutative algebra - an example where the "commutative algebra" is a kind of boolean algebra, which is the algebra we often use for logic.

And it would be nice if he took this idea and somehow used it to develop more ideas about the duality between what he was calling "drawings" and "paintings", or what I call "particles" and "fields".

I'm trying to run with this, but I'm struggling to come up with ideas.

view this post on Zulip John Baez (May 23 2025 at 21:23):

Alex Kreitzberg said:

But just to be clear, did you have specific relationships involving particles, fields, Set\text{Set} and CABA\text{CABA} in mind when you said this?

No. A while back you started talking about CABAs, so I wanted to tell you some interesting things about CABAs and how sets are "geometrical" while CABA's are "commutative-algebraic". I was trying to go anywhere with this - this is just good stuff to know.

view this post on Zulip Alex Kreitzberg (May 23 2025 at 22:23):

Thank you for clarifying. Reading too much theory into what people say is something I struggle with - I've done that with many teachers/bosses/professors/etc.

I am having a lot of fun, and feel very fortunate with how available all of ya'll are to talk about these ideas.

view this post on Zulip Alex Kreitzberg (May 24 2025 at 06:54):

A small break from the main theme.

I saw this painting a couple years ago by Theo Van Doesberg called "Arithmetic composition"

d39b3d80-32bc-455c-b339-130e4f28e5c3.jpg

I was like "That's recursion" and felt compelled to think of it as a painting from points to colors.

So I defined a function that was roughly

f:I2Rf : I^2 \rightarrow \mathbb{R} f(x)={diamond(x)x not in top cornerf(4x)otherwisef(x) = \begin{cases} diamond(x) & x \text{ not in top corner} \\ f(4x) & \text{otherwise} \end{cases}

Then I added a bit of other silly fun to get this:
https://www.shadertoy.com/view/4fsGWH

view this post on Zulip Alex Kreitzberg (May 24 2025 at 06:57):

That's where I got the idea for my definition of a painting as a map into colors.

view this post on Zulip John Baez (May 24 2025 at 09:19):

Reading too much theory into what people say is something I struggle with - I've done that with many teachers/bosses/professors/etc.

I would call it "reading too much theory into" what I said. There was tons of theory in what I said. At least in my case, you seemed to be assuming that I was focused on your problem, when in fact I was talking about things I love and feel everyone should know, which you happened to touch upon. I imagine this could often happen when you talk to teachers. Teachers like to teach, which often means imparting the information they are interested in. So: form a mental model of the person you're talking to, and consider the possibility that they're focused mainly on their own mental world, much as you are focused on yours.

view this post on Zulip Alex Kreitzberg (May 24 2025 at 14:34):

I appreciate how clearly and openly you communicate your thoughts, they're very insightful.

It also helps me calm down and relax.

view this post on Zulip Alex Kreitzberg (May 24 2025 at 17:59):

Regarding adjoint functors between CABA\text{CABA} and Set\text{Set}

We want two Functors FF and UU if UU is a forgetful functor than FF is free.

CABA(F(S),B)Set(S,U(B))\text{CABA}(F(S), B) \cong \text{Set}(S, U(B))

So given a set SS we can freely add the joins of all its elements, complete maps are then determined by the values they take on the original elements of SS, because they preserve joins.

So if I'm understanding that right, that just means FF is again the power set functor right?

So the power set functor can establish an equivalence, or it can instead establish at most an adjunction relative to a forgetful functor?

view this post on Zulip Vít Jelínek (May 24 2025 at 18:22):

Yes, but don't forget the variance: in one case, you are considering the covariant powerset and in the other, it's the contravariant version

view this post on Zulip Alex Kreitzberg (May 24 2025 at 19:26):

Okay cool! And you can see that because UU is covariant, in order for the variance of Set(S,U(B))\text{Set}(S, U( B )) to match CABA(P(S),B)\text{CABA}(P(S), B), PP must be covariant, making the natural transformation an arrow in [Setop×CABA,Set]\left[\text{Set}^{op}\times \text{CABA}, \text{Set}\right]

view this post on Zulip John Baez (May 25 2025 at 12:58):

The story is quite beautiful and slightly elaborate - elaborate enough that I tend to forget the details! But they're fairly easy to work out. Check to see if what I'm saying is correct:

We expect a covariant "free CABA on a set" functor F:SetCABAF: \mathsf{Set} \to \mathsf{CABA}, and I believe this is the covariant powerset functor, using the fact that any powerset is a CABA. (What else could it be?)

We also expect a covariant "underlying set of a CABA" functor U:CABASetU : \mathsf{CABA} \to \mathsf{Set}. This has an obvious description: you just take the underlying set of any CABA, and the underlying function of any map of CABAs. But using the equivalence CABASetop\mathsf{CABA} \cong \mathsf{Set}^{\text{op}}, which we have not proved but believe, we can also rewrite UU as a functor U:SetopSetU : \mathsf{Set}^{\text{op}} \to \mathsf{Set}. And what is this? I believe it's the contravariant powerset functor.

The story goes on... do you know about monads?

view this post on Zulip Nathan Corbyn (May 25 2025 at 13:03):

John Baez said:

The story is quite beautiful and slightly elaborate - elaborate enough that I tend to forget the details! But they're fairly easy to work out. Check to see if what I'm saying is correct:

We expect a covariant "free CABA on a set" functor F:SetCABAF: \mathsf{Set} \to \mathsf{CABA}, and I believe this is the covariant powerset functor, using the fact that any powerset is a CABA. (What else could it be?)

It’s not the covariant powerset, it’s the double powerset. CABA is equivalently the category of algebras for the double powerset monad. When we see CABA as Set^op, the resulting resolution of the monad is two copies of the contravariant powerset, whose composite is of course the double powerset.

view this post on Zulip John Baez (May 25 2025 at 13:42):

Oh, whoops, I used to know that. The free CABA on SS is the set of all "disjunctive normal forms" on elements of SS, which are disjunctions of conjunctions of subsets of SS. So, for example, if S={p,q}S = \{p,q\}, a typical element in the free CABA is

(pq)(p¬q)(¬pq) (p \wedge q) \vee (p \wedge \neg q) \vee (\neg p \wedge q)

view this post on Zulip John Baez (May 25 2025 at 13:43):

I never fully worked out how to think of this as PPSP P S where each PP is the contravariant powerset monad, but at least it looks like it's heading in the right direction. :rolling_eyes: I would really like to see PS PS and then PPSP P S as two steps in the formation of the free CABA on SS, and see if there's some connection to how the covariant powerset functor maps any set to the free [[suplattice]] on SS.

view this post on Zulip John Baez (May 25 2025 at 13:44):

Okay, so now it's all starting to come back to me a bit more clearly. I asked if @Alex Kreitzberg is comfortable with monads because this is supposed to lead up to a nice story involving monads.

view this post on Zulip Nathan Corbyn (May 25 2025 at 13:47):

(Contravariant powerset doesn’t form a monad, but: if we rewrite PX\mathcal{P}X as XΩX \to \Omega, then PPX\mathcal{PP}X becomes (XΩ)Ω(X \to \Omega) \to \Omega and we obtain “assignments of (assignments of elements of XX to truth values) to truth values”. In other words, the double powerset encodes the propositional formulae over a set of generators in terms of the set logical functions they can implement.)

view this post on Zulip John Baez (May 25 2025 at 13:59):

That's nice; I sometimes think of 22X2^{2^X} as the set of 'truth tables' on some set XX of propositions, and this is just that made more precise: a truth table is an “assignments of (assignments of elements X to truth values) to truth values”.

Somehow the fact that the covariant powerset functor maps any set XX to the free suplattice on XX seems completely absent here - that's what was distracting me just now. :crying_cat: The free suplattice on XX is all the propositions you can build from propositions in XX using just or, i.e. disjunctions. (Including infinitary disjunctions.)

view this post on Zulip Alex Kreitzberg (May 26 2025 at 04:02):

My takeaway at the moment, is I need to tighten my arguments to understand all the above moving parts. Which I'll work on soonish.

Regarding whether I "Know Monads"

I understand how to see a Monad as a monoid in the monoidal category of Endofunctors with the tensor product as functor composition. I can also translate this definition into a string diagram.

At least in Set I can define Klesli Categories for various examples of Monads. And I have some sense for how Monads can describe syntactic expressions that can be evaluated.

All that said I never feel like I "really" understand Monads :laughing:

view this post on Zulip John Baez (May 26 2025 at 07:54):

Okay. If someone asked you "is there a monad for CABAs?", what would your reaction be?

view this post on Zulip Alex Kreitzberg (May 27 2025 at 05:18):

I still need to take the time to go through everything.

But my initial reaction was "huh?" Then after a bit of thought it was "Oh! The elements of the monad are boolean expressions, like pq,mn,¬rp\wedge q, m \vee n, \neg r. Then the join operation μx:FFxFx\mu_x : F F x \rightarrow F x takes boolean expressions of boolean expressions; and after applications of distributivity and De Morgan's laws, gives a reduced form - maybe a join of meets - of atomic expressions...So, yes I think there is a monad for CABAs."

view this post on Zulip John Baez (May 27 2025 at 05:57):

Excellent! Sounds good! You should generally expect that any sort of mathematical gadget that's a set with operations obeying equational laws is described by a monad: i.e. the category of such gadgets is the category of algebras of some monad on Set\mathsf{Set}.

view this post on Zulip John Baez (May 27 2025 at 05:59):

CABAs are a bit bigger than you seem to indicate since complete boolean algebras allow for infinite ands and ors (also called infs and sups, or meets and joins).

view this post on Zulip John Baez (May 28 2025 at 19:56):

So, it turns out that CABAs are precisely algebras of the monad which is the "double powerset functor" mentioned a while back by @Nathan Corbyn: the square of the contravariant powerset functor from Set\mathsf{Set} to Set\mathsf{Set}.

view this post on Zulip Alex Kreitzberg (May 28 2025 at 19:59):

Sorry for not messaging something sooner, I am working through all of the above, but digesting all of it feels like swallowing a bowling ball.

There are connections across a wide (for me) variety of abstractions.

The pieces are coming together, and I'm going to try and summarize my understanding, but it's taking a bit (maybe I should try and write down my thoughts one by one as I have them, but I feel like I can see vague outlines of "one" story coming together)

view this post on Zulip Alex Kreitzberg (May 29 2025 at 19:58):

I'm short on proofs, but I have a hopefully useful outline of what I think all the claims are.

Okay, we have three functors:

(And now that I spelled all that out, I suppose there's probably some story with the double power set functor of covariant power set functors)

Given the power set functor is used over and over again, it seems likely that there would be some fun relationships between all of these, but I'm really struggling to think of anything. So I'm just going to list stuff about them in parallel.

We already mentioned that I believe the contravariant power set functor describes an equivalence.

The covariant power set functor, is a free functor which forms an adjunction with [[suplatticies]].

The covariant double contravariant power set functor is also free and forms an adjunction, but with [[CABA]].

Years ago when I took algebra, I was shown a theorem that proved that for any normal subgroup, you could define a homomorphism such that the normal subgroup was the kernal.

I was very impressed by this, but I later noticed that if one could, it was more evocative to understand kernals of concrete homomorphisms. The above theorem then implied this could always be done, but actually using the theorem explicitly wasn't generally necessary.

There seems to be a somewhat analogous situation with Monads. Given a Monad, you can break it apart into adjoint functors in multiple interesting ways, but it's so elegant to describe a monad by a given pair of adjoint functors it's a good thing to lead with the adjunction. (Maybe I'm overselling this point, but this intuition seems helpful)

So we have a couple monads UPP:SetSet\mathop{\mathrm{UPP}} : \mathrm{Set} \rightarrow \mathrm{Set} and UP:SetSet\mathop{\mathrm{UP}} : \mathrm{Set} \rightarrow \mathrm{Set}.

UP\mathop{\mathrm{UP}} seems easier to work with even if it's not literally related with UPP\mathop{\mathrm{UPP}}.

The elements of UP({a,b,c})\mathop{\mathrm{UP}}(\{a, b, c\}) are subsets of {a,b,c}\{a, b, c\}, its join μ:UPUPUP\mu : \mathop{\mathrm{UP}}\mathop{\mathrm{UP}} \rightarrow \mathop{\mathrm{UP}} is defined by taking the union of the set of sets. And its unit simply wraps an element into a set of that element.

I would want an algebra over the covariant power set monad to be a function that makes sense on a sets worth of inputs. So the first example I'd think about would be something like Max:UPZZ\mathop{\mathrm{Max}} : \mathop{\mathrm{UP}} \mathbb{Z} \rightarrow \mathbb{Z}. I believe that works because Max({MaxX1,MaxX2,})=Max(Xi)\mathop{\mathrm{Max}}( \{\mathop{\mathrm{Max}} X_1, \mathop{\mathrm{Max}} X_2, \ldots \}) = \mathop{\mathrm{Max}}( \cup X_i )

The story with UPP\mathrm{UPP} is a bit fancier.

Elements of UPP({p,q,r})\mathop{\mathrm{UPP}}(\{p, q, r\}) are sets of sets, one example is {{p,q},{r}}\{ \{p, q\}, \{r\} \}. There is some connection between these sets and conjunction and disjunction, I was open to thinking of the outer brackets as being purely symmetric with the inner brackets, but because we are working with atomic boolean algebras, I'm not sure that works. My intuition is that the first power set takes sets to joins of elements of the set, and so I'd like to write the above expression as (pq)r(p \vee q) \wedge r.

The obvious choice for unit is η(x)={{x}}\eta(x) = \{\{x\}\} (edit: I guess this is wrong?), the tricky definition to understand is join. The correct definition should capture distributivity of join and meet, but presumably should follow from basic set operations.

I'll admit I'm struggling to get a very comfortable handle on this, it should be something like how a polynomial, evaluated over a polynomial, should reduce to yet another polynomial, because of the distributivity property a(b+c)=ab+aca(b + c) = ab + ac. Similarly a(bc)=(ab)(ac)a \wedge (b \vee c) = (a \wedge b) \wedge (a \wedge c), but we also have a(bc)=(ab)(ac)a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c). So it's certainly easy to imagine nested compound propositions flattening in a natural way, but I can't quite see it.

So, lets go at this from a different point of view.

It was already observed that the contravariant power set functor is representable Phom(,Ω)P \cong \mathop{\mathrm{hom}}( -, \Omega), and this allows for a generalization I'm curious about, where we replace Ω\Omega with [0,1]\left[0, 1\right]. So thinking of two variable objects aa and xx as arbitrary but fixed, we can define

μ:((((ax)x)x)x)((ax)x)\mu : ((((a \rightarrow x) \rightarrow x) \rightarrow x) \rightarrow x) \rightarrow ( (a \rightarrow x) \rightarrow x )

μ(f,h)=f(λgg(h))\mu( f, h )= f (\lambda g \rightarrow g (h))

I computer type checked this, so it should be a natural transformation, and I believe it's unique. I don't understand it as well as I'd like, but it sort of ties a bow on all these observations. I guess rather than believe the computer, I know that this is sometimes called the continuation monad in computer science circles.

I kinda want to look into functions with the type (a[0,1])[0,1](a \rightarrow \left[0,1\right]) \rightarrow \left[0,1\right] a bit more. Taking an average of the values of a "painting" seems to fit this, so maybe there could be something fun here to explore.

view this post on Zulip Alex Kreitzberg (May 30 2025 at 05:39):

After writing all this out, I saw a discussion by Reihl that seems to connect the power set functor with the double power set functor, but I think I'm missing some context.

Specifically there's a natural transformation Set(A,PB)Set(B,PA)\mathop{\mathrm{Set}}(A, \mathop{\mathrm{P}} B) \cong \mathop{\mathrm{Set}}(B, \mathop{\mathrm{P}} A), so the power set functor is its on mutual right adjoint.

By using that the power set functor is representable, along with currying, functions on both sides of the above can then be expressed as maps in A×BΩ A\times B \rightarrow \Omega

Reihl then immediately alludes to the induced double power set monad. This was in Example 5.1.4.vii

I don't see the connection between these observations, is there a small hint someone could give to help me see the connection? (assuming I'm reading this right that she is alluding to such a connection)

view this post on Zulip Alex Kreitzberg (May 30 2025 at 06:03):

Wait, you just compose twice around, it's like a normal adjunction between Set and its opposite category,

0dec3b5c-6bf4-4199-a012-31b66dc19140.jpg

Actually yeah, I think this a good thing to have seen. The covariant functor still isn't playing a role though.

view this post on Zulip John Baez (May 30 2025 at 07:04):

The contravariant power set functor, and the diagram you quoted from Riehl, are the things you need to understand CABAs, the monad for CABAs, and how

CABASetop \mathsf{CABA} \simeq \mathsf{Set}^{\text{op}}

view this post on Zulip John Baez (May 30 2025 at 07:06):

This is the stuff that's fun to understand!

The covariant power set functor lives in its own world, apparently. It's the monad for suplattices. The square of the double power set functor cannot be made into a monad!