# Documentation

Mathlib.RingTheory.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} [] {S : Type u_2} [] {f : R →+* S} {I : } {r : S} (hr : r I) {p : } (hp : I) :
theorem Ideal.coeff_zero_mem_comap_of_root_mem {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {I : } {r : S} (hr : r I) {p : } (hp : = 0) :
theorem Ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {I : } {r : S} (r_non_zero_divisor : ∀ {x : S}, x * r = 0x = 0) (hr : r I) {p : } :
p 0 = 0i, 0

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 RingTheory.Jacobson.

theorem Ideal.exists_nonzero_mem_of_ne_bot {R : Type u_1} [] {P : Ideal ()} (Pb : P ) (hP : ∀ (x : R), Polynomial.C x Px = 0) :
p, 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} [] {S : Type u_2} [] {p : } {P : } [Algebra R S] [Algebra (R p) (S P)] [IsScalarTower R (R p) (S P)] (h : Function.Injective ↑(algebraMap (R p) (S P))) :
Ideal.comap () 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.algebraQuotientOfLEComap {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {p : } {P : } (h : p ) :
Algebra (R p) (S P)

If P lies over p, then R / p has a canonical map to S / P.

Instances For
instance Ideal.Quotient.algebraQuotientMapQuotient {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {p : } :
Algebra (R p) (S )

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

@[simp]
theorem Ideal.Quotient.algebraMap_quotient_map_quotient {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {p : } (x : R) :
↑(algebraMap (R p) (S )) (↑() x) = ↑() (f x)
@[simp]
theorem Ideal.Quotient.mk_smul_mk_quotient_map_quotient {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {p : } (x : R) (y : S) :
↑() x ↑() y = ↑() (f x * y)
instance Ideal.Quotient.tower_quotient_map_quotient {R : Type u_1} [] {S : Type u_2} [] {p : } [Algebra R S] :
IsScalarTower R (R p) (S Ideal.map () p)
instance Ideal.QuotientMapQuotient.isNoetherian {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] (I : ) :
IsNoetherian (R I) (S Ideal.map () I)
theorem Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {I : } [] {r : S} (r_ne_zero : r 0) (hr : r I) {p : } :
p 0 = 0i, 0
theorem Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {I : } {J : } [] (hIJ : I J) {r : S} (hr : r J \ I) {p : } (p_ne_zero : 0) (hpI : I) :
i, ↑() \ ↑()
theorem Ideal.comap_lt_comap_of_root_mem_sdiff {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {I : } {J : } [] (hIJ : I J) {r : S} (hr : r J \ I) {p : } (p_ne_zero : 0) (hp : I) :
<
theorem Ideal.mem_of_one_mem {S : Type u_2} [] {I : } (h : 1 I) (x : S) :
x I
theorem Ideal.comap_lt_comap_of_integral_mem_sdiff {R : Type u_1} [] {S : Type u_2} [] {I : } {J : } [Algebra R S] [hI : ] (hIJ : I J) {x : S} (mem : x J \ I) (integral : ) :
theorem Ideal.comap_ne_bot_of_root_mem {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {I : } [] {r : S} (r_ne_zero : r 0) (hr : r I) {p : } (p_ne_zero : p 0) (hp : = 0) :
theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] (hRS : ) (I : ) [] (hI : Ideal.IsMaximal (Ideal.comap () I)) :
theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap' {R : Type u_1} [] {S : Type u_2} [] (f : R →+* S) (hf : ) (I : ) [hI' : ] (hI : ) :
theorem Ideal.comap_ne_bot_of_algebraic_mem {R : Type u_1} [] {S : Type u_2} [] {I : } [Algebra R S] [] {x : S} (x_ne_zero : x 0) (x_mem : x I) (hx : ) :
theorem Ideal.comap_ne_bot_of_integral_mem {R : Type u_1} [] {S : Type u_2} [] {I : } [Algebra R S] [] [] {x : S} (x_ne_zero : x 0) (x_mem : x I) (hx : ) :
theorem Ideal.eq_bot_of_comap_eq_bot {R : Type u_1} [] {S : Type u_2} [] {I : } [Algebra R S] [] [] (hRS : ) (hI : Ideal.comap () I = ) :
I =
theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] (hRS : ) (I : ) [hI : ] :
theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal' {R : Type u_3} {S : Type u_4} [] [] (f : R →+* S) (hf : ) (I : ) (hI : ) :
theorem Ideal.IsIntegralClosure.comap_lt_comap {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] {A : Type u_3} [] [Algebra R A] [Algebra A S] [] [] {I : } {J : } [] (I_lt_J : I < J) :
theorem Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] {A : Type u_3} [] [Algebra R A] [Algebra A S] [] [] (I : ) [] (hI : Ideal.IsMaximal (Ideal.comap () I)) :
theorem Ideal.IsIntegralClosure.comap_ne_bot {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] {A : Type u_3} [] [Algebra R A] [Algebra A S] [] [] [] [] {I : } (I_ne_bot : I ) :
theorem Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] {A : Type u_3} [] [Algebra R A] [Algebra A S] [] [] [] [] {I : } :
Ideal.comap () I = I =
theorem Ideal.IntegralClosure.comap_lt_comap {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] {I : Ideal { x // x }} {J : Ideal { x // x }} [] (I_lt_J : I < J) :
Ideal.comap (algebraMap R { x // x }) I < Ideal.comap (algebraMap R { x // x }) J
theorem Ideal.IntegralClosure.isMaximal_of_isMaximal_comap {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] (I : Ideal { x // x }) [] (hI : Ideal.IsMaximal (Ideal.comap (algebraMap R { x // x }) I)) :
theorem Ideal.IntegralClosure.comap_ne_bot {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] [] {I : Ideal { x // x }} (I_ne_bot : I ) :
Ideal.comap (algebraMap R { x // x }) I
theorem Ideal.IntegralClosure.eq_bot_of_comap_eq_bot {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] [] {I : Ideal { x // x }} :
Ideal.comap (algebraMap R { x // x }) I = I =
theorem Ideal.exists_ideal_over_prime_of_isIntegral' {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] (H : ) (P : ) [] (hP : RingHom.ker () P) :
Q, Ideal.comap () Q = P

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

theorem Ideal.exists_ideal_over_prime_of_isIntegral {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] (H : ) (P : ) [] (I : ) [] (hIP : Ideal.comap () I P) :
Q, Q I Ideal.comap () Q = P

More general going-up theorem than exists_ideal_over_prime_of_isIntegral'. 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_isIntegral {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] (H : ) (P : ) [P_max : ] (hP : RingHom.ker () P) :
Q, Ideal.comap () Q = P

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