# mathlibdocumentation

ring_theory.ideal.over

# Ideals over/under ideals

This file concerns ideals lying over other ideals. Let f : R →+* S be a ring homomorphism (typically a ring extension), I an ideal of R and J an ideal of S. We say J lies over I (and I under J) if I is the f-preimage of J. This is expressed here by writing I = J.comap f.

## Implementation notes

The proofs of the comap_ne_bot and 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.

theorem ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {f : R →+* S} {I : ideal S} {r : S} (hr : r I) {p : polynomial R} :
p Ip.coeff 0 I

theorem ideal.coeff_zero_mem_comap_of_root_mem {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {f : R →+* S} {I : ideal S} {r : S} (hr : r I) {p : polynomial R} :
p = 0p.coeff 0 I

theorem ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {f : R →+* S} {I : ideal S} {r : S} (r_non_zero_divisor : ∀ {x : S}, x * r = 0x = 0) (hr : r I) {p : polynomial R} :
p 0 p = 0(∃ (i : ), p.coeff i 0 p.coeff i I)

theorem ideal.exists_coeff_ne_zero_mem_comap_of_root_mem {R : Type u_1} [comm_ring R] {S : Type u_2} {f : R →+* S} {I : ideal S} {r : S} (r_ne_zero : r 0) (hr : r I) {p : polynomial R} :
p 0 p = 0(∃ (i : ), p.coeff i 0 p.coeff i I)

theorem ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff {R : Type u_1} [comm_ring R] {S : Type u_2} {f : R →+* S} {I J : ideal S} [I.is_prime] (hIJ : I J) {r : S} (hr : r J \ I) {p : polynomial R} :
p 0 p I(∃ (i : ), p.coeff i J) \ I))

theorem ideal.comap_ne_bot_of_root_mem {R : Type u_1} [comm_ring R] {S : Type u_2} {f : R →+* S} {I : ideal S} {r : S} (r_ne_zero : r 0) (hr : r I) {p : polynomial R} :
p 0 p = 0 I

theorem ideal.comap_lt_comap_of_root_mem_sdiff {R : Type u_1} [comm_ring R] {S : Type u_2} {f : R →+* S} {I J : ideal S} [I.is_prime] (hIJ : I J) {r : S} (hr : r J \ I) {p : polynomial R} :
p 0 p I I < J

theorem ideal.comap_ne_bot_of_algebraic_mem {R : Type u_1} [comm_ring R] {S : Type u_2} {I : ideal S} [ S] {x : S} :
x 0x I xideal.comap S) I

theorem ideal.comap_ne_bot_of_integral_mem {R : Type u_1} [comm_ring R] {S : Type u_2} {I : ideal S} [ S] [nontrivial R] {x : S} :
x 0x I xideal.comap S) I

theorem ideal.eq_bot_of_comap_eq_bot {R : Type u_1} [comm_ring R] {S : Type u_2} {I : ideal S} [ S] [nontrivial R] :
ideal.comap S) I = I =

theorem ideal.mem_of_one_mem {S : Type u_2} {I : ideal S} (h : 1 I) (x : S) :
x I

theorem ideal.comap_lt_comap_of_integral_mem_sdiff {R : Type u_1} [comm_ring R] {S : Type u_2} {I J : ideal S} [ S] [hI : I.is_prime] (hIJ : I J) {x : S} :
x J \ I xideal.comap S) I < ideal.comap S) J

theorem ideal.is_maximal_of_is_integral_of_is_maximal_comap {R : Type u_1} [comm_ring R] {S : Type u_2} [ S] (hRS : S) (I : ideal S) [I.is_prime] :

theorem ideal.is_maximal_comap_of_is_integral_of_is_maximal {R : Type u_1} [comm_ring R] {S : Type u_2} [ S] (hRS : S) (I : ideal S) [hI : I.is_maximal] :

theorem ideal.integral_closure.comap_ne_bot {R : Type u_1} [comm_ring R] {S : Type u_2} [ S] [nontrivial R] {I : ideal S)} :

theorem ideal.integral_closure.eq_bot_of_comap_eq_bot {R : Type u_1} [comm_ring R] {S : Type u_2} [ S] [nontrivial R] {I : ideal S)} :
ideal.comap S)) I = I =

theorem ideal.integral_closure.comap_lt_comap {R : Type u_1} [comm_ring R] {S : Type u_2} [ S] {I J : ideal S)} [I.is_prime] :
I < Jideal.comap S)) I < ideal.comap S)) J

theorem ideal.integral_closure.is_maximal_of_is_maximal_comap {R : Type u_1} [comm_ring R] {S : Type u_2} [ S] (I : ideal S)) [I.is_prime] :

theorem ideal.exists_ideal_over_prime_of_is_integral' {R : Type u_1} [comm_ring R] {S : Type u_2} [ S] (H : S) (P : ideal R) [P.is_prime] :
S).ker P(∃ (Q : ideal S), Q.is_prime ideal.comap S) Q = P)

comap (algebra_map R S) is a surjection from the prime spec of R to prime spec of S. hP : (algebra_map R S).ker ≤ P is a slight generalization of the extension being injective

theorem ideal.exists_ideal_over_prime_of_is_integral {R : Type u_1} [comm_ring R] {S : Type u_2} [ S] (H : S) (P : ideal R) [P.is_prime] (I : ideal S) [I.is_prime] :
ideal.comap S) I P(∃ (Q : ideal S) (H : Q I), Q.is_prime ideal.comap S) Q = P)

More general going-up theorem than exists_ideal_over_prime_of_is_integral'. 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

theorem ideal.exists_ideal_over_maximal_of_is_integral {R : Type u_1} [comm_ring R] {S : Type u_2} [ S] (H : S) (P : ideal R) [P_max : P.is_maximal] :
S).ker P(∃ (Q : ideal S), Q.is_maximal ideal.comap S) Q = P)

comap (algebra_map R S) is a surjection from the max spec of S to max spec of R. hP : (algebra_map R S).ker ≤ P is a slight generalization of the extension being injective