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}
(hp : polynomial.eval₂ f r p ∈ I) :
p.coeff 0 ∈ ideal.comap f 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}
(hp : polynomial.eval₂ f r p = 0) :
p.coeff 0 ∈ ideal.comap f 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 = 0 → x = 0)
(hr : r ∈ I)
{p : polynomial R}
(p_ne_zero : p ≠ 0)
(hp : polynomial.eval₂ f r p = 0) :
theorem
ideal.exists_coeff_ne_zero_mem_comap_of_root_mem
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
{f : R →+* S}
{I : ideal S}
{r : S}
(r_ne_zero : r ≠ 0)
(hr : r ∈ I)
{p : polynomial R}
(p_ne_zero : p ≠ 0)
(hp : polynomial.eval₂ f r p = 0) :
theorem
ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
{f : R →+* S}
{I J : ideal S}
[I.is_prime]
(hIJ : I ≤ J)
{r : S}
(hr : r ∈ ↑J \ ↑I)
{p : polynomial R}
(p_ne_zero : polynomial.map (ideal.quotient.mk (ideal.comap f I)) p ≠ 0)
(hpI : polynomial.eval₂ f r p ∈ I) :
∃ (i : ℕ), p.coeff i ∈ ↑(ideal.comap f J) \ ↑(ideal.comap f I)
theorem
ideal.comap_ne_bot_of_root_mem
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
{f : R →+* S}
{I : ideal S}
{r : S}
(r_ne_zero : r ≠ 0)
(hr : r ∈ I)
{p : polynomial R}
(p_ne_zero : p ≠ 0)
(hp : polynomial.eval₂ f r p = 0) :
ideal.comap f I ≠ ⊥
theorem
ideal.comap_lt_comap_of_root_mem_sdiff
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
{f : R →+* S}
{I J : ideal S}
[I.is_prime]
(hIJ : I ≤ J)
{r : S}
(hr : r ∈ ↑J \ ↑I)
{p : polynomial R}
(p_ne_zero : polynomial.map (ideal.quotient.mk (ideal.comap f I)) p ≠ 0)
(hp : polynomial.eval₂ f r p ∈ I) :
ideal.comap f I < ideal.comap f J
theorem
ideal.comap_ne_bot_of_algebraic_mem
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
{I : ideal S}
[algebra R S]
{x : S}
(x_ne_zero : x ≠ 0)
(x_mem : x ∈ I)
(hx : is_algebraic R x) :
ideal.comap (algebra_map R S) I ≠ ⊥
theorem
ideal.comap_ne_bot_of_integral_mem
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
{I : ideal S}
[algebra R S]
[nontrivial R]
{x : S}
(x_ne_zero : x ≠ 0)
(x_mem : x ∈ I)
(hx : is_integral R x) :
ideal.comap (algebra_map R S) I ≠ ⊥
theorem
ideal.mem_of_one_mem
{S : Type u_2}
[integral_domain S]
{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}
[integral_domain S]
{I J : ideal S}
[algebra R S]
[hI : I.is_prime]
(hIJ : I ≤ J)
{x : S}
(mem : x ∈ ↑J \ ↑I)
(integral : is_integral R x) :
ideal.comap (algebra_map R S) I < ideal.comap (algebra_map R S) J
theorem
ideal.is_maximal_of_is_integral_of_is_maximal_comap
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
[algebra R S]
(hRS : algebra.is_integral R S)
(I : ideal S)
[I.is_prime]
(hI : (ideal.comap (algebra_map R S) I).is_maximal) :
theorem
ideal.is_maximal_comap_of_is_integral_of_is_maximal
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
[algebra R S]
(hRS : algebra.is_integral R S)
(I : ideal S)
[hI : I.is_maximal] :
(ideal.comap (algebra_map R S) I).is_maximal
theorem
ideal.integral_closure.comap_ne_bot
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
[algebra R S]
[nontrivial R]
{I : ideal ↥(integral_closure R S)}
(I_ne_bot : I ≠ ⊥) :
ideal.comap (algebra_map R ↥(integral_closure R S)) I ≠ ⊥
theorem
ideal.integral_closure.eq_bot_of_comap_eq_bot
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
[algebra R S]
[nontrivial R]
{I : ideal ↥(integral_closure R S)}
(a : ideal.comap (algebra_map R ↥(integral_closure R S)) I = ⊥) :
theorem
ideal.integral_closure.comap_lt_comap
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
[algebra R S]
{I J : ideal ↥(integral_closure R S)}
[I.is_prime]
(I_lt_J : I < J) :
ideal.comap (algebra_map R ↥(integral_closure R S)) I < ideal.comap (algebra_map R ↥(integral_closure R S)) J
theorem
ideal.integral_closure.is_maximal_of_is_maximal_comap
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
[algebra R S]
(I : ideal ↥(integral_closure R S))
[I.is_prime]
(hI : (ideal.comap (algebra_map R ↥(integral_closure R S)) I).is_maximal) :
theorem
ideal.exists_ideal_over_prime_of_is_integral'
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[integral_domain S]
[algebra R S]
(H : algebra.is_integral R S)
(P : ideal R)
[P.is_prime]
(hP : (algebra_map R S).ker ≤ P) :
∃ (Q : ideal S), Q.is_prime ∧ ideal.comap (algebra_map R 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}
[integral_domain S]
[algebra R S]
(H : algebra.is_integral R S)
(P : ideal R)
[P.is_prime]
(I : ideal S)
[I.is_prime]
(hIP : ideal.comap (algebra_map R S) I ≤ P) :
∃ (Q : ideal S) (H : Q ≥ I), Q.is_prime ∧ ideal.comap (algebra_map R 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