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} [CommRing R] {S : Type u_2} [CommRing 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} [CommRing R] {S : Type u_2} [CommRing 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} [CommRing R] {S : Type u_2} [CommRing 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} :

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} [CommRing R] {P : Ideal (Polynomial R)} (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} [CommRing R] {S : Type u_2} [CommRing S] {p : Ideal R} {P : Ideal S} [Algebra R S] [Algebra (R p) (S P)] [IsScalarTower R (R p) (S P)] (h : Function.Injective ↑(algebraMap (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.algebraQuotientOfLEComap {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing 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
Instances For
    instance Ideal.Quotient.algebraQuotientMapQuotient {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing 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.algebraMap_quotient_map_quotient {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {p : Ideal R} (x : R) :
    ↑(algebraMap (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} [CommRing R] {S : Type u_2} [CommRing 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)
    theorem Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I : Ideal S} [IsDomain S] {r : S} (r_ne_zero : r 0) (hr : r I) {p : Polynomial R} :
    theorem Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I : Ideal S} {J : Ideal S} [Ideal.IsPrime I] (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, Polynomial.coeff p i ↑(Ideal.comap f J) \ ↑(Ideal.comap f I)
    theorem Ideal.comap_lt_comap_of_root_mem_sdiff {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I : Ideal S} {J : Ideal S} [Ideal.IsPrime I] (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} [CommRing S] {I : Ideal S} (h : 1 I) (x : S) :
    x I
    theorem Ideal.comap_lt_comap_of_integral_mem_sdiff {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {I : Ideal S} {J : Ideal S} [Algebra R S] [hI : Ideal.IsPrime I] (hIJ : I J) {x : S} (mem : x J \ I) (integral : IsIntegral R x) :
    theorem Ideal.comap_ne_bot_of_root_mem {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I : Ideal S} [IsDomain 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.comap_ne_bot_of_algebraic_mem {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {I : Ideal S} [Algebra R S] [IsDomain S] {x : S} (x_ne_zero : x 0) (x_mem : x I) (hx : IsAlgebraic R x) :
    theorem Ideal.comap_ne_bot_of_integral_mem {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {I : Ideal S} [Algebra R S] [Nontrivial R] [IsDomain S] {x : S} (x_ne_zero : x 0) (x_mem : x I) (hx : IsIntegral R x) :
    theorem Ideal.eq_bot_of_comap_eq_bot {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {I : Ideal S} [Algebra R S] [Nontrivial R] [IsDomain S] (hRS : Algebra.IsIntegral R S) (hI : Ideal.comap (algebraMap R S) I = ) :
    I =
    theorem Ideal.IsIntegralClosure.comap_lt_comap {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] {A : Type u_3} [CommRing A] [Algebra R A] [Algebra A S] [IsScalarTower R A S] [IsIntegralClosure A R S] {I : Ideal A} {J : Ideal A} [Ideal.IsPrime I] (I_lt_J : I < J) :
    theorem Ideal.IsIntegralClosure.comap_ne_bot {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] {A : Type u_3} [CommRing A] [Algebra R A] [Algebra A S] [IsScalarTower R A S] [IsIntegralClosure A R S] [IsDomain A] [Nontrivial R] {I : Ideal A} (I_ne_bot : I ) :
    theorem Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] {A : Type u_3} [CommRing A] [Algebra R A] [Algebra A S] [IsScalarTower R A S] [IsIntegralClosure A R S] [IsDomain A] [Nontrivial R] {I : Ideal A} :
    theorem Ideal.IntegralClosure.comap_lt_comap {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {I : Ideal { x // x integralClosure R S }} {J : Ideal { x // x integralClosure R S }} [Ideal.IsPrime I] (I_lt_J : I < J) :
    theorem Ideal.IntegralClosure.comap_ne_bot {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain S] [Nontrivial R] {I : Ideal { x // x integralClosure R S }} (I_ne_bot : I ) :
    theorem Ideal.IntegralClosure.eq_bot_of_comap_eq_bot {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain S] [Nontrivial R] {I : Ideal { x // x integralClosure R S }} :
    Ideal.comap (algebraMap R { x // x integralClosure R S }) I = I =

    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} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (H : Algebra.IsIntegral R S) (P : Ideal R) [Ideal.IsPrime P] (I : Ideal S) [Ideal.IsPrime I] (hIP : Ideal.comap (algebraMap R S) I 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} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain S] (H : Algebra.IsIntegral R S) (P : Ideal R) [P_max : Ideal.IsMaximal P] (hP : RingHom.ker (algebraMap R S) 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