Ideals over/under ideals in integral extensions #
This file proves some going-up results for integral algebras.
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.injective_quotient_le_comap_map
{R : Type u_1}
[CommRing R]
(P : Ideal (Polynomial R))
:
Function.Injective
⇑(quotientMap (map (Polynomial.mapRingHom (Quotient.mk (comap Polynomial.C P))) P)
(Polynomial.mapRingHom (Quotient.mk (comap Polynomial.C P))) ⋯)
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))
:
((Quotient.mk (map (Polynomial.mapRingHom (Quotient.mk (comap Polynomial.C P))) P)).comp Polynomial.C).comp
(Quotient.mk (comap Polynomial.C P)) = (quotientMap (map (Polynomial.mapRingHom (Quotient.mk (comap Polynomial.C P))) P)
(Polynomial.mapRingHom (Quotient.mk (comap Polynomial.C P))) ⋯).comp
((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 Mathlib/RingTheory/Jacobson/Polynomial.lean.
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 ∈ P → x = 0)
:
∃ p ∈ P, Polynomial.map (Quotient.mk (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.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 J : Ideal S}
[I.IsPrime]
(hIJ : I ≤ J)
{r : S}
(hr : r ∈ ↑J \ ↑I)
{p : Polynomial R}
(p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0)
(hpI : Polynomial.eval₂ f r p ∈ 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 J : Ideal S}
[I.IsPrime]
(hIJ : I ≤ J)
{r : S}
(hr : r ∈ ↑J \ ↑I)
{p : Polynomial R}
(p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0)
(hp : Polynomial.eval₂ f r p ∈ I)
:
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 : (comap (algebraMap R S) I).IsMaximal)
:
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 : comap (algebraMap R S) 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]
:
(comap (algebraMap R S) 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 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 : (comap (algebraMap R A) 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 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 : (comap (algebraMap R ↥(integralClosure R S)) 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.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 ↥(integralClosure R S)}
:
comap (algebraMap R ↥(integralClosure R S)) I = ⊥ → 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)
:
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 : comap (algebraMap R S) I ≤ P)
:
∃ Q ≥ I, Q.IsPrime ∧ 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_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 : comap (algebraMap R S) I ≤ P)
:
∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P
instance
Ideal.nonempty_primesOver
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
[IsDomain R]
[Nontrivial S]
[Algebra.IsIntegral R S]
[Module.IsTorsionFree R S]
(P : Ideal R)
[P.IsPrime]
:
Nonempty ↑(P.primesOver S)
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)
:
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.exists_maximal_ideal_liesOver_of_isIntegral
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
[Algebra.IsIntegral R S]
[FaithfulSMul R S]
(P : Ideal R)
[P.IsMaximal]
:
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)
:
theorem
Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
{p : Ideal R}
[p.IsPrime]
{q : Ideal S}
[q.IsPrime]
(hq : p.primesOver S = {q})
[Algebra.IsIntegral R S]
(x : S)
(hx : x ∉ q)
:
∃ r ∉ p, x ∣ (algebraMap R S) r
If S is an integral R-algebra such that q is the unique prime of S lying over
a prime p of R, then any x ∉ q divides some r ∉ p.
instance
Ideal.IsMaximal.under
(A : Type u_1)
[CommRing A]
{B : Type u_2}
[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.
theorem
Ideal.eq_bot_of_liesOver_bot
(A : Type u_1)
[CommRing A]
{B : Type u_2}
[CommRing B]
[Algebra A B]
[Algebra.IsIntegral A B]
(P : Ideal B)
[Nontrivial A]
[IsDomain B]
[h : P.LiesOver ⊥]
:
instance
Ideal.Quotient.algebra_isIntegral_of_liesOver
{A : Type u_1}
[CommRing A]
{B : Type u_2}
[CommRing B]
[Algebra A B]
[Algebra.IsIntegral A B]
(P : Ideal B)
(p : Ideal A)
[P.LiesOver p]
:
Algebra.IsIntegral (A ⧸ p) (B ⧸ P)
B ⧸ P is an integral A ⧸ p-algebra if B is an integral A-algebra.
@[deprecated Ideal.exists_maximal_ideal_liesOver_of_isIntegral (since := "2025-11-06")]
theorem
Ideal.exists_ideal_liesOver_maximal_of_isIntegral
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
[Algebra.IsIntegral R S]
[FaithfulSMul R S]
(P : Ideal R)
[P.IsMaximal]
:
instance
Ideal.primesOver.isMaximal
{A : Type u_1}
[CommRing A]
{p : Ideal A}
[p.IsMaximal]
{B : Type u_2}
[CommRing B]
[Algebra A B]
[Algebra.IsIntegral A B]
(Q : ↑(p.primesOver B))
:
(↑Q).IsMaximal
theorem
Ideal.isMaximal_of_mem_primesOver
{A : Type u_1}
[CommRing A]
{p : Ideal A}
[p.IsMaximal]
{B : Type u_2}
[CommRing B]
[Algebra A B]
[Algebra.IsIntegral A B]
{P : Ideal B}
(hP : P ∈ p.primesOver B)
:
theorem
Ideal.primesOver_bot
(A : Type u_1)
[CommRing A]
(B : Type u_2)
[CommRing B]
[Algebra A B]
[Algebra.IsIntegral A B]
[Module.IsTorsionFree A B]
[IsDomain A]
[IsDomain B]
: