Zulip Chat Archive

Stream: maths

Topic: kernels for ring homomorphisms


view this post on Zulip Casper Putz (Jan 14 2019 at 12:54):

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.

view this post on Zulip Johan Commelin (Jan 14 2019 at 12:56):

There are kernels for is_group_hom, I think

view this post on Zulip Johan Commelin (Jan 14 2019 at 12:56):

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

view this post on Zulip Johan Commelin (Jan 14 2019 at 12:57):

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

view this post on Zulip Casper Putz (Jan 14 2019 at 13:06):

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

view this post on Zulip Casper Putz (Jan 14 2019 at 13:06):

Yes, makes a lot of sense I think

view this post on Zulip Johan Commelin (Jan 14 2019 at 13:09):

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

view this post on Zulip Johan Commelin (Jan 14 2019 at 13:10):

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


Last updated: May 09 2021 at 11:09 UTC