maximal ideals in integral extensions

Stream: Is there code for X?

[Devon Tuma]

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]

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

[Johan Commelin]

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]

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]

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!