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: Morphism-based pullback notation?

Jacques Carette (Feb 10 2021 at 14:20):

The usual notation for pullbacks is categorically sub-optimal, as it focuses too much on the objects. I am seeking a notation that would highlight that it's the pullback of 2 morphisms that we're computing, to make it also easier to see that the result in fact contains data corresponding to 2 morphisms (and a bunch of proofs).

Morgan Rogers (he/him) (Feb 10 2021 at 14:25):

Any time I've needed to do this, I've had some conventions about spans or cospans set up ahead of time that I could just take the pullback as a special case of, and had few enough to talk about that I could say "Let $(h,k)$ be the span obtained as the pullback of $f:A \rightarrow B \leftarrow C : g$" without that seeming too long-winded.

Nathanael Arkor (Feb 10 2021 at 14:29):

For a morphism $f : A \to B$ in a category with pullbacks along $f$, there is base change functor $f^* : \mathbf C/B \to \mathbf C/A$, so that the pullback of $g : X \to B$ along $f$ is denoted $f^* g : A \times_B X \to A$. This makes it clear that pullback is an operation on morphisms. If the category doesn't have all pullbacks along $f$, this operation is no longer functorial, but the notation could still be appropriately suggestive. (Though note that the notation isn't symmetric: $f^* g$ and $g^* f$ are the two pullback projections.)

Jacques Carette (Feb 10 2021 at 14:30):

I was hoping there were some 'standard brackets' (rather than just parentheses) that were used for this.

Jacques Carette (Feb 10 2021 at 14:31):

I'm not so happy with the base-change notation, exactly because it isn't symmetric. The situation in which I'm interested in having a notation is symmetric (and involves many different pullbacks, thus the need for a shorter notation than pullback-fg).

Nathanael Arkor (Feb 10 2021 at 14:33):

What about $f \times_A g$ for $f : X \to A$ and $g : Y \to A$? After all, the pullback of $f$ and $g$ is the product in the slice category $\mathbf C/A$. This also has the advantage of looking very much like the traditional notation.

Jacques Carette (Feb 10 2021 at 14:36):

I'm definitely in favour of that. If enough others here approve of that choice, I'll give it a whirl in agda-categories and see. I think @Reed Mullanix should be notified of this discussion...

Matteo Capucci (he/him) (Feb 10 2021 at 15:16):

Nathanael Arkor said:

What about $f \times_A g$ for $f : X \to A$ and $g : Y \to A$? After all, the pullback of $f$ and $g$ is the product in the slice category $\mathbf C/A$. This also has the advantage of looking very much like the traditional notation.

This feels so natural I wonder why I've never seen it before :O

Mike Shulman (Feb 10 2021 at 15:49):

I'm pretty sure I've seen $f \times_A g$ sometimes.

Reed Mullanix (Feb 10 2021 at 16:20):

This would definitely solve a lot of notational issues I'm having, thanks all!

Mike Shulman (Feb 10 2021 at 16:47):

Note that the most consistent thing would be for $f\times_A g$ to denote the "diagonal" morphism from the pullback vertex to $A$, since this is the product object in $\mathbf{C}/A$.

Jacques Carette (Feb 10 2021 at 17:03):

Shouldn't we get more used to notation denoting a bundle (record, what have you) of things? It's certainly my experience that getting used to lots of stuff being 'records' and then using explicit projections, assuming you have nice notation for it, increases precision a lot, at a tiny cost to readability.

Mike Shulman (Feb 10 2021 at 18:24):

Well, I wouldn't want to have to include the notation $f\times_A g$ in the names of its projection maps, for instance; I'd rather just write those as $\pi_1$ and $\pi_2$ (or give them explicit names manually in some case if I need them).

Jacques Carette (Feb 10 2021 at 18:46):

Of course. "local scope" is a very useful thing to lighten notation. The point is that if you have 8 pullbacks in scope (and that number is not random) and you need to use all the projections, it does actually become nicer to use $(f \times_A g).\pi_1$ rather than inventing 16 names.

Mike Shulman (Feb 10 2021 at 19:43):

Sure, although I would probably write something like $\pi^{f,g}_1$ instead. In general I think the distinction between "$f\times_A g$ denoting a record with an implicit coercion" and "$\pi_1$ having $f$ and $g$ as implicit parameters that can be made explicit" is something that doesn't really matter when writing mathematics informally on paper.

Jacques Carette (Feb 10 2021 at 20:00):

Indeed. It's worth remembering that 99% of the time, I'm personally doing mathematics formally on a computer. I still want as-good-a-notation-as-possible. With unicode and mixfix notation, one can do quite well - but it's still not full 2D notation.

Ben MacAdam (Feb 11 2021 at 06:10):

I picked up the notation $A {{}_u\times_v} B$ from Matthew Burke, for a morphism of cospans $f,g$ over $m$ you can write $f \times_m g$.