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.
Jacques Carette (Jun 26 2020 at 01:54):I'm trying, vainly, to find a detailed, formal definition of "product-preserving functor", and I've come up empty handed. I've got multiple guesses as to what it might mean -- and that's exactly the problem, I have more than one guess. [Yes, I'm trying to formalize morphisms of Lawvere theories.]
Reid Barton (Jun 26 2020 at 03:53):The image of a finite product cone is a finite product cone. (I assume you mean all finite products since you mention Lawvere theories.)
John Baez (Jun 26 2020 at 06:13):It doesn't count as "detailed, formal", but this is the definition:
John Baez (Jun 26 2020 at 06:16):If you want something that fills in all the details you might be more likely to find it in a definition of "limit-preserving functor", since a product is a limit.
John Baez (Jun 26 2020 at 06:16):If I had a whiteboard and 15 minutes I could write down the definition very carefully.
Morgan Rogers (he/him) (Jun 26 2020 at 08:37):Note that if your categories come equipped with a choice of products, a product-preserving functor between them is typically not required to preserve that choice on the nose (and if it does, you would use a qualifier such as "strict" to indicate this)
Jacques Carette (Jun 26 2020 at 11:20):Yes, I mean all finite products. Now, having all finite products is induced by having a terminal object and all binary products (i.e. being cartesian): is there an essential difference? In which case preserving products would be the same as being a cartesian functor.
Nathanael Arkor (Jun 26 2020 at 11:23):There is no essential difference between having n-ary products for all natural numbers n, and having binary products and a terminal object. It's simply a choice of presentation.
John Baez (Jun 26 2020 at 18:28):A functor that preserves finite products is called a "cartesian" functor - they are the same thing.
John Baez (Jun 26 2020 at 18:29):If anyone talks about a category with chosen products, and functors preserving those chosen products, they are talking about something else - and something less useful in most mathematical applications.
Dan Doel (Jun 26 2020 at 18:29):Is it only called that when the categories it maps between have all finite products (and are thus Cartesian)?
John Baez (Jun 26 2020 at 18:30):If you talk about a functor preserving all finite products that exist between categories that don't have all finite products, it's your job to warn people, because this is not the main thing people talk about.
John Baez (Jun 26 2020 at 18:31):It's like talking about a homomorphism between things that, umm, aren't quite groups because multiplication is partially defined.
Dan Doel (Jun 26 2020 at 18:31):I guess that case is irrelevant for Lawvere theories.
John Baez (Jun 26 2020 at 18:32):So anyway: yes, if someone says "cartesian functor" I'm gonna assume they mean between cartesian categories.
John Baez (Jun 26 2020 at 18:32):To be honest, I've never heard it used any other way.
Dan Doel (Jun 26 2020 at 18:33):Right, I wouldn't expect it.
Dan Doel (Jun 26 2020 at 18:34):I think people usually say things like "preserves finite products that exist" if not all finite products exist, too. But I suppose someone might not do that (though it would be poor communication).
Reid Barton (Jun 26 2020 at 18:46):Note however that some people use "cartesian functor" to mean a functor which preserves all finite limits. Personally, I rarely encounter either usage.
John Baez (Jun 26 2020 at 18:50):After you say "finite-product-preserving functor" 10 times in a paper you start wanting to say "cartesian functor" instead, so I think Christian and I did that in our paper on enriched Lawvere theories. Of course we defined this term.
Morgan Rogers (he/him) (Jun 26 2020 at 19:44):Johnstone does a reasonable job in the Elephant of pushing through the tension between "cartesian functor" (which he defines to mean functor preserving finite limits) and "cartesian/cartesian-closed categories" (where cartesian refers just to finite products).
John Baez (Jun 26 2020 at 19:48):There's another perfectly standard term for "preserving finite limits", namely "right exact", so I see no need to sully "cartesian" with this extra meaning. And if "right exact" is too long, there's even a standard abbreviation, namely "rex".
John Baez (Jun 26 2020 at 19:49):In my paper with Kenny Courser on structured cospans, we use to mean the category of categories with finite limits and right exact functors.
John Baez (Jun 26 2020 at 19:50):Of course this leads to lots of fun dinosaur jokes too.
Nathanael Arkor (Jun 26 2020 at 19:51):John Baez said:
Of course this leads to lots of fun dinosaur jokes too.
Surely the leading motivation for describing finitely complete structures.
Jules Hedges (Jun 26 2020 at 19:54):John Baez said:
There's another perfectly standard term for "preserving finite limits", namely "right exact"
How did I make it this far and not know this?!? I thought exact functors were something mysterious from algebraic topology
John Baez (Jun 26 2020 at 19:55):They are - and so are "categories".
John Baez (Jun 26 2020 at 19:55):Left exact = preserving finite colimits
Right exact = preserving finite limits
Exact = preserving finite limits and colimits
John Baez (Jun 26 2020 at 19:56):An exact functor between abelian categories is also equivalently one that preserves "direct sums" and "short exact sequences". That's probably more like how you saw defined. But that's just an obscurantist approach.
Jacques Carette (Jun 26 2020 at 20:07):This is perfect! That's what I ended up implementing. Coming soon to your favourite agda-categories library near you.
But wow, in everything I read, no one, I mean no one admitted that 'finite-product preserving' and 'cartesian' were the least bit related. [Including the nLab BTW.]
John Baez (Jun 26 2020 at 20:08):Weird.
Nathanael Arkor (Jun 26 2020 at 20:11):Jacques Carette said:
This is perfect! That's what I ended up implementing. Coming soon to your favourite agda-categories library near you.
But wow, in everything I read, no one, I mean no one admitted that 'finite-product preserving' and 'cartesian' were the least bit related. [Including the nLab BTW.]
This is the second bullet point on the nLab page for "cartesian functor".
Jacques Carette (Jun 26 2020 at 20:14):Thanks! Unlike https://ncatlab.org/nlab/show/product-preserving+functor. Or https://ncatlab.org/nlab/show/categories+with+finite+products+are+cosifted. Or the page on Lawvere theories.
Nathanael Arkor (Jun 26 2020 at 20:15):They should be updated :)
John Baez (Jun 26 2020 at 20:36):Do it!
Paolo Capriotti (Jun 26 2020 at 21:52):John Baez said:
Left exact = preserving finite colimits
Right exact = preserving finite limits
Exact = preserving finite limits and colimits
I think you have it backwards there.
Rune Haugseng (Jun 26 2020 at 23:21):This is why you should never name anything "left/right X"...
Cole Comfort (Jun 27 2020 at 02:28):Rune Haugseng said:
This is why you should never name anything "left/right X"...
You can either ask for the preservations or left/right exact sequences (in the abelian case at least) or limits/colimits; so you will run into the same problem because there are just two dual notions.
John Baez (Jun 27 2020 at 05:41):Yes, I said it backwards. I have about a 51% chance of saying these things correctly in casual conversation, but when I get serious I can always figure it out.
It's annoying that colimits are left adjoints and "left exact" means preserving finite limits.
John Baez (Jun 27 2020 at 05:44):However, it's sorta cute that finite limits theories are so connected to syntax, which is sort of "lexical".
Amar Hadzihasanovic (Jun 27 2020 at 14:13):One of my least favourite examples is how left hom-objects (in a monoidal category) are right Kan lifts.
Amar Hadzihasanovic (Jun 27 2020 at 14:14):And right hom-objects are right Kan extensions.