Z-module structure on abelian groups

[ThomatoTomato]

We want to make lm_carrier into an equivalence of categories.

Pipeline:

• Turn lm_carrier : LeftModule R -> AbGroup into a functor
• Define a canonical Z-module structure
• Prove that lm_carrier is an equivalence
• Define a coercion from AbGroup into LeftModule cring_Z and write tests

[Alizter]

This is grp_homo_op. We define ab_mul as a map from Z to group endomorphisms. This means that the left dist property for modules is just the group homomorphism preserving the operation.

[Alizter]

Actually it seems we are missing a lot (in the existing library) here which is a shame. I think the best way forward would be to try to generalise what I've called cring_catamorphism which is integer multiplication with 1 to an arbitrary ring element. That way it would generalise the ab_mul function and the lemmas we prove about cring_catamorphism should generalise past multiplication with 1. That should encompass most of what we want to prove here.

The issue with this however is that I would like to switch from BinInt to Int soon, which should simplify the proofs here. So maybe we should hold off on this for the time being until we clean that up.

Thank you for taking a look at this however.

[jdchristensen]

Comment style as I mentioned in the other PR. I'll let you check all comments.

[jdchristensen]

I think the best way forward would be to try to generalise what I've called cring_catamorphism which is integer multiplication with 1 to an arbitrary ring element.

In fact, as far as I can see, cring_catamorphism doesn't use anything about R being a ring except that it has a chosen element 1. Once you generalize it to an arbitrary ring element, then R should only be assumed to be an abelian group, and the material on cring_catamorphism should be renamed and moved to the AbGroups folder. (In fact, it probably doesn't even use that the group is abelian, so could be moved to Groups.)

[jdchristensen]

We should probably call this grp_pow_int and put it and its properties in Groups.v, right after grp_pow. (Unless, for dependency reasons, we don't want Groups.v to depend on the definition of the integers?) And I agree that we should use the newer definition of the integers for this. Since the newer definition is in the library, this could be done now, right?

[Alizter]

@jdchristensen Yes, we could do this immediately. I can work on that today if you like.

[jdchristensen]

I can work on that today if you like.

Sounds good to me, unless you think it might be a good thing for @ThomatoTomato to tackle (with an outline of what is needed). Probably we want to implement and use something like what is in Spaces/BinInt/Equiv.v, using that in a group, multiplication by a fixed element is an equivalence. (OTOH, if we define grp_pow_int directly from the definition of Int, it might compute better? Not sure.)

[jdchristensen]

Ah, I see that you already started on this, asking @ThomatoTomato for help.

[Alizter]

I created #1995 which is partially finished.