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.
Implementation notes #
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.
P be an ideal in
R[x]. The map
R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R))
The identity in this lemma asserts that the "obvious" square
R → (R / (P ∩ R)) ↓ ↓ R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R))
commutes. It is used, for instance, in the proof of
in the file
This technical lemma asserts the existence of a polynomial
p in an ideal
P ⊂ R[x]
that is non-zero in the quotient
R / (P ∩ R) [x]. The assumptions are equivalent to
P ≠ 0 and
P ∩ R = (0).
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