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} :
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} :
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 ≠ 0 → polynomial.eval₂ f r p = 0 → (∃ (i : ℕ), p.coeff i ≠ 0 ∧ p.coeff i ∈ ideal.comap f I)
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 ≠ 0 → polynomial.eval₂ f r p = 0 → (∃ (i : ℕ), p.coeff i ≠ 0 ∧ p.coeff i ∈ ideal.comap f I)
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} :
polynomial.map (ideal.quotient.mk (ideal.comap f I)) p ≠ 0 → 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 ≠ 0 → 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} :
polynomial.map (ideal.quotient.mk (ideal.comap f I)) p ≠ 0 → 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 ≠ 0 → x ∈ I → 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 ≠ 0 → x ∈ I → 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} :
x ∈ ↑J \ ↑I → 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 : ∀ (x : S), is_integral R x)
(I : ideal S)
[I.is_prime] :
(ideal.comap (algebra_map R S) I).is_maximal → 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 ≠ ⊥ → 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)} :
ideal.comap (algebra_map R ↥(integral_closure R S)) I = ⊥ → 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 < 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] :
(ideal.comap (algebra_map R ↥(integral_closure R S)) I).is_maximal → I.is_maximal