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 ⊔ (or rather that big chunky ∐ I see), an abuse of notation. We have a coproduct functor −⊔− and that takes a pair of morphisms f:a→b and c→d to f⊔g:a⊔c→b⊔d. If instead you have a pair of maps f:a→c and g:b→c and you want a formula for the induced map a⊔b→c, then the correct formula for it would be the composite
a⊔bf⊔g→c⊔c∇c→cwhere ∇c is the codiagonal map. Thus not to be notated as f⊔g:a⊔b→c.
Note that this construction is dual to the following construction which takes given maps f:a→b,g:a→c to
aΔa→a×af×g→b×cwhich you denote as (f,g):a→b×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⊔b→c as notation for the coproduct construction and ⟨f,g⟩:a→b×c for the product construction and not play favorites. I’d be just as happy with [f,g]:a⊔b→c for the coproduct.
Following those conventions, a formula for the map c1⊔c2→c1×c2 might be
[⟨Idc1,01,2⟩,⟨02,1,Idc2⟩]or, dually,
⟨[Idc1,02,1],[01,2,Idc2]⟩(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∐g for maps out of a coproduct. Just like one shouldn’t write f×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
) and ⊔ (\sqcup
) there is also ⨿ (\amalg
). I’ve never been clear on whether there is an intended semantic distinction between ⊔ and ⨿, 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 ∐ as a binary operator, replacing it with ⊔.
(Personally, in my own work I prefer to use ∑ over ∐, and + over ⊔, 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⨿XZ. Again, my habit is usually to write Y+XZ.
Thanks Todd!
I use + sometimes too, but particularly in extensive categories where the coproduct really is a “disjoint union” I often find ⊔ or ⨿ 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 ∐ for the external coproducts and ∑ for the internal Σ-types.
added more hyperlinks to keywords in these examples (Ab, derived category, stable homotopy category, exact functor)
1 to 24 of 24