is_ring_hom.ker

Stream: maths

[Kevin Buzzard]

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?

[Johan Commelin]

We do...

[Johan Commelin]

I think

[Johan Commelin]

Hmmm... but only in a very convoluted way

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Or is that not the case?

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

Ooh, not letI of course.

[Kevin Buzzard]

I was just expecting my proof to look different.

[Johan Commelin]

I know that feeling (-;