Ab is abelian

Stream: general

[Scott Morrison]

@Markus Himmel, do you have already, or planned, the constructions that Ab or Module R are abelian?

[Markus Himmel]

I have the version for Module R in my repository (but some cleanup is required)

[Markus Himmel]

Adding the version for Ab was the next thing on my todo list, but I only got as far as noticing that there is some stuff missing in subgroup.lean(like cod_restrict) until I got distracted by real-life obligations yet again

[Kenny Lau]

Ab is just Z-Mod!

[Markus Himmel]

Yes, but pulling the abelian instance via this equivalence gives definitionally not-so-nice kernels, which would make working with exactness less fun

[Johan Commelin]

@Kenny Lau Sure, if you can turn that into a 1-line proof that Ab is abelian (and the resulting biproducts are actually usable), then I'll be you 3 good Belgian beers.

[Scott Morrison]

I just made #3366, which just provides has_image_maps Ab. Later this will hopefully be obsoleted by [abelian Ab], but it would be good to check that that has equally good definitional behaviour.