Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
biproducts, additive and abelian categories
Here is a definition of biproducts, semiadditive categories and additive categories. We show that semiadditive categories have a commutative monoid structure on their hom and additive categories have an abelian group structure.
We also show that the group of endormorphisms forms a ring with composition.
Kernels, cokernels and abelian categories are also defined.
I will probably split this PR further into smaller parts once the main theory has been settled. I'll keep it here for a global overview.
TODO
- [ ] clean up associativity proof
- [ ] left modules are additive
- [ ] left modules are abelian (over a commutative ring!)
- [x] AbGroup is additive
- [ ] AbGroup is abelian
- [ ] quotients in abelian categories
- [ ] epi-mono factorization in abelian categories
- [x] speed up slow build
- [x] work out how to make op of additive category additive without funext
- [x] Fix unification issue in 8.18
- [ ] finish opposite additive cat proof (inverse law is tricky)
5 years ago I was apparently interested in doing this:
- https://github.com/HoTT/Coq-HoTT/issues/1126
I pushed a slight cleanup to using decidability. I'm guessing the lemmas/tactics I added can be used elsewhere. But if you think they don't help, feel free to revert.
Did you replace apply with nrapply to speed things up? I've noticed this occasionally before, and I don't know why it happens.
@jdchristensen I think apply is wasting time trying all sorts of first-order heuristics which are not fast when there are typeclass searches to be done.
@jdchristensen FTR, I will push some changes here shortly. I am working on smart constructors for biproducts and showing that AbGroup has them.
I've managed to prove that AbGroup is additive. It's good to see that the underlying function of both operations on homs are the same as expected.
If you get a chance to re-read all of the new comments and check for typos, that would be great.
I've fixed the spelling errors in the new comments I've added. I keep forgetting to turn my spellchecker on.
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.
I've now make a quick pass over everything. You've done a heroic amount! I'm hopeful that some parts can be simplified by thinking of conceptual ways to organize what is going on, but even if not, this will be great to have.
@jdchristensen In the latest commit before, I've revised some of the proofs in Products.v. I've given two new proofs of the pentagon: one with the twist construction and one without the twist construction. The one without ended up being much shorter compared to both other proofs. I'll clean this up later so that we only have a single proof. Something to think about with regards to the twist construction.
@jdchristensen Would you like me to split off the changes to WildCat/Products.v so that we can better review in a separate PR?
One of my merges accidentally introduced some WIP changes so the build fails. I will fix the build accordingly soon enough.
I've fixed the build errors and tried to make progress on the cocommutative comonoids giving commutative monoid structures on the homs. Unfortunately, this doesn't follow formally from what I can tell so I had to reprove the argument like I did for commutative monoids giving commutative monoids. Once this is done, I have trouble using it since the is1bifunctor instance for cat_binbiprod and cat_bincoprod are different.
One way to fix this is to redefine biproduct so that the coproduct structure is something that can be proved rather than part of the data. I don't know if this will really work, but I am getting quite stuck with this approach, however I'll continue to experiment when I have more time.
I've [...] tried to make progress on the cocommutative comonoids giving commutative monoid structures on the homs. Unfortunately, this doesn't follow formally
It should be formal. If X is a cocommutative comonoid in a wild category C, then you should be able to prove easily (or, if you are lucky, it might be definitionally true) that X is a commutative monoid in C^op. From that it follows that Hom in C^op from any Y to X is a commutative monoid. But that Hom type is definitionally equal to Hom in C from X to Y, so we have a commutative monoid structure here as well.
I haven't looked at the code you pushed, so I don't know how this compares to what have done, but the point is that the argument factors into two parts, and the second part is definitional, and doesn't require that you check the commutative monoid axioms again.
As you said, it should be possible to prove that the double opposite monoid structure is the original structure, however this does not appear to be the case definitionally hence why I struggled earlier. One possible way to fix this is to fix natural transformations (and equivlaences) to become definitionally involutive as highlighted in #1961. This would allow the associator and unitors to be definitionally involutive. (For the full monoidal structure it seems we would need two pentagons and two traingles) however I don't see any use for that yet) .
Even if it is not definitional that a comonoid in C is a monoid in C^op, I still suspect that going via this statement might be a better way to prove that hom from a comonoid is a monoid. First, this statement only involves one object, not two, and shouldn't need any extensionality, so it should have less bureaucracy. Second, it's a useful statement to know independently of this application . Third, once you have this statement, the monoid structure on the hom will be immediate.
@jdchristensen Do you think it would be a good idea to split off the part on biproducts into a separate PR so that it can be reviewed and merged separately? It mostly mirrors what we have for Products and Coproducts and can be modified later when we wish to make progress on semiadditive categories.
@Alizter At this point, I don't remember the status of everything in this PR. Skimming the above, I see lots of discussions that haven't been marked as resolved, so it seems like there might still be a lot to do for the whole PR. But smaller pieces that are ready to merge would be easier to review.
@jdchristensen Yes, there are a lot of points and I've lost track of most of them at this point.
My plan for making progress is to isolate the part about biproducts and afterwards we can try to tackle the definition of additivity together with the abgroup homs. I've tried a few times to formalize the argument about cocommutative comonoids but I am always running into difficulties which means I am probably doing something wrong. As this PR is too big for its own good, it would be good to investigate these in its own separate PR.