tensor products of abelian groups

[Alizter]

This PR constructs the tensor product of abelian groups. We show that tensor products give a symmetric monoidal structure to AbGroup using the twist construction for symmetric monoidal categories.

This PR depends on:

• free abelian groups #2020
• grp_pow and related things #2015

So it would be good to finish those before. In the meantime this PR can be read. There are some issues I would like to address:

• ab_tensor_prod and its constructor tensor are slow to work with. If you have a goal involving them and you do a cbn or simpl, Coq will hang. We should think carefully about helping Coq to not unfold certain parts to make this reasonable to work with.
• The file TensorProduct.v needs comments.
• Some of the grp_pow lemmas should follow from the lemmas outlined in grp_pow and related things #2015.
• There is some duplication between the different induction principles for ab_tensor_prod. We need to think how to share more here.

cc @ThomatoTomato as this is something you are presumably interested in.

[jdchristensen]

This is looking good so far!

[jdchristensen]

I guess we should have a version of subgroup_generated that lets you provide a family gen : I -> A of elements, and constructs the predicate fun x => exists i, gen i = x for you. Also, I think (a1 + a2, b) - ((a1,b) + (a2,b)) would be the more natural parenthesization. And it might make tensor_dist_* a bit easier. And ab_tensor_prod_rec. In fact, we should probably generalize this to an abelian group with generators and relations, with relations given by two functions I -> A representing the left and right hand sides of the relations, and a recursion principle in this generality. It should be cleaner.

[Alizter]

Could you expand on this idea a bit further? What would gen be in this case?

[jdchristensen]

In my first sentence, we could take I to be A * A * B + A * B * B and gen would send (a1,a2,b) to (a1+a2,b) - ((a1,b) + (a2,b)) and act similarly on the A * B * B summand.

In my last sentence, I would stay the same, and we'd have lhs sending (a1,a2,b) to (a1+a1,b) and rhs sending (a1,a2,b) to (a1,b) + (a2,b) (and both would act similarly on the other summand). Then the induction principle would involve an equation, rather than a difference, which might eliminate some of the manipulations needed.

I don't think either thing I'm suggesting saves very much, though, so maybe it's not worth changing.

[jdchristensen]

I like that the twist construction worked well here. I suspect that you can also prove symmetry and the twist using a Yoneda argument, using the universal property and properties of biadditive maps. But the way you've done it is pretty straightforward.

[Alizter]

When we later characterize the universal property as a right adjoint to the internal hom, the Yoneda lemma will play a crucial role in proving things like distributivity over the direct sum.

[Alizter]

The pentagon takes 20 universes or so which isn't ideal. I've been trying to chase down the source of the issue but it seems to be quite systemic throughout the groups library. I think basically any time we use $-> instead of GroupHomomorphism we end up introducing a strictly larger universe for the wildcat Group/AbGroup which can be a bit annoying.

[jdchristensen]

The pentagon takes 20 universes or so which isn't ideal. I've been trying to chase down the source of the issue but it seems to be quite systemic throughout the groups library. I think basically any time we use $-> instead of GroupHomomorphism we end up introducing a strictly larger universe for the wildcat Group/AbGroup which can be a bit annoying.

I'm hoping that algebraic universes get merged into Coq soon, which I think will get rid of this problem. We'll be able to use u+1 as the universe that is currently free. So it's probably find to not worry about this too much here. (And 20 isn't too bad.)

coq/coq#18903

[jdchristensen]

If you agree I think we have resolved the final issue here with the slowness.

Well, there are still issues with using cbn which could bite us in the future, but that's also the case in other parts of the library, so I'm happy with how this works now.

It's also great how much simplified by making the free group recursor compute to the expected thing definitionally!

What's left to do in this PR? If you think it's ready to merge, let me make one more pass over it before you do. It might be a day or two before I get a chance.

[Alizter]

@jdchristensen I think another pass would be good. Here is a checklist for the remaining issues that I can think of:

• I think some of the comments in TensorProduct.v need updating as they are referencing the old way of reducing terms. (Edit: I had a look and it seems fine)
• Have another look at why cbn is slow. I think this is due to the unfolding of the type, but I can't understand why the simpl never isn't preventing this from happening.
• Consider renaming ab_tensor_prod to ab_tensor? I've got some preliminary stuff on the tensor product of modules, and there I've named simple tensors mtensor and I can give the abelian group/bimodule a better name. To me ab_tensor seems more economical.

[Alizter]

I wrote a little introduction to the file to explain the tensor product of abelian groups.

When I was first learning about tensor products as an undergraduate I struggled with understanding what they are supposed to be useful for. This probably stems from the fact that it is the first "non-canonical" construction defined by a mapping property. Upto then, the way you constructed objects seemed more important and the idea of a universal mapping property was alien. So having something with just a property and no single definition caused a lot of questions marks.

