kernels for ring homomorphisms

Stream: maths

[Casper Putz]

Hi, I wanted to use kernels of ring homomorphisms for the finite fields stuff I am working on with @Joey van Langen . They are not implemented for ring homs, but you would define them exactly the same as is done for linear maps (in linear_algebra.basic). I cannot easily reuse the one for linear maps as a ring homomorphism is not necessarily a linear map of modules. However, all the basic properties of the kernel of a linear map (and ring hom) only depend on the underlying additive group stucture. One could define a kernel of a group_hom and then the kernel (pullback) can be lifted.

I was wondering if there are any reasons for not making linear_map and ring_hom extend group_hom (which would be needed to be defined as only is_group_hom is defined now). This could be done for a lot of these algebraic structures which extend each other, but it could maybe be a bit cumbersome. So I wanted to know some of your opinions about this.

[Johan Commelin]

There are kernels for is_group_hom, I think

[Johan Commelin]

And currently I think we only have is_ring_hom. Not the bundled ring_hom.

[Johan Commelin]

I agree that it would be good if is_ring_hom extended is_add_group_hom.

[Casper Putz]

Ah I see, yes you can reuse the kernel of is_group_hom (didn't see it before). Thanks!

[Casper Putz]

Yes, makes a lot of sense I think

[Johan Commelin]

Beware! In Lean there is currently a difference between group and add_group.

[Johan Commelin]

You would have to refactor is_ring_hom. Which I think makes sense... but it might cause a lot of breakage (it shouldn't).