Categories as extensible structures

[Benoit]

Here is a question prompted by my remark in https://groups.google.com/d/msg/metamath/Nvh_ue-PSBM/Nj-XpBvBAAAJ

  "there is some gymnastic to do to put things in the right "slot", which looks painful..."

I see in ~df-cat that if c is a category, then ( Base " c ) is actually the set of objects of c while the set of morphisms is denoted ( Hom " c ).  It looks a bit strange, and it would be more natural  in my opinion to take the set of morphisms as the base set, while having a slot ( Obj " c ) for the set of objects of c.  Is there a particular reason for choosing the current convention ?  Would it be possible to change it to the proposed one, or would it be too much work ?

Benoît

[Mario Carneiro]

That proposal seems very odd to me. When we talk about categories, we almost always refer to them using their set of objects. For example, the category of groups (and group homomorphisms), or the functor category D^C (using the same exponential notation used for the underlying set of objects; the homs are natural transformations which have no such nice notation).

If we wanted to equip our algebraic objects with a category structure (for instance, the reals as a poset category), the objects would be the carrier and the homs would be something new. So everything seems to point to Obj = Base and Hom being a new slot.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/12352990-c8ab-4df9-b031-d30c586b7ef8%40googlegroups.com.

[Benoit]

Ok. I'm not insisting since I'm not fond of extensible structures anyway.  But it is certainly not odd to make morphisms the underlying set of a category.  The fact that an "arrows only" definition of a category is possible shows that it's that latter set which is more important.  Also, it is common to say that a monoid (resp. group) is a category (resp. groupoid) with one object. (This is actually what led me to this proposal, see the linked post with the question by David Starner.)

Indeed, one often says things like "the category of groups" instead of "the category of groups and group morphisms" or "the category of morphisms", but this is an abuse of language.  It's ok in this case since the morphisms are obvious, but it is not always so.

As you noted, considering posets as thin categories seems to contradict this.  The same goes with metric spaces as (\R, \leq)-enriched categories.  But actually, these are examples of categorification, so it's expected that there is a shift by 1 (from n-morphisms to (n+1)-morphisms).

Benoît

[Mario Carneiro]

I figured the monoid example would come up, but I think that really is a special case. Morphisms don't really act like a set, they are more like a |C| x |C| indexed family of sets. It just so happens that when |C| is a singleton that's just one set. In any other case, in any category that is not just a monoid in disguise, collapsing all morphisms into one pot doesn't look like the right thing to do. (Yes it is useful for some things, and (Arrow`C) is available for that, but most of the time when you want to build hom sets you really want the domain and codomain to be inputs not outputs.) So even if we wanted the homs to be "primary", they don't have the right type to be in the (Base`C) slot anyway.

I think that "the morphisms are obvious" given the objects in the same way that the addition or multiplication is obvious given the base set like RR or CC. You can call it an "abuse of language", but I think this is really what mathematicians want structures to accomplish, and which is encoded in systems like Lean's typeclass inference, that infers a quasi-unique structure "ring R" given a carrier type R. (Mathematically it is clearly not unique in most cases - there are many ring structures on RR - but we really want a single "canonical" one.)
 

--

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/84285818-c976-4912-a4bd-2c9af466e79e%40googlegroups.com.

[Benoit]

You're right: the set of morphisms is naturally a "bi-fibered" set over the set of objects.  But the question we have to answer in the present case is "what do we put in the Slot "Base" of a category".  This is less a matter of profound mathematical nature (I wrote often enough the uneasiness I have regarding extensible structures being "nonmathematical") than a matter of convenience and practical applications.  Since I admit I am not a big contributor, I leave it to more experienced users to decide the best coding.  I'll have a look at ( Arrow ` C ) as you suggested.

By the way: it is not because the set of morphisms is bi-fibered that we cannot consider it as a set: after all, "the total space of a fibration" is a common mathematical object.  A special example: in a Lie groupoid, one requires that the morphisms form a smooth manifold: even if this manifold is bi-fibered, it is considered as a whole.

About your wish that there be a "unique canonical notion of morphism once one knows the objects" (if I understood you correctly), it is not the case.  It might be the case for algebraic structures concrete over Set, but not in general.  Already when the objects are sets, the morphisms can be either functions or relations.  When the objects are metric spaces, the best notion of morphisms is probably short maps (as hinted in my previous message in this thread), but the categories of metric spaces and continuous (or uniform, or Lipschitz, or locally Lipshitz, or coarse) maps are also interesting.  Same goes with Banach spaces, etc.  Even for structures, it is not that clear: tropical semiring, p-adic valuations (by the way: your formalization of Ostrowski is impressive), etc.

Benoît