biproducts, additive and abelian categories

[Alizter]

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!)
• AbGroup is additive
• AbGroup is abelian
• quotients in abelian categories
• epi-mono factorization in abelian categories
• speed up slow build
• work out how to make op of additive category additive without funext
• 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:

• Abelian categories #1126

[jdchristensen]

I've only read partway, and will read more later.

[jdchristensen]

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.

[Alizter]

@jdchristensen They look helpful, thanks!

[jdchristensen]

It's interesting that this is very fast, but the test I tried to add showing that the Is1Cat structure on A^op^op is definitionally equal to the original Is1Cat structure is slow. Any idea why, or how to make that test faster?

[Alizter]

I think its just a bad combination of typeclass search and unification. I switched reflexivity to nrefine idpath and that cut it down to 3s from 6. I think whats left is just reduction.

The issue is that this completely unbundled approach has very poor sharing of terms. If you Set Printing All you will see how huge the terms become. Coq is spending most of it's time unfolding and trying to unify stuff I believe.

[jdchristensen]

What I don't understand is that in the proof of coproduct_op, Coq should need to know that these Is1Cat structures agree, and it does so almost instantly. Why is it fast here but takes 6s in the test? (If you add in the Defined that adds an additional 6s, so it really takes 12s in the test.)

(Also, nrefine idpath and exact idpath are both slightly slower for me than reflexitivity, and all three take around 6s.)

[Alizter]

Let's create an issue about this since I don't want to debug it at the moment. What I would do is create an opam switch with function pointer fp enabled in the OCaml compiler. Afterwards I would use something like https://github.com/janestreet/memtrace to inspect the processor trace of the reduction. There we should be able to see what is taking the most time. (fp just names the function symbols in the machine code with nice names so we can find them in Coq's source).

[JasonGross]

Try #[local] Strategy -100 [<list of constants that need to be unfolded for unification>] or #[local] Strategy 100 [<list of constants that should not be unfolded>]. You could debug by manually doing unfold Product, Coproduct in *. refine H'. and seeing how much you have to unfold manually before things become fast

[Alizter]

Thanks for the tip @JasonGross. Unfortunately it didn't help much. The terms involved just become so large that Coq's printer fails to even print it. I have no idea why there is such a huge increase in complexity compared to other tests in that file.

[Alizter]

I've created #1936 so we can continue the discussion there.

[jdchristensen]

Did you replace apply with nrapply to speed things up? I've noticed this occasionally before, and I don't know why it happens.

[Alizter]

@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.

[Alizter]

@jdchristensen FTR, I will push some changes here shortly. I am working on smart constructors for biproducts and showing that AbGroup has them.

[Alizter]

@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.

[Alizter]

@jdchristensen Would you like me to split off the changes to WildCat/Products.v so that we can better review in a separate PR?

[jdchristensen]

Yes, it might be helpful to split it up.

[Alizter]

One of my merges accidentally introduced some WIP changes so the build fails. I will fix the build accordingly soon enough.

[Alizter]

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.

[jdchristensen]

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.

[Alizter]

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)
.

[jdchristensen]

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.