biproducts

[Alizter]

In this PR we define what we mean by a category having biproducts. We prove standard lemmas, monoidal structure, funtoriality results and duality.

cc @ThomatoTomato you might want to take a look at this since it is directly part of the abelian category formalization in #1929.

[jdchristensen]

Some of the comments in #1929 that aren't marked as resolved are about the file Biproducts.v. Have they been addressed here? (I haven't had time to take a look at this PR yet, but will do so soon.)

[Alizter]

@jdchristensen I don't remember. I will take a closer look ASAP.

[Alizter]

I'll reproduce the outstanding comments here so we can address them in one place:

1. Regarding line 143:

I think this argument about how cat_coprod_prod computes when composed with the inclusions and projections has appeared more than once, so it should be factored out as a lemma. Then, with the change that only uses r once (using catie_homotopic), maybe there is no longer a need to assert the various pieces?

I'll write down and use these lemmas. They can probably appear in Coproducts.v.

I need to think a bit more about the rest of the comments.

2. Regarding line 907:

I have a feeling that what you are doing here might overlap with cat_biprod_corec_rec. If cat_biprod_corec_rec is generalized to be about comparing two maps from a coproduct to a product, then maybe it exactly covers what you need here? Or maybe a slight variation gives a common generalization of both goals?

In Biproducts.v, symmetry and associativity of biproducts is proved using that these hold for products. Then there is some work in showing that these maps respect the coproduct structure. I feel like this should be more formal. In a category with biproducts, every product is canonically a biproduct (as is every coproduct). This is because the biproduct and the product both satisfy the universal property of the product. So the maps showing that products are associative and symmetric, defined using the product structure, should "automatically" respect the coproduct structure. I'm not sure how to make this more precise in a way that would make the proofs simpler, but I suspect that there should be a way.

[Alizter]

@jdchristensen I haven't been able to make progress with the comments that we had, perhaps I no longer understand what needs to be done. Would you be able to take another look at this and give a fresh review, that should allow us to make some progress on this.

I would like to get this merged eventually, so that we can make room for the other abelian cat stuff.

[jdchristensen]

@Alizter It will take me some time to remember the context here. I might have time tomorrow, but if not, it will likely be next week.

[jdchristensen]

I'm about to (finally) review this again. Is it ok if I rebase this (or at least merge master into it) before I do so?

[Alizter]

That's fine with me @jdchristensen

[jdchristensen]

I squashed the previous commits into a single commit, adjusted the result so it builds with current master, and pushed that as a single commit. Then I pushed small commits which make some minor fixes here and there. A couple of small changes also improved many of the slow Defined. lines.

I spoke to @ThomatoTomato today, and we discussed ways that Biproducts.v could be adjusted to make many things smoother. The main idea is to make the smart constructor (or something like it) the main definition of a biproduct. In this version, instead of having separate coproduct and product objects, there is just a single object. There will be instances showing that this object is both a coproduct and a product, so many of the lemmas about biproducts can be skipped, since we can just apply the results about (co)products. It should also be trivial to show that this data gives a biproduct in the opposite category, and moreover this proof will likely be definitionally involutive. What is currently the definition of Biproduct would instead be a different constructor.

A second thing that will likely be helpful is to add IsProduct and IsCoproduct which say when an object with projection/inclusion maps satisfies the universal property. And there will be a lemma saying that if X along with some projections is a product and Y -> X is an equivalence, then Y with the composite maps is a product. The dual of this would make the proof that the current definition of Biproduct implies the new definition trivial, and avoid some duplication.

(As an aside, I think the new definition can drop the HasEquivs assumption on A.)

@ThomatoTomato is willing to try to tackle this reorganization. Is that ok with you @Alizter?

[Alizter]

@jdchristensen That sounds good to me.

[jdchristensen]

@ThomatoTomato I think it's possible to get some of the benefits mentioned above without doing a major restructuring, so I think this makes a good first goal. The idea is to (1) use the instance biproduct_product and drop all of the cat_biprod_* wrapper results about products, and (2) add an instance that shows that the product is also a coproduct, and drop all of the cat_biprod_* results about coproducts. I've already done (1) as a test, and it worked; I'll push it in a minute. For (2), I think the right way to proceed is to add a result to Products.v that says that if X along with some projections is a product and Y -> X is an equivalence, then Y with the composite maps is a product. Then add the dual result to Coproducts.v, and use it to create the instance using cate_cat_prod_corec_inv.

At this point, you wouldn't yet change the definition of Biproduct or add IsProduct and IsCoproduct, so it's a self-contained small change.

After that, we can decide on the next steps.

[ThomatoTomato]

(2) has now been completed. In the first commit we add a result that let us transfer (co)product structures along equivalences in a category. Typeclass search tricks itself into looking for a different goal than what we want, so the second commit tweaks the priorities of typeclass search. In the final commit we remove wrappers for the coproduct. It was still not successfull at infering every parameter, so at some places we need to tell it what the diagram is.

Binary biproducts still keep making wrappers. So a next step would be to keep simplifying. However, it looks like adding IsProductand IsCoproduct could help make this process easier, as typeclass search still gets itself into trouble at this point.

We've also added a couple of new tricks to the main library. Would it be wise to rebase this on master?

[jdchristensen]

Thanks. I'll take a look soon. About rebasing, I guess lhs' and rhs' might be useful, but please wait until I review before rebasing.

[jdchristensen]

I don't understand why this comment is here. biproduct_product is a field of the Biproduct record, so by definition a biproduct is a product.

[jdchristensen]

This is looking good. I've just pushed some changes. Feel free to rebase and to then continue with the next step, probably IsProduct and IsCoproduct. (Github is having problems, so my two commits aren't appearing here. When they do, feel free to continue.)

[jdchristensen]

My commits show up in @Alizter 's repo: master...Alizter:HoTT:ps/rr/biproducts

Hopefully github will show them in this PR soon.

[jdchristensen]

@ThomatoTomato Ok, the commits are here now. See comments above, where I didn't tag you.

[Alizter]

I'll see if I can find some time this week to take a closer look.

[jdchristensen]

@Alizter Thomas is starting to do the next step, which is to change WildCat/Products.v to split the class Product into IsProduct X (with the second and third fields) and Product, which has an object X and an IsProduct X field. (Just like IsEquiv f and Equiv.) Then most results in Products.v which have Product as a hypothesis will be changed to instead take an object X and an IsProduct X argument. This will allow Coq to infer these arguments in situations where X can be deduced from the goal.

The dual changes will be made to Coproducts.v.

Because of instances, I think nothing else in the library will be forced to change, but some places might find it convenient to use the IsProduct/IsCoproduct set-up. Biproducts.v is one place where some things will become simpler.

Does this all sound reasonable to you?

Cc: @ThomatoTomato

[Alizter]

@jdchristensen That sounds good to me.