# 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) :
p.coeff 0
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) :
p.coeff 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 = 0∃ (i : ), p.coeff i 0 p.coeff i

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} [] (P : Ideal ()) :
((Ideal.Quotient.mk (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)).comp Polynomial.C).comp (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) = (Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P) (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) ).comp (.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 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) :
pP, 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.

Equations
• = ().toAlgebra
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.

Equations
• Ideal.Quotient.algebraQuotientMapQuotient =
@[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)
Equations
• =
instance Ideal.QuotientMapQuotient.isNoetherian {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] (I : ) :
IsNoetherian (R I) (S Ideal.map () I)
Equations
• =
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 = 0∃ (i : ), p.coeff i 0 p.coeff i
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 : } [I.IsPrime] (hIJ : I J) {r : S} (hr : r J \ I) {p : } (p_ne_zero : 0) (hpI : I) :
∃ (i : ), p.coeff i () \ ()
theorem Ideal.comap_lt_comap_of_root_mem_sdiff {R : Type u_1} [] {S : Type u_2} [] {f : R →+* S} {I : } {J : } [I.IsPrime] (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 : I.IsPrime] (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] [] (I : ) [I.IsPrime] (hI : (Ideal.comap () I).IsMaximal) :
I.IsMaximal
theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap' {R : Type u_1} [] {S : Type u_2} [] (f : R →+* S) (hf : f.IsIntegral) (I : ) [I.IsPrime] (hI : ().IsMaximal) :
I.IsMaximal
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] [] [] [] (hI : Ideal.comap () I = ) :
I =
theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] (I : ) [hI : I.IsMaximal] :
(Ideal.comap () I).IsMaximal
theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal' {R : Type u_3} {S : Type u_4} [] [] (f : R →+* S) (hf : f.IsIntegral) (I : ) [I.IsMaximal] :
().IsMaximal
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.IsPrime] (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 : ) [I.IsPrime] (hI : (Ideal.comap () I).IsMaximal) :
I.IsMaximal
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 ()} {J : Ideal ()} [I.IsPrime] (I_lt_J : I < J) :
theorem Ideal.IntegralClosure.isMaximal_of_isMaximal_comap {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] (I : Ideal ()) [I.IsPrime] (hI : (Ideal.comap (algebraMap R ()) I).IsMaximal) :
I.IsMaximal
theorem Ideal.IntegralClosure.comap_ne_bot {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] [] {I : Ideal ()} (I_ne_bot : I ) :
theorem Ideal.IntegralClosure.eq_bot_of_comap_eq_bot {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] [] {I : Ideal ()} :
Ideal.comap (algebraMap R ()) I = I =
theorem Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] [] (P : ) [P.IsPrime] (hP : RingHom.ker () P) :
∃ (Q : ), Q.IsPrime 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_of_isPrime {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] (P : ) [P.IsPrime] (I : ) [I.IsPrime] (hIP : Ideal.comap () I P) :
QI, Q.IsPrime Ideal.comap () Q = P

More general going-up theorem than exists_ideal_over_prime_of_isIntegral_of_isDomain. 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_comap_le_prime {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] (P : ) [P.IsPrime] (I : ) (hI : Ideal.comap () I P) :
QI, Q.IsPrime Ideal.comap () Q P
theorem Ideal.exists_ideal_over_prime_of_isIntegral {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] (P : ) [P.IsPrime] (I : ) (hIP : Ideal.comap () I P) :
QI, Q.IsPrime Ideal.comap () Q = P
theorem Ideal.exists_ideal_over_maximal_of_isIntegral {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] [] (P : ) [P_max : P.IsMaximal] (hP : RingHom.ker () P) :
∃ (Q : ), Q.IsMaximal 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

theorem Ideal.map_eq_top_iff_of_ker_le {R : Type u_1} [] {S : Type u_2} [] (f : R →+* S) {I : } (hf₁ : I) (hf₂ : f.IsIntegral) :
theorem Ideal.map_eq_top_iff {R : Type u_1} [] {S : Type u_2} [] (f : R →+* S) {I : } (hf₁ : ) (hf₂ : f.IsIntegral) :