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) :
p.coeff 0 Ideal.comap f 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) :
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} [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} :
p 0Polynomial.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.

theorem Ideal.quotient_mk_maps_eq {R : Type u_1} [CommRing R] (P : Ideal (Polynomial R)) :
((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 ((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 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) :
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} [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) :
    @[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) :
    instance Ideal.Quotient.tower_quotient_map_quotient {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {p : Ideal R} [Algebra R S] :
    Equations
    • =
    instance Ideal.QuotientMapQuotient.isNoetherian {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsNoetherian R S] (I : Ideal R) :
    Equations
    • =
    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} :
    p 0Polynomial.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} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I : Ideal S} {J : Ideal S} [I.IsPrime] (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} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I : Ideal S} {J : Ideal S} [I.IsPrime] (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 : I.IsPrime] (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.isMaximal_of_isIntegral_of_isMaximal_comap {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (I : Ideal S) [I.IsPrime] (hI : (Ideal.comap (algebraMap R S) I).IsMaximal) :
    I.IsMaximal
    theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap' {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (I : Ideal S) [I.IsPrime] (hI : (Ideal.comap f I).IsMaximal) :
    I.IsMaximal
    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] [Algebra.IsIntegral R S] (hI : Ideal.comap (algebraMap R S) I = ) :
    I =
    theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (I : Ideal S) [hI : I.IsMaximal] :
    (Ideal.comap (algebraMap R S) I).IsMaximal
    theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal' {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (I : Ideal S) [I.IsMaximal] :
    (Ideal.comap f I).IsMaximal
    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} [I.IsPrime] (I_lt_J : I < J) :
    theorem Ideal.IsIntegralClosure.isMaximal_of_isMaximal_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) [I.IsPrime] (hI : (Ideal.comap (algebraMap R A) I).IsMaximal) :
    I.IsMaximal
    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 (integralClosure R S)} {J : Ideal (integralClosure R S)} [I.IsPrime] (I_lt_J : I < J) :
    theorem Ideal.IntegralClosure.isMaximal_of_isMaximal_comap {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal (integralClosure R S)) [I.IsPrime] (hI : (Ideal.comap (algebraMap R (integralClosure R S)) I).IsMaximal) :
    I.IsMaximal
    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 (integralClosure R S)} (I_ne_bot : I ) :
    theorem Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain S] [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (hP : RingHom.ker (algebraMap R S) P) :
    ∃ (Q : Ideal S), Q.IsPrime Ideal.comap (algebraMap R S) 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} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (I : Ideal S) [I.IsPrime] (hIP : Ideal.comap (algebraMap R S) I P) :
    QI, Q.IsPrime Ideal.comap (algebraMap R S) 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} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (P : Ideal R) [P.IsPrime] (I : Ideal S) (hI : Ideal.comap (algebraMap R S) I P) :
    QI, Q.IsPrime Ideal.comap (algebraMap R S) Q P
    theorem Ideal.exists_ideal_over_prime_of_isIntegral {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (I : Ideal S) (hIP : Ideal.comap (algebraMap R S) I P) :
    QI, Q.IsPrime Ideal.comap (algebraMap R S) Q = P
    theorem Ideal.exists_ideal_over_maximal_of_isIntegral {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (P : Ideal R) [P_max : P.IsMaximal] (hP : RingHom.ker (algebraMap R S) P) :
    ∃ (Q : Ideal S), Q.IsMaximal Ideal.comap (algebraMap R S) 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_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal R} (hf₁ : RingHom.ker f I) (hf₂ : f.IsIntegral) :
    theorem Ideal.map_eq_top_iff {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal R} (hf₁ : Function.Injective f) (hf₂ : f.IsIntegral) :
    @[reducible, inline]
    abbrev Ideal.under (A : Type u_2) [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) :

    The ideal obtained by pulling back the ideal P from B to A.

    Equations
    Instances For
      theorem Ideal.under_def (A : Type u_2) [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) :
      instance Ideal.IsPrime.under (A : Type u_2) [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) [hP : P.IsPrime] :
      (Ideal.under A P).IsPrime
      Equations
      • =
      class Ideal.LiesOver {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) (p : Ideal A) :

      P lies over p if p is the preimage of P of the algebraMap.

      Instances
        theorem Ideal.LiesOver.over {A : Type u_2} :
        ∀ {inst : CommSemiring A} {B : Type u_3} {inst_1 : Semiring B} {inst_2 : Algebra A B} {P : Ideal B} {p : Ideal A} [self : P.LiesOver p], p = Ideal.under A P
        instance Ideal.over_under {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) :
        P.LiesOver (Ideal.under A P)
        Equations
        • =
        theorem Ideal.over_def {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] :
        theorem Ideal.mem_of_liesOver {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] (x : A) :
        x p (algebraMap A B) x P
        @[simp]
        theorem Ideal.under_under {A : Type u_2} [CommSemiring A] {B : Type u_3} [CommSemiring B] {C : Type u_4} [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) :
        theorem Ideal.LiesOver.trans {A : Type u_2} [CommSemiring A] {B : Type u_3} [CommSemiring B] {C : Type u_4} [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (P : Ideal B) (p : Ideal A) [𝔓.LiesOver P] [P.LiesOver p] :
        𝔓.LiesOver p
        theorem Ideal.LiesOver.tower_bot {A : Type u_2} [CommSemiring A] {B : Type u_3} [CommSemiring B] {C : Type u_4} [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (P : Ideal B) (p : Ideal A) [hp : 𝔓.LiesOver p] [hP : 𝔓.LiesOver P] :
        P.LiesOver p
        instance Ideal.under_liesOver_of_liesOver {A : Type u_2} [CommSemiring A] (B : Type u_3) [CommSemiring B] {C : Type u_4} [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (p : Ideal A) [𝔓.LiesOver p] :
        (Ideal.under B 𝔓).LiesOver p
        Equations
        • =
        instance Ideal.Quotient.algebraOfLiesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] :
        Algebra (A p) (B P)

        If P lies over p, then canonically B ⧸ P is a A ⧸ p-algebra.

        Equations
        instance Ideal.Quotient.isScalarTower_of_liesOver (R : Type u_2) [CommSemiring R] {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] [Algebra R A] [Algebra R B] [IsScalarTower R A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] :
        IsScalarTower R (A p) (B P)
        Equations
        • =
        instance Ideal.Quotient.module_finite_of_liesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [Module.Finite A B] :
        Module.Finite (A p) (B P)

        B ⧸ P is a finite A ⧸ p-module if B is a finite A-module.

        Equations
        • =
        instance Ideal.Quotient.algebra_finiteType_of_liesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [Algebra.FiniteType A B] :

        B ⧸ P is a finitely generated A ⧸ p-algebra if B is a finitely generated A-algebra.

        Equations
        • =
        instance Ideal.Quotient.isNoetherian_of_liesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [IsNoetherian A B] :
        IsNoetherian (A p) (B P)

        B ⧸ P is a Noetherian A ⧸ p-module if B is a Noetherian A-module.

        Equations
        • =
        theorem Ideal.Quotient.algebraMap_injective_of_liesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] :
        instance Ideal.Quotient.instNoZeroSMulDivisorsQuotientOfIsPrime {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [P.IsPrime] :
        Equations
        • =
        instance Ideal.IsMaximal.under (A : Type u_2) [CommRing A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (P : Ideal B) [P.IsMaximal] :
        (Ideal.under A P).IsMaximal

        If B is an integral A-algebra, P is a maximal ideal of B, then the pull back of P is also a maximal ideal of A.

        Equations
        • =
        theorem Ideal.IsMaximal.of_liesOver_isMaximal {A : Type u_2} [CommRing A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [hpm : p.IsMaximal] [P.IsPrime] :
        P.IsMaximal
        theorem Ideal.IsMaximal.of_isMaximal_liesOver {A : Type u_2} [CommRing A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [P.IsMaximal] :
        p.IsMaximal
        instance Ideal.Quotient.algebra_isIntegral_of_liesOver {A : Type u_2} [CommRing A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] :

        B ⧸ P is an integral A ⧸ p-algebra if B is a integral A-algebra.

        Equations
        • =