wildcat: binary products

[Alizter]

We define what it means for a wild cat to have binary products and then show Type, pType and Group to have binary products. This notion of product is only 1-coherent as it will not be the correct notion of a product in a bicategory. But this doesn't matter for now as we haven't even defined a full bicategory yet.

AbGroup will be left out for now as a notion of biproduct will follow soon.

I've also defined binary coproducts as products in the opposite category and shown Type, pType and Group as examples of categories with binary coproducts.

[jdchristensen]

Would it be better to first define what it means for two objects x and y in a wild category A to have a product, and to then say that A has products if all pairs of objects have a product? Then, things could be proved about any particular binary product even if you don't know that the entire category has them.

The definition of products involves a lot of data. Would it work to instead say that the functor A^op -> ZeroGroupoid sending z to (z $-> x) * (z $-> y) (product of 0-groupoids) is representable? In other words, there is a product object x $* y and a natural equivalence of 0-groupoids (z $-> x) * (z $-> y) $<~> (z $-> x $* y). This avoids redundancy, and might turn out to be a well-behaved notion. All of the data you specify would be derivable, and there could be a constructor that takes data like you listed and provides the natural equivalence. We'd also be able to leverage the work on 0-groupoids and use results like isequiv_0gpd_issurjinj to help construct equivalences of 0-groupoids. This point of view also makes it clear that the product is unique. But maybe there are issues I'm not seeing?

About naming, should we prefix more of the names with cat_? We could use cat_prod instead of product, so it is only one character longer.

There are many spelling mistakes in the comments. Can you double-check them?

[Alizter]

Would it be better to first define what it means for two objects x and y in a wild category A to have a product, and to then say that A has products if all pairs of objects have a product? Then, things could be proved about any particular binary product even if you don't know that the entire category has them.

That sounds like a good idea, I'll try to experiment with it. Do you have any categories in mind where binary products aren't available for all objects?

The definition of products involves a lot of data. Would it work to instead say that the functor A^op -> ZeroGroupoid sending z to (z $-> x) * (z $-> y) (product of 0-groupoids) is representable? In other words, there is a product object x $* y and a natural equivalence of 0-groupoids (z $-> x) * (z $-> y) $<~> (z $-> x $* y). This avoids redundancy, and might turn out to be a well-behaved notion. All of the data you specify would be derivable, and there could be a constructor that takes data like you listed and provides the natural equivalence. We'd also be able to leverage the work on 0-groupoids and use results like isequiv_0gpd_issurjinj to help construct equivalences of 0-groupoids. This point of view also makes it clear that the product is unique. But maybe there are issues I'm not seeing?

Very interesting idea! I'll try it out!

About naming, should we prefix more of the names with cat_? We could use cat_prod instead of product, so it is only one character longer.

That seems like a sensible idea.

There are many spelling mistakes in the comments. Can you double-check them?

Yes, sorry about that. I need to reenable my spell checker.

I'll mark this as draft for now/

[jdchristensen]

Do you have any categories in mind where binary products aren't available for all objects?

I mainly made that suggestion since I thought it would lead to a better factorization of the code, but there are examples. E.g. in a poset (regarded as a category), products are meets, which sometimes exist and sometimes don't. In the category of manifolds with boundary, manifolds that happen to not have a boundary have products, but manifolds with non-empty boundary don't.

[jdchristensen]

About my second suggestions (using representability), an intermediate amount of data might be better to work with. Say that a product of x and y is an object xy and projection maps xy $-> x and xy $-> y such that the induced map (z $-> xy) -> (z $-> x) * (z $-> y) is an equivalence of 0-groupoids for each z. The advantage of this is that there is no need to require naturality, since this map will automatically be natural.

[Alizter]

This seems to be working but I will need some more time to finish it. Your suggestion of factoring products for a specific pair of objects also led to more composable code. Another class of examples of such categories I thought of is the sum of a category with products to one without. Obviously, only a subclass of the category has products in that case.

I like that we are reflecting limits from groupoids into wild categories. I'm hopeful we can do a similar strategy for more general limits and colimits. That way things like the 3x3 lemma for pushouts could be reduced to the 3x3 lemma for pullbacks in groupoids.

[Alizter]

