Ideals over/under ideals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.injective_quotient_le_comap_map
{R : Type u_1}
[comm_ring R]
(P : ideal (polynomial R)) :
Let P be an ideal in R[x]. The map
R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R))
is injective.
theorem
ideal.quotient_mk_maps_eq
{R : Type u_1}
[comm_ring R]
(P : ideal (polynomial R)) :
((ideal.quotient.mk (ideal.map (polynomial.map_ring_hom (ideal.quotient.mk (ideal.comap polynomial.C P))) P)).comp polynomial.C).comp (ideal.quotient.mk (ideal.comap polynomial.C P)) = ((ideal.map (polynomial.map_ring_hom (ideal.quotient.mk (ideal.comap polynomial.C P))) P).quotient_map (polynomial.map_ring_hom (ideal.quotient.mk (ideal.comap polynomial.C P))) ideal.le_comap_map).comp ((ideal.quotient.mk P).comp polynomial.C)
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 quotient_mk_comp_C_is_integral_of_jacobson,
in the file ring_theory/jacobson.
theorem
ideal.exists_nonzero_mem_of_ne_bot
{R : Type u_1}
[comm_ring R]
{P : ideal (polynomial R)}
(Pb : P ≠ ⊥)
(hP : ∀ (x : R), ⇑polynomial.C x ∈ P → x = 0) :
∃ (p : polynomial R), p ∈ P ∧ polynomial.map (ideal.quotient.mk (ideal.comap polynomial.C P)) p ≠ 0
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).
theorem
ideal.comap_eq_of_scalar_tower_quotient
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
{p : ideal R}
{P : ideal S}
[algebra R S]
[algebra (R ⧸ p) (S ⧸ P)]
[is_scalar_tower R (R ⧸ p) (S ⧸ P)]
(h : function.injective ⇑(algebra_map (R ⧸ p) (S ⧸ P))) :
ideal.comap (algebra_map R S) P = p
If there is an injective map R/p → S/P such that following diagram commutes:
R → S
↓ ↓
R/p → S/P
then P lies over p.
def
ideal.quotient.algebra_quotient_of_le_comap
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
{f : R →+* S}
{p : ideal R}
{P : ideal S}
(h : p ≤ ideal.comap f P) :
If P lies over p, then R / p has a canonical map to S / P.
Equations
@[protected, instance]
def
ideal.quotient.algebra_quotient_map_quotient
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
{f : R →+* S}
{p : ideal R} :
R / p has a canonical map to S / pS.
Equations
- ideal.quotient.algebra_quotient_map_quotient = ideal.quotient.algebra_quotient_of_le_comap ideal.quotient.algebra_quotient_map_quotient._proof_1
@[simp]
theorem
ideal.quotient.algebra_map_quotient_map_quotient
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
{f : R →+* S}
{p : ideal R}
(x : R) :
⇑(algebra_map (R ⧸ p) (S ⧸ ideal.map f p)) (⇑(ideal.quotient.mk p) x) = ⇑(ideal.quotient.mk (ideal.map f p)) (⇑f x)
@[simp]
theorem
ideal.quotient.mk_smul_mk_quotient_map_quotient
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
{f : R →+* S}
{p : ideal R}
(x : R)
(y : S) :
⇑(ideal.quotient.mk p) x • ⇑(ideal.quotient.mk (ideal.map f p)) y = ⇑(ideal.quotient.mk (ideal.map f p)) (⇑f x * y)
@[protected, instance]
def
ideal.quotient.tower_quotient_map_quotient
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
{p : ideal R}
[algebra R S] :
is_scalar_tower R (R ⧸ p) (S ⧸ ideal.map (algebra_map R S) p)
@[protected, instance]
def
ideal.quotient_map_quotient.is_noetherian
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_noetherian R S]
(I : ideal R) :
is_noetherian (R ⧸ I) (S ⧸ ideal.map (algebra_map R S) I)
theorem
ideal.exists_coeff_ne_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}
[is_domain 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}
[comm_ring 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_lt_comap_of_root_mem_sdiff
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring 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_lt_comap_of_integral_mem_sdiff
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring 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.comap_ne_bot_of_root_mem
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
{f : R →+* S}
{I : ideal S}
[is_domain 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.is_maximal_of_is_integral_of_is_maximal_comap
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring 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_of_is_integral_of_is_maximal_comap'
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
(f : R →+* S)
(hf : f.is_integral)
(I : ideal S)
[hI' : I.is_prime]
(hI : (ideal.comap f I).is_maximal) :
theorem
ideal.comap_ne_bot_of_algebraic_mem
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
{I : ideal S}
[algebra R S]
[is_domain 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}
[comm_ring S]
{I : ideal S}
[algebra R S]
[nontrivial R]
[is_domain S]
{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.eq_bot_of_comap_eq_bot
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
{I : ideal S}
[algebra R S]
[nontrivial R]
[is_domain S]
(hRS : algebra.is_integral R S)
(hI : ideal.comap (algebra_map R S) I = ⊥) :
theorem
ideal.is_maximal_comap_of_is_integral_of_is_maximal
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring 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.is_maximal_comap_of_is_integral_of_is_maximal'
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : f.is_integral)
(I : ideal S)
(hI : I.is_maximal) :
(ideal.comap f I).is_maximal
theorem
ideal.is_integral_closure.comap_lt_comap
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
{A : Type u_3}
[comm_ring A]
[algebra R A]
[algebra A S]
[is_scalar_tower R A S]
[is_integral_closure A R S]
{I J : ideal A}
[I.is_prime]
(I_lt_J : I < J) :
ideal.comap (algebra_map R A) I < ideal.comap (algebra_map R A) J
theorem
ideal.is_integral_closure.is_maximal_of_is_maximal_comap
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
{A : Type u_3}
[comm_ring A]
[algebra R A]
[algebra A S]
[is_scalar_tower R A S]
[is_integral_closure A R S]
(I : ideal A)
[I.is_prime]
(hI : (ideal.comap (algebra_map R A) I).is_maximal) :
theorem
ideal.is_integral_closure.comap_ne_bot
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
{A : Type u_3}
[comm_ring A]
[algebra R A]
[algebra A S]
[is_scalar_tower R A S]
[is_integral_closure A R S]
[is_domain A]
[nontrivial R]
{I : ideal A}
(I_ne_bot : I ≠ ⊥) :
ideal.comap (algebra_map R A) I ≠ ⊥
theorem
ideal.is_integral_closure.eq_bot_of_comap_eq_bot
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
{A : Type u_3}
[comm_ring A]
[algebra R A]
[algebra A S]
[is_scalar_tower R A S]
[is_integral_closure A R S]
[is_domain A]
[nontrivial R]
{I : ideal A} :
ideal.comap (algebra_map R A) I = ⊥ → I = ⊥
theorem
ideal.integral_closure.comap_lt_comap
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring 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}
[comm_ring 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.integral_closure.comap_ne_bot
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_domain 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}
[comm_ring S]
[algebra R S]
[is_domain S]
[nontrivial R]
{I : ideal ↥(integral_closure R S)} :
ideal.comap (algebra_map R ↥(integral_closure R S)) I = ⊥ → I = ⊥
theorem
ideal.exists_ideal_over_prime_of_is_integral'
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_domain S]
(H : algebra.is_integral R S)
(P : ideal R)
[P.is_prime]
(hP : ring_hom.ker (algebra_map R S) ≤ 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}
[comm_ring 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
theorem
ideal.exists_ideal_over_maximal_of_is_integral
{R : Type u_1}
[comm_ring R]
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_domain S]
(H : algebra.is_integral R S)
(P : ideal R)
[P_max : P.is_maximal]
(hP : ring_hom.ker (algebra_map R S) ≤ P) :
∃ (Q : ideal S), Q.is_maximal ∧ ideal.comap (algebra_map R 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