I think the punchline that should be kept in mind is that they describe biadditive maps. It seems obvious to us now, but it might help any future readers who are maybe not so familiar with the concept.

[jdchristensen]

• Consider renaming ab_tensor_prod to ab_tensor?

I'm fine with this, but how will we name the simple tensors in the module case? One pattern would be ab_tensor_prod, ab_tensor, mtensor_prod and mtensor for the operations on groups/modules and the operations on elements. (Right now we just use tensor for the second one, but it's hard to see how that will have a corresponding name in the module case.)

[Alizter]

I don't yet know what the best names will be once we introduce tensor products of modules, so perhaps the best thing to do would be to rename tensor to ab_tensor. Or alternatively, we could just leave it alone for now.

[Alizter]

After thinking about it some more, at some point when we start doing calculations with modules we might prefer to work only with R-modules and treat abelian groups as Z-modules in that case. Then it might make sense for the module tensor product to have the name mtensor for the type (don't know yet if it will be a bimodule or what) and tensor for simple tensors.

[Alizter]

Out of curiosity here are the longest lines:

./theories/Algebra/AbGroups/TensorProduct:     Chars 199 - 264 [Require~Import~Algebra.Groups....] 0.07 secs (0.04u,0.029s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 3416 - 3424 [Defined.] 0.038 secs (0.024u,0.014s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 23833 - 23864 [(apply~(grp_homo_op~(ab_mul~z))).] 0.036 secs (0.036u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 25793 - 25822 [exact~(tensor_ab_mul~_~_~_)^.] 0.034 secs (0.034u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 14868 - 14899 [(rapply~path_sigma_hprop;~simpl).] 0.029 secs (0.029u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 3736 - 3744 [Defined.] 0.026 secs (0.026u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 11658 - 11725 [rapply~(ab_tensor_prod_ind_hpr...] 0.025 secs (0.025u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 7021 - 7029 [Defined.] 0.022 secs (0.022u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 6539 - 6557 [strip_truncations.] 0.017 secs (0.016u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 16661 - 16669 [Defined.] 0.017 secs (0.017u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 12230 - 12282 [rapply~(ab_tensor_prod_ind_hpr...] 0.017 secs (0.017u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 3396 - 3415 [by~exists~a,b,b'.] 0.016 secs (0.002u,0.014s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 11038 - 11077 [rapply~ab_tensor_prod_ind_hpro...] 0.016 secs (0.016u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 88 - 165 [Require~Import~WildCat.Core~Wi...] 0.015 secs (0.009u,0.005s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 14917 - 14925 [Defined.] 0.014 secs (0.014u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 0 - 46 [Require~Import~Basics.Overture...] 0.012 secs (0.008u,0.004s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 9530 - 9562 [rapply~ab_tensor_prod_ind_hprop.] 0.01 secs (0.01u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 20239 - 20245 [Proof.] 0.01 secs (0.01u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 8990 - 8998 [Defined.] 0.009 secs (0.009u,0.s)
./theories/Algebra/AbGroups/TensorProduct:     Chars 8948 - 8972 [(rewrite~<-~tensor_neg_l).] 0.008 secs (0.008u,0.s)

And the entire file is under 1s.

Benchmark 1: /nix/store/6hyzsj2kifsymlv8zm39lnqrybfbigi9-coq-8.19.2/bin/coqc -R ./theories HoTT -noinit -indices-matter benched_file.v
  Time (mean ± σ):     939.0 ms ±  18.5 ms    [User: 817.2 ms, System: 118.1 ms]
  Range (min … max):   900.0 ms … 965.7 ms    10 runs

There doesn't appear to be any lines that take longer than they should.

[Alizter]

We can mark ab_tensor_prod as opaque and remove a few unfolds and the entire file compiles. We can even remove most of the change statements and replace it with simpl.

However this (only marking as opaque not removing change) has a detrimental effect on the timing of the file, whereby the compilation time goes from 1s to around 1.2s. There is a lot of noise, however the increase appears to be consistent.

Also, cbn still hangs.

[jdchristensen]

However the naming is done, I think we need some pattern between the abelian group names and the module names. And ab_tensor_prod/mtensor_prod isn't really bad for the name of the type.

[jdchristensen]

We can mark ab_tensor_prod as opaque and remove a few unfolds and the entire file compiles. We can even remove most of the change statements and replace it with simpl.

However this (only marking as opaque not removing change) has a detrimental effect on the timing of the file, whereby the compilation time goes from 1s to around 1.2s. There is a lot of noise, however the increase appears to be consistent.

Also, cbn still hangs.

Since it doesn't fix cbn, then I think we should leave it as it is.

[jdchristensen]

I've reread the entire diff, and think it looks good!