@jdchristensen I've managed to change the definition to the one you suggested. It does in fact contain the exact same data, but it took a while for me to get it working since I had to really understand the terms I was looking at in the proofs. In the end, I managed to make all the lemmas fall out. Rather than forcing users to go through building a groupoid equivalence, I created a nicer constructor for building products that contains the equivalent data.

I've also fixed some typos and naming choices.

[Alizter]

I've added a definition of binary coproduct as a product in the opposite category. Many of the properties and lemmas follow definitionally from the product case. The functoriality of the coproduct was so straight forward, but with the correct lemmas about the interaction of functors and opposite categories, should make it possible. I've however left this for future work, as the functoriality of the coproduct is not as useful compared to the product.

[jdchristensen]

I like how that turned out!

[Alizter]

@jdchristensen I'm proving coproducts in a few categories as we speak, so I'll push those soon and address your review comments.

[Alizter]

@jdchristensen I've shown that Type, pType and Group have coproducts also. Let me know if there are any more categories you can think of.

We probably need to do a little more work before showing that CRing has coproducts due to the need for a tensor product of rings.

AbGroup will follow this later. I plan to define a notion of binary biproduct where a category has biproducts if it has binary product and coproduct with the canonical map between them being an equivalence. I'll need to do some more experimentation on that however.

[Alizter]

Once we have biproducts following this PR, we should be able to define semi-additive and additive categories. Together with some more simple (co)limits we can generalize most of our homological algebra work to an arbitrary (appropriate) category.

[jdchristensen]

This looks great!

[Alizter]

@jdchristensen I'm looking at possibly generalising all of this for arbitrary limits for which I will need to describe limits in ZeroGroupoid. I've done this by defining limits as the hom from a constant diagram to a diagram in the presheaf category.

It seems at some point I have to require the 1-functoriality of the carrier map of a ZeroGroupoid. Do you think this is true? I'm having trouble defining how it should act on 2-cells. I feel like we are missing this level of coherence.

If this is not possible, then I will need to rethink how to define a general notion of limit.

[jdchristensen]

It seems at some point I have to require the 1-functoriality of the carrier map of a ZeroGroupoid. Do you think this is true? I'm having trouble defining how it should act on 2-cells. I feel like we are missing this level of coherence.

No, that's not true. If G is the 0-groupoid with underlying type Unit and one (identity) morphism, H is the 0-groupoid with underlying type Bool with morphisms in both directions between true and false, then there is a 2-cell between the into inclusion functors G → H (as maps of 0-groupoids), but there is no 2-cell in Type between those maps.

I haven't thought about why this would be needed to define limits. But I did think about defining an equalizer of two parallel functors f, g : G → H of 0-groupoids, and when defining the 1-cells in the equalizer, there is a 2-cell in H that needs filling. It could be done using the identity type, but that feels a bit unnatural. So for general limits, we might need to assume that our ambient wild category has enough higher cells for us to construct the appropriate limit of the Yoneda functors. Not sure.

Things are easier for products since there are no morphisms in the diagram.

[Alizter]

Some other ideas I've been floating around: We might be able to define a displayed ZeroGroupoid and maybe replicate the "forall" construction from pType. I feel like this would be too good to be true however.

[Alizter]

Merging this now, I'll play around some more with general limits / colimits. If we manage to get something working, it could be very useful in replacing all our limit / colimit theories for Type with something more generic and useful.

[Alizter]

@jdchristensen The reason you might need carrier to be a 1-functor is that a diagram of groupoids is D^op -> ZeroGroupoid, however a type based limit takes functors of the form D^op -> Type. The underlying assumption is that carrier is not only a functor, but also limit preserving, which I would believe to be true. Here is a definition of limit in Type:

(** General limits in Type. *)
Definition limit_type {D : Type} `{Is1Cat D}
  (F : D^op -> Type) `{!Is0Functor F, !Is1Functor F}
  : Type
  := NatTrans (fun _ : D^op => Unit : Type) F.

and I would start limit in ZeroGroupoid off like:

Definition limit_0gpd {D : Type} `{Is1Cat D}
  (F : D^op -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
  : ZeroGpd.
Proof.
  snrapply (Build_ZeroGpd (limit_type (carrier o F))).