## Stream: maths

### Topic: is_ring_hom.ker

#### 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?

We do...

I think

#### Johan Commelin (Mar 25 2019 at 13:03):

Hmmm... but only in a very convoluted way

#### Johan Commelin (Mar 25 2019 at 13:03):

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

#### Kevin Buzzard (Mar 25 2019 at 13:03):

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

#### 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.

#### Kevin Buzzard (Mar 25 2019 at 13:05):

Or is that not the case?

#### 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.

#### Johan Commelin (Mar 25 2019 at 13:07):

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

#### 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

#### 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.

#### Johan Commelin (Mar 25 2019 at 13:07):

Ooh, not letI of course.

#### Kevin Buzzard (Mar 25 2019 at 13:08):

I was just expecting my proof to look different.

#### Johan Commelin (Mar 25 2019 at 13:08):

I know that feeling (-;

Last updated: May 09 2021 at 10:11 UTC