## Stream: Is there code for X?

### Topic: maximal ideals in integral extensions

#### Devon Tuma (Aug 14 2020 at 18:08):

I've found in ring_theory/ideal/over.lean the statement is_maximal_of_is_integral_of_is_maximal_comap, but I can't find a converse statement along the lines of is_maximal_comap_of_is_integral_of_is_maximal, which is what I want. I would guess this doesn't exist yet since I'd expect it to be in the same file, but I wanted to double check I wasn't missing something before I try and write a proof myself.

#### Johan Commelin (Aug 14 2020 at 19:12):

@Anne Baanen Can you confirm?
But I guess it's true that we don't have this.

#### Johan Commelin (Aug 14 2020 at 19:13):

If someone wants to do going-up/going-down theorems, that would be nice! I think there are even comments about such a TODO in that file.

#### Devon Tuma (Aug 14 2020 at 20:41):

I could look at doing some of that then, it seems better than just ad-hoc proving the one statement I want, assuming no one else is already working on anything in that area.

#### Anne Baanen (Aug 15 2020 at 09:31):

That file was mostly me ad-hoc proving the statements that I needed. I would be very happy if you do (some of) going-up/going-down!

Last updated: May 17 2021 at 16:26 UTC