Ideals over/under ideals
This file concerns ideals lying over other ideals.
f : R →+* S be a ring homomorphism (typically a ring extension),
I an ideal of
J an ideal of
S. We say
J lies over
I is the
This is expressed here by writing
I = J.comap f.
The proofs of the
comap_lt_comap families use an approach
specific for their situation: we construct an element in
I.comap f from the
coefficients of a minimal polynomial.
Once mathlib has more material on the localization at a prime ideal, the results
can be proven using more general going-up/going-down theory.
More general going-up theorem than
TODO: Version of going-up theorem with arbitrary length chains (by induction on this)?
Not sure how best to write an ascending chain in Lean