mathlib documentation

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} (hp : polynomial.eval₂ f r p 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) :
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_ne_zero : p 0) (hp : polynomial.eval₂ f r p = 0) :
∃ (i : ), p.coeff i 0 p.coeff i ideal.comap f I

Let P be an ideal in R[x]. The map R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R)) is injective.

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 Px = 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))) :

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) :
algebra (R p) (S 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} :
algebra (R p) (S ideal.map f p)

R / p has a canonical map to S / pS.

Equations
@[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) :
@[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) :
@[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] :
@[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) :
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) :
∃ (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} [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) :
theorem ideal.mem_of_one_mem {S : Type u_2} [comm_ring 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} [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) :
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) :
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) :
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) :
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 = ) :
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] :
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) :
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) :
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 ) :
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} :
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) :
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 ) :
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