Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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).
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).
David, that way would be fine with me too!
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.
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.
I also like the version Mike has for copairing, FWIW.
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.
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.
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$.
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.
1 to 12 of 12