# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorColin Tan
• CommentTimeJan 15th 2019

Added the contents of the canonical isomorphism induced by some non-canonical isomorphism as coming from Lack’s proof.

• CommentRowNumber2.
• CommentAuthorColin Tan
• CommentTimeApr 1st 2019

Added an explicit formula for the natural map from coproducts to products.

• CommentRowNumber3.
• CommentAuthorTodd_Trimble
• CommentTimeApr 6th 2019

I consider that formula, particularly the usage of $\sqcup$ (or rather that big chunky $\coprod$ I see), an abuse of notation. We have a coproduct functor $-\sqcup -$ and that takes a pair of morphisms $f: a \to b$ and $c \to d$ to $f \sqcup g: a \sqcup c \to b \sqcup d$. If instead you have a pair of maps $f: a \to c$ and $g: b \to c$ and you want a formula for the induced map $a \sqcup b \to c$, then the correct formula for it would be the composite

$a \sqcup b \stackrel{f \sqcup g}{\to} c \sqcup c \stackrel{\nabla_c}{\to} c$

where $\nabla_c$ is the codiagonal map. Thus not to be notated as $f \sqcup g: a \sqcup b \to c$.

Note that this construction is dual to the following construction which takes given maps $f: a \to b, g: a \to c$ to

$a \stackrel{\Delta_a}{\to} a \times a \stackrel{f \times g}{\to} b \times c$

which you denote as $(f, g): a \to b \times c$. Morally, it seems “unfair” to favor the product with a nice snappy notation like $(f, g)$ (the notation you use) while not doing the same, or otherwise spelling out a cumbersome formula, for the dual construction on the coproduct side. My own habit has been to use something like $(f, g): a \sqcup b \to c$ as notation for the coproduct construction and $\langle f, g \rangle: a \to b \times c$ for the product construction and not play favorites. I’d be just as happy with $[f, g]: a \sqcup b \to c$ for the coproduct.

Following those conventions, a formula for the map $c_1 \sqcup c_2 \to c_1 \times c_2$ might be

$[\langle Id_{c_1}, 0_{1, 2}\rangle, \langle 0_{2, 1}, Id_{c_2}\rangle]$

or, dually,

$\langle [Id_{c_1}, 0_{2, 1}], [0_{1, 2}, Id_{c_2}] \rangle$

(or some such).

• CommentRowNumber4.
• CommentAuthorDavidRoberts
• CommentTimeApr 7th 2019

Perhaps ironically, I would use parentheses for maps to products (like vector notation for functions with Euclidean codomain) and angle brackets for maps out of a coproduct (which I’ve seen used before, but I can’t recall where).

• CommentRowNumber5.
• CommentAuthorTodd_Trimble
• CommentTimeApr 7th 2019

David, that way would be fine with me too!

• CommentRowNumber6.
• CommentAuthorDavidRoberts
• CommentTimeApr 7th 2019

And yes, like Todd, I strongly disagree with the notation $f \coprod g$ for maps out of a coproduct. Just like one shouldn’t write $f\times g$ for a map to a product.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeApr 7th 2019

Me three. I use $(f,g)$ for map into a product (analogously to the standard notation for elements of a cartesian product set, which it generalizes if you identify elements with maps out of 1) and usually $[f,g]$ for maps out of a coproduct, calling them “pairing” and “copairing” respectively.

• CommentRowNumber8.
• CommentAuthorDavidRoberts
• CommentTimeApr 7th 2019

I also like the version Mike has for copairing, FWIW.

• CommentRowNumber9.
• CommentAuthorDmitri Pavlov
• CommentTimeApr 7th 2019

I also disagree with f∐g and I like [f,g].

Additionally, ∐ (\coprod) instead of ⊔ (\sqcup) is a wrong symbol to use for binary coproducts, just like ⨁ (\bigoplus) instead of ⊕ (\oplus) is a wrong symbol for binary direct sums.

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeApr 7th 2019

Note that in addition to $\coprod$ (\coprod) and $\sqcup$ (\sqcup) there is also $\amalg$ (\amalg). I’ve never been clear on whether there is an intended semantic distinction between $\sqcup$ and $\amalg$, but both seem to be sized as binary operators.

• CommentRowNumber11.
• CommentAuthorTodd_Trimble
• CommentTimeApr 8th 2019
• (edited Apr 8th 2019)

Following this discussion, and unless there are serious objections, some time soon I am going to start making edits at a number of pages, getting around to biproduct after clearing away some underbrush elsewhere. I’ve made a start at product, and following Dmitri’s observation, I would like to edit away in coproduct the big chunky $\coprod$ as a binary operator, replacing it with $\sqcup$.

(Personally, in my own work I prefer to use $\sum$ over $\coprod$, and $+$ over $\sqcup$, but it would be close to impossible to get universal agreement on such things. However, some mention of these alternatives should be made.)

I would guess that people like ’\amalg’ for pushout notation like $Y \amalg_X Z$. Again, my habit is usually to write $Y +_X Z$.

• CommentRowNumber12.
• CommentAuthorMike Shulman
• CommentTimeApr 8th 2019

Thanks Todd!

I use $+$ sometimes too, but particularly in extensive categories where the coproduct really is a “disjoint union” I often find $\sqcup$ or $\amalg$ easier for me personally to parse, and I also sometimes find that a $+$ isn’t quite strong enough to comfortably support subscripts as used for pushouts (particularly when the subscript gets longer than a single letter). And when both a category and its internal type theory are in play, I sometimes find it’s useful to distinguish between $\coprod$ for the external coproducts and $\sum$ for the internal $\Sigma$-types.