Zulip Chat Archive

Stream: maths

Topic: is_ring_hom.ker


view this post on Zulip Kevin Buzzard (Mar 25 2019 at 12:55):

There is no occurrence of ker in algebra/ring.lean. Do we not have the defintion of the kernel of a ring homomorphism, and the fact that it is an ideal, in mathlib?

view this post on Zulip Johan Commelin (Mar 25 2019 at 13:03):

We do...

view this post on Zulip Johan Commelin (Mar 25 2019 at 13:03):

I think

view this post on Zulip Johan Commelin (Mar 25 2019 at 13:03):

Hmmm... but only in a very convoluted way

view this post on Zulip Johan Commelin (Mar 25 2019 at 13:03):

Every ring hom gives a linear map... and we have kernels of linear maps

view this post on Zulip Kevin Buzzard (Mar 25 2019 at 13:03):

I couldn't find any occurrence of ker in ring_theory/ideals.lean either.

view this post on Zulip Kevin Buzzard (Mar 25 2019 at 13:04):

This would involve making my target ring a module over my source ring in some sort of "once and for all" way, which is not what I want in this situation.

view this post on Zulip Kevin Buzzard (Mar 25 2019 at 13:05):

Or is that not the case?

view this post on Zulip Johan Commelin (Mar 25 2019 at 13:07):

Hmm... ideals are bundled. Ring homs aren't... That might hint at why it's not there. It's just how history went.

view this post on Zulip Johan Commelin (Mar 25 2019 at 13:07):

You really need an ideal? Or is a subgroup enough?

view this post on Zulip Johan Commelin (Mar 25 2019 at 13:07):

If you need an ideal, the best way is to upgrade your ring hom to a linear map. You can do this locally in the proof with letI

view this post on Zulip Kevin Buzzard (Mar 25 2019 at 13:07):

I don't need anything -- I am currently ignoring this completely and just working with the stuff which gets sent to zero.

view this post on Zulip Johan Commelin (Mar 25 2019 at 13:07):

Ooh, not letI of course.

view this post on Zulip Kevin Buzzard (Mar 25 2019 at 13:08):

I was just expecting my proof to look different.

view this post on Zulip Johan Commelin (Mar 25 2019 at 13:08):

I know that feeling (-;


Last updated: May 09 2021 at 10:11 UTC